Initial program 12.4
\[\frac{\sin ky}{\sqrt{{\left(\sin kx\right)}^{2} + {\left(\sin ky\right)}^{2}}} \cdot \sin th\]
Simplified12.4
\[\leadsto \color{blue}{\sin th \cdot \frac{\sin ky}{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}\]
- Using strategy
rm Applied *-commutative12.4
\[\leadsto \sin th \cdot \frac{\sin ky}{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}\]
- Using strategy
rm Applied add-sqr-sqrt12.7
\[\leadsto \sin th \cdot \frac{\sin ky}{\color{blue}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}} \cdot \sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}\]
Applied associate-/r*12.7
\[\leadsto \sin th \cdot \color{blue}{\frac{\frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}\]
Applied associate-*r/13.2
\[\leadsto \color{blue}{\frac{\sin th \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}\]
- Using strategy
rm Applied *-un-lft-identity13.2
\[\leadsto \frac{\sin th \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \color{blue}{1 \cdot \left(\sin ky \cdot \sin ky\right)}}}}\]
Applied *-un-lft-identity13.2
\[\leadsto \frac{\sin th \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\sqrt{\sqrt{\color{blue}{\left(1 \cdot \sin kx\right)} \cdot \sin kx + 1 \cdot \left(\sin ky \cdot \sin ky\right)}}}\]
Applied associate-*l*13.2
\[\leadsto \frac{\sin th \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\sqrt{\sqrt{\color{blue}{1 \cdot \left(\sin kx \cdot \sin kx\right)} + 1 \cdot \left(\sin ky \cdot \sin ky\right)}}}\]
Applied distribute-lft-out13.2
\[\leadsto \frac{\sin th \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\sqrt{\sqrt{\color{blue}{1 \cdot \left(\sin kx \cdot \sin kx + \sin ky \cdot \sin ky\right)}}}}\]
Applied sqrt-prod13.2
\[\leadsto \frac{\sin th \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\sqrt{\color{blue}{\sqrt{1} \cdot \sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}\]
Applied sqrt-prod13.2
\[\leadsto \frac{\sin th \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\color{blue}{\sqrt{\sqrt{1}} \cdot \sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}\]
Applied *-un-lft-identity13.2
\[\leadsto \frac{\color{blue}{\left(1 \cdot \sin th\right)} \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\sqrt{\sqrt{1}} \cdot \sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}\]
Applied associate-*l*13.2
\[\leadsto \frac{\color{blue}{1 \cdot \left(\sin th \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}\right)}}{\sqrt{\sqrt{1}} \cdot \sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}\]
Applied times-frac13.2
\[\leadsto \color{blue}{\frac{1}{\sqrt{\sqrt{1}}} \cdot \frac{\sin th \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}\]
Simplified13.2
\[\leadsto \color{blue}{1} \cdot \frac{\sin th \cdot \frac{\sin ky}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}}{\sqrt{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}\]
Simplified12.4
\[\leadsto 1 \cdot \color{blue}{\frac{\sin th}{\frac{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}{\sin ky}}}\]
Final simplification12.4
\[\leadsto \frac{\sin th}{\frac{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}{\sin ky}}\]
