Theorem normsq

Description: The square of a norm. (Contributed by NM, 12-May-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	normsq	$$⊢A\in \mathscr{H}\to {{norm}_{ℎ}\left(A\right)}^2=A{\cdot }_{\mathrm{ih}}A$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {norm}_{ℎ}\left(A\right)={norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
2	1	oveq1d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {{norm}_{ℎ}\left(A\right)}^2={{norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)}^2$$
3		id	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)$$
4	3 3	oveq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to A{\cdot }_{\mathrm{ih}}A=if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)$$
5	2 4	eqeq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left({{norm}_{ℎ}\left(A\right)}^2=A{\cdot }_{\mathrm{ih}}A\leftrightarrow {{norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)}^2=if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
6		ifhvhv0	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \mathscr{H}$$
7	6	normsqi	$$⊢{{norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)}^2=if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}if\left(A\in \mathscr{H},A,0_{ℎ}\right)$$
8	5 7	dedth	$$⊢A\in \mathscr{H}\to {{norm}_{ℎ}\left(A\right)}^2=A{\cdot }_{\mathrm{ih}}A$$