Theorem lnopunilem2

Description: Lemma for lnopunii . (Contributed by NM, 12-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnopunilem.1	$$⊢T\in \mathrm{LinOp}$$
	lnopunilem.2	$$⊢\forall x\in \mathscr{H}{norm}_{ℎ}\left(T\left(x\right)\right)={norm}_{ℎ}\left(x\right)$$
	lnopunilem.3	$$⊢A\in \mathscr{H}$$
	lnopunilem.4	$$⊢B\in \mathscr{H}$$
Assertion	lnopunilem2	$$⊢T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)=A{\cdot }_{\mathrm{ih}}B$$

Proof

Step	Hyp	Ref	Expression
1		lnopunilem.1	$$⊢T\in \mathrm{LinOp}$$
2		lnopunilem.2	$$⊢\forall x\in \mathscr{H}{norm}_{ℎ}\left(T\left(x\right)\right)={norm}_{ℎ}\left(x\right)$$
3		lnopunilem.3	$$⊢A\in \mathscr{H}$$
4		lnopunilem.4	$$⊢B\in \mathscr{H}$$
5		fvoveq1	$$⊢y=if\left(y\in ℂ,y,0\right)\to \Re \left(y\left(T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\right)\right)=\Re \left(if\left(y\in ℂ,y,0\right)\left(T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\right)\right)$$
6		fvoveq1	$$⊢y=if\left(y\in ℂ,y,0\right)\to \Re \left(y\left(A{\cdot }_{\mathrm{ih}}B\right)\right)=\Re \left(if\left(y\in ℂ,y,0\right)\left(A{\cdot }_{\mathrm{ih}}B\right)\right)$$
7	5 6	eqeq12d	$$⊢y=if\left(y\in ℂ,y,0\right)\to \left(\Re \left(y\left(T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\right)\right)=\Re \left(y\left(A{\cdot }_{\mathrm{ih}}B\right)\right)\leftrightarrow \Re \left(if\left(y\in ℂ,y,0\right)\left(T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\right)\right)=\Re \left(if\left(y\in ℂ,y,0\right)\left(A{\cdot }_{\mathrm{ih}}B\right)\right)\right)$$
8		0cn	$$⊢0\in ℂ$$
9	8	elimel	$$⊢if\left(y\in ℂ,y,0\right)\in ℂ$$
10	1 2 3 4 9	lnopunilem1	$$⊢\Re \left(if\left(y\in ℂ,y,0\right)\left(T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\right)\right)=\Re \left(if\left(y\in ℂ,y,0\right)\left(A{\cdot }_{\mathrm{ih}}B\right)\right)$$
11	7 10	dedth	$$⊢y\in ℂ\to \Re \left(y\left(T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\right)\right)=\Re \left(y\left(A{\cdot }_{\mathrm{ih}}B\right)\right)$$
12	11	rgen	$$⊢\forall y\in ℂ\Re \left(y\left(T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\right)\right)=\Re \left(y\left(A{\cdot }_{\mathrm{ih}}B\right)\right)$$
13	1	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
14	13	ffvelrni	$$⊢A\in \mathscr{H}\to T\left(A\right)\in \mathscr{H}$$
15	3 14	ax-mp	$$⊢T\left(A\right)\in \mathscr{H}$$
16	13	ffvelrni	$$⊢B\in \mathscr{H}\to T\left(B\right)\in \mathscr{H}$$
17	4 16	ax-mp	$$⊢T\left(B\right)\in \mathscr{H}$$
18	15 17	hicli	$$⊢T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\in ℂ$$
19	3 4	hicli	$$⊢A{\cdot }_{\mathrm{ih}}B\in ℂ$$
20		recan	$$⊢\left(T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\in ℂ\wedge A{\cdot }_{\mathrm{ih}}B\in ℂ\right)\to \left(\forall y\in ℂ\Re \left(y\left(T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\right)\right)=\Re \left(y\left(A{\cdot }_{\mathrm{ih}}B\right)\right)\leftrightarrow T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)=A{\cdot }_{\mathrm{ih}}B\right)$$
21	18 19 20	mp2an	$$⊢\forall y\in ℂ\Re \left(y\left(T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)\right)\right)=\Re \left(y\left(A{\cdot }_{\mathrm{ih}}B\right)\right)\leftrightarrow T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)=A{\cdot }_{\mathrm{ih}}B$$
22	12 21	mpbi	$$⊢T\left(A\right){\cdot }_{\mathrm{ih}}T\left(B\right)=A{\cdot }_{\mathrm{ih}}B$$