Metamath Proof Explorer

Theorem lnopunilem1

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

Ref Expression
Hypotheses lnopunilem.1 ⊢T∈LinOp
lnopunilem.2 ⊢∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x
lnopunilem.3 ⊢A∈ℋ
lnopunilem.4 ⊢B∈ℋ
lnopunilem1.5 ⊢C∈ℂ
Assertion lnopunilem1 ⊢ℜ⁡C⁢T⁡A⋅ihT⁡B=ℜ⁡C⁢A⋅ihB

Proof

Step Hyp Ref Expression
1 lnopunilem.1 ⊢T∈LinOp
2 lnopunilem.2 ⊢∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x
3 lnopunilem.3 ⊢A∈ℋ
4 lnopunilem.4 ⊢B∈ℋ
5 lnopunilem1.5 ⊢C∈ℂ
6 1 lnopfi ⊢T:ℋ⟶ℋ
7 6 ffvelcdmi ⊢A∈ℋ→T⁡A∈ℋ
8 3 7 ax-mp ⊢T⁡A∈ℋ
9 6 ffvelcdmi ⊢B∈ℋ→T⁡B∈ℋ
10 4 9 ax-mp ⊢T⁡B∈ℋ
11 8 10 hicli ⊢T⁡A⋅ihT⁡B∈ℂ
12 5 11 mulcli ⊢C⁢T⁡A⋅ihT⁡B∈ℂ
13 reval ⊢C⁢T⁡A⋅ihT⁡B∈ℂ→ℜ⁡C⁢T⁡A⋅ihT⁡B=C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾2
14 12 13 ax-mp ⊢ℜ⁡C⁢T⁡A⋅ihT⁡B=C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾2
15 3 4 hicli ⊢A⋅ihB∈ℂ
16 5 15 mulcli ⊢C⁢A⋅ihB∈ℂ
17 reval ⊢C⁢A⋅ihB∈ℂ→ℜ⁡C⁢A⋅ihB=C⁢A⋅ihB+C⁢A⋅ihB‾2
18 16 17 ax-mp ⊢ℜ⁡C⁢A⋅ihB=C⁢A⋅ihB+C⁢A⋅ihB‾2
19 2fveq3 ⊢x=y→normℎ⁡T⁡x=normℎ⁡T⁡y
20 fveq2 ⊢x=y→normℎ⁡x=normℎ⁡y
21 19 20 eqeq12d ⊢x=y→normℎ⁡T⁡x=normℎ⁡x↔normℎ⁡T⁡y=normℎ⁡y
22 21 cbvralvw ⊢∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x↔∀y∈ℋnormℎ⁡T⁡y=normℎ⁡y
23 2 22 mpbi ⊢∀y∈ℋnormℎ⁡T⁡y=normℎ⁡y
24 oveq1 ⊢normℎ⁡T⁡y=normℎ⁡y→normℎ⁡T⁡y2=normℎ⁡y2
25 6 ffvelcdmi ⊢y∈ℋ→T⁡y∈ℋ
26 normsq ⊢T⁡y∈ℋ→normℎ⁡T⁡y2=T⁡y⋅ihT⁡y
27 25 26 syl ⊢y∈ℋ→normℎ⁡T⁡y2=T⁡y⋅ihT⁡y
28 normsq ⊢y∈ℋ→normℎ⁡y2=y⋅ihy
29 27 28 eqeq12d ⊢y∈ℋ→normℎ⁡T⁡y2=normℎ⁡y2↔T⁡y⋅ihT⁡y=y⋅ihy
30 24 29 imbitrid ⊢y∈ℋ→normℎ⁡T⁡y=normℎ⁡y→T⁡y⋅ihT⁡y=y⋅ihy
31 30 ralimia ⊢∀y∈ℋnormℎ⁡T⁡y=normℎ⁡y→∀y∈ℋT⁡y⋅ihT⁡y=y⋅ihy
32 23 31 ax-mp ⊢∀y∈ℋT⁡y⋅ihT⁡y=y⋅ihy
33 fveq2 ⊢y=A→T⁡y=T⁡A
34 33 33 oveq12d ⊢y=A→T⁡y⋅ihT⁡y=T⁡A⋅ihT⁡A
35 id ⊢y=A→y=A
36 35 35 oveq12d ⊢y=A→y⋅ihy=A⋅ihA
37 34 36 eqeq12d ⊢y=A→T⁡y⋅ihT⁡y=y⋅ihy↔T⁡A⋅ihT⁡A=A⋅ihA
38 37 rspcv ⊢A∈ℋ→∀y∈ℋT⁡y⋅ihT⁡y=y⋅ihy→T⁡A⋅ihT⁡A=A⋅ihA
39 3 32 38 mp2 ⊢T⁡A⋅ihT⁡A=A⋅ihA
40 39 oveq2i ⊢C‾⁢T⁡A⋅ihT⁡A=C‾⁢A⋅ihA
41 40 oveq2i ⊢C⁢C‾⁢T⁡A⋅ihT⁡A=C⁢C‾⁢A⋅ihA
42 fveq2 ⊢y=B→T⁡y=T⁡B
43 42 42 oveq12d ⊢y=B→T⁡y⋅ihT⁡y=T⁡B⋅ihT⁡B
44 id ⊢y=B→y=B
45 44 44 oveq12d ⊢y=B→y⋅ihy=B⋅ihB
46 43 45 eqeq12d ⊢y=B→T⁡y⋅ihT⁡y=y⋅ihy↔T⁡B⋅ihT⁡B=B⋅ihB
47 46 rspcv ⊢B∈ℋ→∀y∈ℋT⁡y⋅ihT⁡y=y⋅ihy→T⁡B⋅ihT⁡B=B⋅ihB
48 4 32 47 mp2 ⊢T⁡B⋅ihT⁡B=B⋅ihB
49 41 48 oveq12i ⊢C⁢C‾⁢T⁡A⋅ihT⁡A+T⁡B⋅ihT⁡B=C⁢C‾⁢A⋅ihA+B⋅ihB
50 49 oveq1i ⊢C⁢C‾⁢T⁡A⋅ihT⁡A+T⁡B⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾=C⁢C‾⁢A⋅ihA+B⋅ihB+C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾
51 5 cjcli ⊢C‾∈ℂ
52 8 8 hicli ⊢T⁡A⋅ihT⁡A∈ℂ
53 51 52 mulcli ⊢C‾⁢T⁡A⋅ihT⁡A∈ℂ
54 5 53 mulcli ⊢C⁢C‾⁢T⁡A⋅ihT⁡A∈ℂ
55 10 10 hicli ⊢T⁡B⋅ihT⁡B∈ℂ
56 12 cjcli ⊢C⁢T⁡A⋅ihT⁡B‾∈ℂ
57 54 55 12 56 add42i ⊢C⁢C‾⁢T⁡A⋅ihT⁡A+T⁡B⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾=C⁢C‾⁢T⁡A⋅ihT⁡A+C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾+T⁡B⋅ihT⁡B
58 3 3 hicli ⊢A⋅ihA∈ℂ
59 51 58 mulcli ⊢C‾⁢A⋅ihA∈ℂ
60 5 59 mulcli ⊢C⁢C‾⁢A⋅ihA∈ℂ
61 4 4 hicli ⊢B⋅ihB∈ℂ
62 16 cjcli ⊢C⁢A⋅ihB‾∈ℂ
63 60 61 16 62 add42i ⊢C⁢C‾⁢A⋅ihA+B⋅ihB+C⁢A⋅ihB+C⁢A⋅ihB‾=C⁢C‾⁢A⋅ihA+C⁢A⋅ihB+C⁢A⋅ihB‾+B⋅ihB
64 5 3 hvmulcli ⊢C⋅ℎA∈ℋ
65 64 4 hvaddcli ⊢C⋅ℎA+ℎB∈ℋ
66 fveq2 ⊢y=C⋅ℎA+ℎB→T⁡y=T⁡C⋅ℎA+ℎB
67 66 66 oveq12d ⊢y=C⋅ℎA+ℎB→T⁡y⋅ihT⁡y=T⁡C⋅ℎA+ℎB⋅ihT⁡C⋅ℎA+ℎB
68 id ⊢y=C⋅ℎA+ℎB→y=C⋅ℎA+ℎB
69 68 68 oveq12d ⊢y=C⋅ℎA+ℎB→y⋅ihy=C⋅ℎA+ℎB⋅ihC⋅ℎA+ℎB
70 67 69 eqeq12d ⊢y=C⋅ℎA+ℎB→T⁡y⋅ihT⁡y=y⋅ihy↔T⁡C⋅ℎA+ℎB⋅ihT⁡C⋅ℎA+ℎB=C⋅ℎA+ℎB⋅ihC⋅ℎA+ℎB
71 70 rspcv ⊢C⋅ℎA+ℎB∈ℋ→∀y∈ℋT⁡y⋅ihT⁡y=y⋅ihy→T⁡C⋅ℎA+ℎB⋅ihT⁡C⋅ℎA+ℎB=C⋅ℎA+ℎB⋅ihC⋅ℎA+ℎB
72 65 32 71 mp2 ⊢T⁡C⋅ℎA+ℎB⋅ihT⁡C⋅ℎA+ℎB=C⋅ℎA+ℎB⋅ihC⋅ℎA+ℎB
73 ax-his2 ⊢C⋅ℎA∈ℋ∧B∈ℋ∧C⋅ℎA+ℎB∈ℋ→C⋅ℎA+ℎB⋅ihC⋅ℎA+ℎB=C⋅ℎA⋅ihC⋅ℎA+ℎB+B⋅ihC⋅ℎA+ℎB
74 64 4 65 73 mp3an ⊢C⋅ℎA+ℎB⋅ihC⋅ℎA+ℎB=C⋅ℎA⋅ihC⋅ℎA+ℎB+B⋅ihC⋅ℎA+ℎB
75 ax-his3 ⊢C∈ℂ∧A∈ℋ∧C⋅ℎA+ℎB∈ℋ→C⋅ℎA⋅ihC⋅ℎA+ℎB=C⁢A⋅ihC⋅ℎA+ℎB
76 5 3 65 75 mp3an ⊢C⋅ℎA⋅ihC⋅ℎA+ℎB=C⁢A⋅ihC⋅ℎA+ℎB
77 his7 ⊢A∈ℋ∧C⋅ℎA∈ℋ∧B∈ℋ→A⋅ihC⋅ℎA+ℎB=A⋅ihC⋅ℎA+A⋅ihB
78 3 64 4 77 mp3an ⊢A⋅ihC⋅ℎA+ℎB=A⋅ihC⋅ℎA+A⋅ihB
79 his5 ⊢C∈ℂ∧A∈ℋ∧A∈ℋ→A⋅ihC⋅ℎA=C‾⁢A⋅ihA
80 5 3 3 79 mp3an ⊢A⋅ihC⋅ℎA=C‾⁢A⋅ihA
81 80 oveq1i ⊢A⋅ihC⋅ℎA+A⋅ihB=C‾⁢A⋅ihA+A⋅ihB
82 78 81 eqtri ⊢A⋅ihC⋅ℎA+ℎB=C‾⁢A⋅ihA+A⋅ihB
83 82 oveq2i ⊢C⁢A⋅ihC⋅ℎA+ℎB=C⁢C‾⁢A⋅ihA+A⋅ihB
84 5 59 15 adddii ⊢C⁢C‾⁢A⋅ihA+A⋅ihB=C⁢C‾⁢A⋅ihA+C⁢A⋅ihB
85 76 83 84 3eqtri ⊢C⋅ℎA⋅ihC⋅ℎA+ℎB=C⁢C‾⁢A⋅ihA+C⁢A⋅ihB
86 his7 ⊢B∈ℋ∧C⋅ℎA∈ℋ∧B∈ℋ→B⋅ihC⋅ℎA+ℎB=B⋅ihC⋅ℎA+B⋅ihB
87 4 64 4 86 mp3an ⊢B⋅ihC⋅ℎA+ℎB=B⋅ihC⋅ℎA+B⋅ihB
88 his5 ⊢C∈ℂ∧B∈ℋ∧A∈ℋ→B⋅ihC⋅ℎA=C‾⁢B⋅ihA
89 5 4 3 88 mp3an ⊢B⋅ihC⋅ℎA=C‾⁢B⋅ihA
90 5 15 cjmuli ⊢C⁢A⋅ihB‾=C‾⁢A⋅ihB‾
91 4 3 his1i ⊢B⋅ihA=A⋅ihB‾
92 91 oveq2i ⊢C‾⁢B⋅ihA=C‾⁢A⋅ihB‾
93 90 92 eqtr4i ⊢C⁢A⋅ihB‾=C‾⁢B⋅ihA
94 89 93 eqtr4i ⊢B⋅ihC⋅ℎA=C⁢A⋅ihB‾
95 94 oveq1i ⊢B⋅ihC⋅ℎA+B⋅ihB=C⁢A⋅ihB‾+B⋅ihB
96 87 95 eqtri ⊢B⋅ihC⋅ℎA+ℎB=C⁢A⋅ihB‾+B⋅ihB
97 85 96 oveq12i ⊢C⋅ℎA⋅ihC⋅ℎA+ℎB+B⋅ihC⋅ℎA+ℎB=C⁢C‾⁢A⋅ihA+C⁢A⋅ihB+C⁢A⋅ihB‾+B⋅ihB
98 72 74 97 3eqtrri ⊢C⁢C‾⁢A⋅ihA+C⁢A⋅ihB+C⁢A⋅ihB‾+B⋅ihB=T⁡C⋅ℎA+ℎB⋅ihT⁡C⋅ℎA+ℎB
99 1 lnopli ⊢C∈ℂ∧A∈ℋ∧B∈ℋ→T⁡C⋅ℎA+ℎB=C⋅ℎT⁡A+ℎT⁡B
100 5 3 4 99 mp3an ⊢T⁡C⋅ℎA+ℎB=C⋅ℎT⁡A+ℎT⁡B
101 100 100 oveq12i ⊢T⁡C⋅ℎA+ℎB⋅ihT⁡C⋅ℎA+ℎB=C⋅ℎT⁡A+ℎT⁡B⋅ihC⋅ℎT⁡A+ℎT⁡B
102 5 8 hvmulcli ⊢C⋅ℎT⁡A∈ℋ
103 102 10 hvaddcli ⊢C⋅ℎT⁡A+ℎT⁡B∈ℋ
104 ax-his2 ⊢C⋅ℎT⁡A∈ℋ∧T⁡B∈ℋ∧C⋅ℎT⁡A+ℎT⁡B∈ℋ→C⋅ℎT⁡A+ℎT⁡B⋅ihC⋅ℎT⁡A+ℎT⁡B=C⋅ℎT⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B+T⁡B⋅ihC⋅ℎT⁡A+ℎT⁡B
105 102 10 103 104 mp3an ⊢C⋅ℎT⁡A+ℎT⁡B⋅ihC⋅ℎT⁡A+ℎT⁡B=C⋅ℎT⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B+T⁡B⋅ihC⋅ℎT⁡A+ℎT⁡B
106 101 105 eqtri ⊢T⁡C⋅ℎA+ℎB⋅ihT⁡C⋅ℎA+ℎB=C⋅ℎT⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B+T⁡B⋅ihC⋅ℎT⁡A+ℎT⁡B
107 ax-his3 ⊢C∈ℂ∧T⁡A∈ℋ∧C⋅ℎT⁡A+ℎT⁡B∈ℋ→C⋅ℎT⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B=C⁢T⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B
108 5 8 103 107 mp3an ⊢C⋅ℎT⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B=C⁢T⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B
109 his7 ⊢T⁡A∈ℋ∧C⋅ℎT⁡A∈ℋ∧T⁡B∈ℋ→T⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B=T⁡A⋅ihC⋅ℎT⁡A+T⁡A⋅ihT⁡B
110 8 102 10 109 mp3an ⊢T⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B=T⁡A⋅ihC⋅ℎT⁡A+T⁡A⋅ihT⁡B
111 his5 ⊢C∈ℂ∧T⁡A∈ℋ∧T⁡A∈ℋ→T⁡A⋅ihC⋅ℎT⁡A=C‾⁢T⁡A⋅ihT⁡A
112 5 8 8 111 mp3an ⊢T⁡A⋅ihC⋅ℎT⁡A=C‾⁢T⁡A⋅ihT⁡A
113 112 oveq1i ⊢T⁡A⋅ihC⋅ℎT⁡A+T⁡A⋅ihT⁡B=C‾⁢T⁡A⋅ihT⁡A+T⁡A⋅ihT⁡B
114 110 113 eqtri ⊢T⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B=C‾⁢T⁡A⋅ihT⁡A+T⁡A⋅ihT⁡B
115 114 oveq2i ⊢C⁢T⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B=C⁢C‾⁢T⁡A⋅ihT⁡A+T⁡A⋅ihT⁡B
116 5 53 11 adddii ⊢C⁢C‾⁢T⁡A⋅ihT⁡A+T⁡A⋅ihT⁡B=C⁢C‾⁢T⁡A⋅ihT⁡A+C⁢T⁡A⋅ihT⁡B
117 108 115 116 3eqtri ⊢C⋅ℎT⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B=C⁢C‾⁢T⁡A⋅ihT⁡A+C⁢T⁡A⋅ihT⁡B
118 his7 ⊢T⁡B∈ℋ∧C⋅ℎT⁡A∈ℋ∧T⁡B∈ℋ→T⁡B⋅ihC⋅ℎT⁡A+ℎT⁡B=T⁡B⋅ihC⋅ℎT⁡A+T⁡B⋅ihT⁡B
119 10 102 10 118 mp3an ⊢T⁡B⋅ihC⋅ℎT⁡A+ℎT⁡B=T⁡B⋅ihC⋅ℎT⁡A+T⁡B⋅ihT⁡B
120 his5 ⊢C∈ℂ∧T⁡B∈ℋ∧T⁡A∈ℋ→T⁡B⋅ihC⋅ℎT⁡A=C‾⁢T⁡B⋅ihT⁡A
121 5 10 8 120 mp3an ⊢T⁡B⋅ihC⋅ℎT⁡A=C‾⁢T⁡B⋅ihT⁡A
122 5 11 cjmuli ⊢C⁢T⁡A⋅ihT⁡B‾=C‾⁢T⁡A⋅ihT⁡B‾
123 10 8 his1i ⊢T⁡B⋅ihT⁡A=T⁡A⋅ihT⁡B‾
124 123 oveq2i ⊢C‾⁢T⁡B⋅ihT⁡A=C‾⁢T⁡A⋅ihT⁡B‾
125 122 124 eqtr4i ⊢C⁢T⁡A⋅ihT⁡B‾=C‾⁢T⁡B⋅ihT⁡A
126 121 125 eqtr4i ⊢T⁡B⋅ihC⋅ℎT⁡A=C⁢T⁡A⋅ihT⁡B‾
127 126 oveq1i ⊢T⁡B⋅ihC⋅ℎT⁡A+T⁡B⋅ihT⁡B=C⁢T⁡A⋅ihT⁡B‾+T⁡B⋅ihT⁡B
128 119 127 eqtri ⊢T⁡B⋅ihC⋅ℎT⁡A+ℎT⁡B=C⁢T⁡A⋅ihT⁡B‾+T⁡B⋅ihT⁡B
129 117 128 oveq12i ⊢C⋅ℎT⁡A⋅ihC⋅ℎT⁡A+ℎT⁡B+T⁡B⋅ihC⋅ℎT⁡A+ℎT⁡B=C⁢C‾⁢T⁡A⋅ihT⁡A+C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾+T⁡B⋅ihT⁡B
130 98 106 129 3eqtrri ⊢C⁢C‾⁢T⁡A⋅ihT⁡A+C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾+T⁡B⋅ihT⁡B=C⁢C‾⁢A⋅ihA+C⁢A⋅ihB+C⁢A⋅ihB‾+B⋅ihB
131 63 130 eqtr4i ⊢C⁢C‾⁢A⋅ihA+B⋅ihB+C⁢A⋅ihB+C⁢A⋅ihB‾=C⁢C‾⁢T⁡A⋅ihT⁡A+C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾+T⁡B⋅ihT⁡B
132 57 131 eqtr4i ⊢C⁢C‾⁢T⁡A⋅ihT⁡A+T⁡B⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾=C⁢C‾⁢A⋅ihA+B⋅ihB+C⁢A⋅ihB+C⁢A⋅ihB‾
133 50 132 eqtr3i ⊢C⁢C‾⁢A⋅ihA+B⋅ihB+C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾=C⁢C‾⁢A⋅ihA+B⋅ihB+C⁢A⋅ihB+C⁢A⋅ihB‾
134 60 61 addcli ⊢C⁢C‾⁢A⋅ihA+B⋅ihB∈ℂ
135 12 56 addcli ⊢C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾∈ℂ
136 16 62 addcli ⊢C⁢A⋅ihB+C⁢A⋅ihB‾∈ℂ
137 134 135 136 addcani ⊢C⁢C‾⁢A⋅ihA+B⋅ihB+C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾=C⁢C‾⁢A⋅ihA+B⋅ihB+C⁢A⋅ihB+C⁢A⋅ihB‾↔C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾=C⁢A⋅ihB+C⁢A⋅ihB‾
138 133 137 mpbi ⊢C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾=C⁢A⋅ihB+C⁢A⋅ihB‾
139 138 oveq1i ⊢C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾2=C⁢A⋅ihB+C⁢A⋅ihB‾2
140 18 139 eqtr4i ⊢ℜ⁡C⁢A⋅ihB=C⁢T⁡A⋅ihT⁡B+C⁢T⁡A⋅ihT⁡B‾2
141 14 140 eqtr4i ⊢ℜ⁡C⁢T⁡A⋅ihT⁡B=ℜ⁡C⁢A⋅ihB