Metamath Proof Explorer

Theorem ipdirilem

Description: Lemma for ipdiri . (Contributed by NM, 26-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 ⊢ X = BaseSet ⁡ U
ip1i.2 ⊢ G = + v ⁡ U
ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
ip1i.9 ⊢ U ∈ CPreHil OLD
ipdiri.8 ⊢ A ∈ X
ipdiri.9 ⊢ B ∈ X
ipdiri.10 ⊢ C ∈ X
Assertion ipdirilem ⊢ A G B P C = A P C + B P C

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ X = BaseSet ⁡ U
2 ip1i.2 ⊢ G = + v ⁡ U
3 ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
5 ip1i.9 ⊢ U ∈ CPreHil OLD
6 ipdiri.8 ⊢ A ∈ X
7 ipdiri.9 ⊢ B ∈ X
8 ipdiri.10 ⊢ C ∈ X
9 2thalfe1 ⊢ 2 ⁢ 1 2 = 1
10 9 oveq1i ⊢ 2 ⁢ 1 2 S A G B = 1 S A G B
11 5 phnvi ⊢ U ∈ NrmCVec
12 2cn ⊢ 2 ∈ ℂ
13 halfcn ⊢ 1 2 ∈ ℂ
14 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B ∈ X
15 11 6 7 14 mp3an ⊢ A G B ∈ X
16 12 13 15 3pm3.2i ⊢ 2 ∈ ℂ ∧ 1 2 ∈ ℂ ∧ A G B ∈ X
17 1 3 nvsass ⊢ U ∈ NrmCVec ∧ 2 ∈ ℂ ∧ 1 2 ∈ ℂ ∧ A G B ∈ X → 2 ⁢ 1 2 S A G B = 2 S 1 2 S A G B
18 11 16 17 mp2an ⊢ 2 ⁢ 1 2 S A G B = 2 S 1 2 S A G B
19 1 3 nvsid ⊢ U ∈ NrmCVec ∧ A G B ∈ X → 1 S A G B = A G B
20 11 15 19 mp2an ⊢ 1 S A G B = A G B
21 10 18 20 3eqtr3i ⊢ 2 S 1 2 S A G B = A G B
22 21 oveq1i ⊢ 2 S 1 2 S A G B P C = A G B P C
23 1 3 nvscl ⊢ U ∈ NrmCVec ∧ 1 2 ∈ ℂ ∧ A G B ∈ X → 1 2 S A G B ∈ X
24 11 13 15 23 mp3an ⊢ 1 2 S A G B ∈ X
25 1 2 3 4 5 24 8 ip2i ⊢ 2 S 1 2 S A G B P C = 2 ⁢ 1 2 S A G B P C
26 22 25 eqtr3i ⊢ A G B P C = 2 ⁢ 1 2 S A G B P C
27 neg1cn ⊢ − 1 ∈ ℂ
28 1 3 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ B ∈ X → -1 S B ∈ X
29 11 27 7 28 mp3an ⊢ -1 S B ∈ X
30 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ -1 S B ∈ X → A G -1 S B ∈ X
31 11 6 29 30 mp3an ⊢ A G -1 S B ∈ X
32 1 3 nvscl ⊢ U ∈ NrmCVec ∧ 1 2 ∈ ℂ ∧ A G -1 S B ∈ X → 1 2 S A G -1 S B ∈ X
33 11 13 31 32 mp3an ⊢ 1 2 S A G -1 S B ∈ X
34 1 2 3 4 5 24 33 8 ip1i ⊢ 1 2 S A G B G 1 2 S A G -1 S B P C + 1 2 S A G B G -1 S 1 2 S A G -1 S B P C = 2 ⁢ 1 2 S A G B P C
35 eqid ⊢ 1 st ⁡ U = 1 st ⁡ U
36 35 nvvc ⊢ U ∈ NrmCVec → 1 st ⁡ U ∈ CVec OLD
37 11 36 ax-mp ⊢ 1 st ⁡ U ∈ CVec OLD
38 2 vafval ⊢ G = 1 st ⁡ 1 st ⁡ U
39 38 vcablo ⊢ 1 st ⁡ U ∈ CVec OLD → G ∈ AbelOp
40 37 39 ax-mp ⊢ G ∈ AbelOp
41 6 7 pm3.2i ⊢ A ∈ X ∧ B ∈ X
42 6 29 pm3.2i ⊢ A ∈ X ∧ -1 S B ∈ X
43 1 2 bafval ⊢ X = ran ⁡ G
44 43 ablo4 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ A ∈ X ∧ -1 S B ∈ X → A G B G A G -1 S B = A G A G B G -1 S B
45 40 41 42 44 mp3an ⊢ A G B G A G -1 S B = A G A G B G -1 S B
46 3 smfval ⊢ S = 2 nd ⁡ 1 st ⁡ U
47 38 46 43 vc2OLD ⊢ 1 st ⁡ U ∈ CVec OLD ∧ A ∈ X → A G A = 2 S A
48 37 6 47 mp2an ⊢ A G A = 2 S A
49 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
50 1 2 3 49 nvrinv ⊢ U ∈ NrmCVec ∧ B ∈ X → B G -1 S B = 0 vec ⁡ U
51 11 7 50 mp2an ⊢ B G -1 S B = 0 vec ⁡ U
52 48 51 oveq12i ⊢ A G A G B G -1 S B = 2 S A G 0 vec ⁡ U
53 1 3 nvscl ⊢ U ∈ NrmCVec ∧ 2 ∈ ℂ ∧ A ∈ X → 2 S A ∈ X
54 11 12 6 53 mp3an ⊢ 2 S A ∈ X
55 1 2 49 nv0rid ⊢ U ∈ NrmCVec ∧ 2 S A ∈ X → 2 S A G 0 vec ⁡ U = 2 S A
56 11 54 55 mp2an ⊢ 2 S A G 0 vec ⁡ U = 2 S A
57 45 52 56 3eqtri ⊢ A G B G A G -1 S B = 2 S A
58 57 oveq2i ⊢ 1 2 S A G B G A G -1 S B = 1 2 S 2 S A
59 13 12 6 3pm3.2i ⊢ 1 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ A ∈ X
60 1 3 nvsass ⊢ U ∈ NrmCVec ∧ 1 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ A ∈ X → 1 2 ⋅ 2 S A = 1 2 S 2 S A
61 11 59 60 mp2an ⊢ 1 2 ⋅ 2 S A = 1 2 S 2 S A
62 58 61 eqtr4i ⊢ 1 2 S A G B G A G -1 S B = 1 2 ⋅ 2 S A
63 13 15 31 3pm3.2i ⊢ 1 2 ∈ ℂ ∧ A G B ∈ X ∧ A G -1 S B ∈ X
64 1 2 3 nvdi ⊢ U ∈ NrmCVec ∧ 1 2 ∈ ℂ ∧ A G B ∈ X ∧ A G -1 S B ∈ X → 1 2 S A G B G A G -1 S B = 1 2 S A G B G 1 2 S A G -1 S B
65 11 63 64 mp2an ⊢ 1 2 S A G B G A G -1 S B = 1 2 S A G B G 1 2 S A G -1 S B
66 ax-1cn ⊢ 1 ∈ ℂ
67 2ne0 ⊢ 2 ≠ 0
68 66 12 67 divcan1i ⊢ 1 2 ⋅ 2 = 1
69 68 oveq1i ⊢ 1 2 ⋅ 2 S A = 1 S A
70 1 3 nvsid ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 S A = A
71 11 6 70 mp2an ⊢ 1 S A = A
72 69 71 eqtri ⊢ 1 2 ⋅ 2 S A = A
73 62 65 72 3eqtr3i ⊢ 1 2 S A G B G 1 2 S A G -1 S B = A
74 73 oveq1i ⊢ 1 2 S A G B G 1 2 S A G -1 S B P C = A P C
75 27 13 mulcomi ⊢ -1 ⁢ 1 2 = 1 2 ⁢ -1
76 75 oveq1i ⊢ -1 ⁢ 1 2 S A G -1 S B = 1 2 ⁢ -1 S A G -1 S B
77 27 13 31 3pm3.2i ⊢ − 1 ∈ ℂ ∧ 1 2 ∈ ℂ ∧ A G -1 S B ∈ X
78 1 3 nvsass ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ 1 2 ∈ ℂ ∧ A G -1 S B ∈ X → -1 ⁢ 1 2 S A G -1 S B = -1 S 1 2 S A G -1 S B
79 11 77 78 mp2an ⊢ -1 ⁢ 1 2 S A G -1 S B = -1 S 1 2 S A G -1 S B
80 13 27 31 3pm3.2i ⊢ 1 2 ∈ ℂ ∧ − 1 ∈ ℂ ∧ A G -1 S B ∈ X
81 1 3 nvsass ⊢ U ∈ NrmCVec ∧ 1 2 ∈ ℂ ∧ − 1 ∈ ℂ ∧ A G -1 S B ∈ X → 1 2 ⁢ -1 S A G -1 S B = 1 2 S -1 S A G -1 S B
82 11 80 81 mp2an ⊢ 1 2 ⁢ -1 S A G -1 S B = 1 2 S -1 S A G -1 S B
83 27 6 29 3pm3.2i ⊢ − 1 ∈ ℂ ∧ A ∈ X ∧ -1 S B ∈ X
84 1 2 3 nvdi ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ A ∈ X ∧ -1 S B ∈ X → -1 S A G -1 S B = -1 S A G -1 S -1 S B
85 11 83 84 mp2an ⊢ -1 S A G -1 S B = -1 S A G -1 S -1 S B
86 neg1mulneg1e1 ⊢ -1 ⁢ -1 = 1
87 86 oveq1i ⊢ -1 ⁢ -1 S B = 1 S B
88 27 27 7 3pm3.2i ⊢ − 1 ∈ ℂ ∧ − 1 ∈ ℂ ∧ B ∈ X
89 1 3 nvsass ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ − 1 ∈ ℂ ∧ B ∈ X → -1 ⁢ -1 S B = -1 S -1 S B
90 11 88 89 mp2an ⊢ -1 ⁢ -1 S B = -1 S -1 S B
91 1 3 nvsid ⊢ U ∈ NrmCVec ∧ B ∈ X → 1 S B = B
92 11 7 91 mp2an ⊢ 1 S B = B
93 87 90 92 3eqtr3i ⊢ -1 S -1 S B = B
94 93 oveq2i ⊢ -1 S A G -1 S -1 S B = -1 S A G B
95 85 94 eqtri ⊢ -1 S A G -1 S B = -1 S A G B
96 95 oveq2i ⊢ 1 2 S -1 S A G -1 S B = 1 2 S -1 S A G B
97 82 96 eqtri ⊢ 1 2 ⁢ -1 S A G -1 S B = 1 2 S -1 S A G B
98 76 79 97 3eqtr3i ⊢ -1 S 1 2 S A G -1 S B = 1 2 S -1 S A G B
99 98 oveq2i ⊢ 1 2 S A G B G -1 S 1 2 S A G -1 S B = 1 2 S A G B G 1 2 S -1 S A G B
100 1 3 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ A ∈ X → -1 S A ∈ X
101 11 27 6 100 mp3an ⊢ -1 S A ∈ X
102 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ -1 S A ∈ X ∧ B ∈ X → -1 S A G B ∈ X
103 11 101 7 102 mp3an ⊢ -1 S A G B ∈ X
104 13 15 103 3pm3.2i ⊢ 1 2 ∈ ℂ ∧ A G B ∈ X ∧ -1 S A G B ∈ X
105 1 2 3 nvdi ⊢ U ∈ NrmCVec ∧ 1 2 ∈ ℂ ∧ A G B ∈ X ∧ -1 S A G B ∈ X → 1 2 S A G B G -1 S A G B = 1 2 S A G B G 1 2 S -1 S A G B
106 11 104 105 mp2an ⊢ 1 2 S A G B G -1 S A G B = 1 2 S A G B G 1 2 S -1 S A G B
107 99 106 eqtr4i ⊢ 1 2 S A G B G -1 S 1 2 S A G -1 S B = 1 2 S A G B G -1 S A G B
108 101 7 pm3.2i ⊢ -1 S A ∈ X ∧ B ∈ X
109 43 ablo4 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ -1 S A ∈ X ∧ B ∈ X → A G B G -1 S A G B = A G -1 S A G B G B
110 40 41 108 109 mp3an ⊢ A G B G -1 S A G B = A G -1 S A G B G B
111 1 2 3 49 nvrinv ⊢ U ∈ NrmCVec ∧ A ∈ X → A G -1 S A = 0 vec ⁡ U
112 11 6 111 mp2an ⊢ A G -1 S A = 0 vec ⁡ U
113 112 oveq1i ⊢ A G -1 S A G B G B = 0 vec ⁡ U G B G B
114 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ B ∈ X → B G B ∈ X
115 11 7 7 114 mp3an ⊢ B G B ∈ X
116 1 2 49 nv0lid ⊢ U ∈ NrmCVec ∧ B G B ∈ X → 0 vec ⁡ U G B G B = B G B
117 11 115 116 mp2an ⊢ 0 vec ⁡ U G B G B = B G B
118 113 117 eqtri ⊢ A G -1 S A G B G B = B G B
119 38 46 43 vc2OLD ⊢ 1 st ⁡ U ∈ CVec OLD ∧ B ∈ X → B G B = 2 S B
120 37 7 119 mp2an ⊢ B G B = 2 S B
121 110 118 120 3eqtri ⊢ A G B G -1 S A G B = 2 S B
122 121 oveq2i ⊢ 1 2 S A G B G -1 S A G B = 1 2 S 2 S B
123 13 12 7 3pm3.2i ⊢ 1 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ B ∈ X
124 1 3 nvsass ⊢ U ∈ NrmCVec ∧ 1 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ B ∈ X → 1 2 ⋅ 2 S B = 1 2 S 2 S B
125 11 123 124 mp2an ⊢ 1 2 ⋅ 2 S B = 1 2 S 2 S B
126 68 oveq1i ⊢ 1 2 ⋅ 2 S B = 1 S B
127 122 125 126 3eqtr2i ⊢ 1 2 S A G B G -1 S A G B = 1 S B
128 107 127 92 3eqtri ⊢ 1 2 S A G B G -1 S 1 2 S A G -1 S B = B
129 128 oveq1i ⊢ 1 2 S A G B G -1 S 1 2 S A G -1 S B P C = B P C
130 74 129 oveq12i ⊢ 1 2 S A G B G 1 2 S A G -1 S B P C + 1 2 S A G B G -1 S 1 2 S A G -1 S B P C = A P C + B P C
131 26 34 130 3eqtr2i ⊢ A G B P C = A P C + B P C