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 2cn ⊢ 2 ∈ ℂ
10 2ne0 ⊢ 2 ≠ 0
11 9 10 recidi ⊢ 2 ⁢ 1 2 = 1
12 11 oveq1i ⊢ 2 ⁢ 1 2 S A G B = 1 S A G B
13 5 phnvi ⊢ U ∈ NrmCVec
14 halfcn ⊢ 1 2 ∈ ℂ
15 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B ∈ X
16 13 6 7 15 mp3an ⊢ A G B ∈ X
17 9 14 16 3pm3.2i ⊢ 2 ∈ ℂ ∧ 1 2 ∈ ℂ ∧ A G B ∈ X
18 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
19 13 17 18 mp2an ⊢ 2 ⁢ 1 2 S A G B = 2 S 1 2 S A G B
20 1 3 nvsid ⊢ U ∈ NrmCVec ∧ A G B ∈ X → 1 S A G B = A G B
21 13 16 20 mp2an ⊢ 1 S A G B = A G B
22 12 19 21 3eqtr3i ⊢ 2 S 1 2 S A G B = A G B
23 22 oveq1i ⊢ 2 S 1 2 S A G B P C = A G B P C
24 1 3 nvscl ⊢ U ∈ NrmCVec ∧ 1 2 ∈ ℂ ∧ A G B ∈ X → 1 2 S A G B ∈ X
25 13 14 16 24 mp3an ⊢ 1 2 S A G B ∈ X
26 1 2 3 4 5 25 8 ip2i ⊢ 2 S 1 2 S A G B P C = 2 ⁢ 1 2 S A G B P C
27 23 26 eqtr3i ⊢ A G B P C = 2 ⁢ 1 2 S A G B P C
28 neg1cn ⊢ − 1 ∈ ℂ
29 1 3 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ B ∈ X → -1 S B ∈ X
30 13 28 7 29 mp3an ⊢ -1 S B ∈ X
31 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ -1 S B ∈ X → A G -1 S B ∈ X
32 13 6 30 31 mp3an ⊢ A G -1 S B ∈ X
33 1 3 nvscl ⊢ U ∈ NrmCVec ∧ 1 2 ∈ ℂ ∧ A G -1 S B ∈ X → 1 2 S A G -1 S B ∈ X
34 13 14 32 33 mp3an ⊢ 1 2 S A G -1 S B ∈ X
35 1 2 3 4 5 25 34 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
36 eqid ⊢ 1 st ⁡ U = 1 st ⁡ U
37 36 nvvc ⊢ U ∈ NrmCVec → 1 st ⁡ U ∈ CVec OLD
38 13 37 ax-mp ⊢ 1 st ⁡ U ∈ CVec OLD
39 2 vafval ⊢ G = 1 st ⁡ 1 st ⁡ U
40 39 vcablo ⊢ 1 st ⁡ U ∈ CVec OLD → G ∈ AbelOp
41 38 40 ax-mp ⊢ G ∈ AbelOp
42 6 7 pm3.2i ⊢ A ∈ X ∧ B ∈ X
43 6 30 pm3.2i ⊢ A ∈ X ∧ -1 S B ∈ X
44 1 2 bafval ⊢ X = ran ⁡ G
45 44 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
46 41 42 43 45 mp3an ⊢ A G B G A G -1 S B = A G A G B G -1 S B
47 3 smfval ⊢ S = 2 nd ⁡ 1 st ⁡ U
48 39 47 44 vc2OLD ⊢ 1 st ⁡ U ∈ CVec OLD ∧ A ∈ X → A G A = 2 S A
49 38 6 48 mp2an ⊢ A G A = 2 S A
50 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
51 1 2 3 50 nvrinv ⊢ U ∈ NrmCVec ∧ B ∈ X → B G -1 S B = 0 vec ⁡ U
52 13 7 51 mp2an ⊢ B G -1 S B = 0 vec ⁡ U
53 49 52 oveq12i ⊢ A G A G B G -1 S B = 2 S A G 0 vec ⁡ U
54 1 3 nvscl ⊢ U ∈ NrmCVec ∧ 2 ∈ ℂ ∧ A ∈ X → 2 S A ∈ X
55 13 9 6 54 mp3an ⊢ 2 S A ∈ X
56 1 2 50 nv0rid ⊢ U ∈ NrmCVec ∧ 2 S A ∈ X → 2 S A G 0 vec ⁡ U = 2 S A
57 13 55 56 mp2an ⊢ 2 S A G 0 vec ⁡ U = 2 S A
58 46 53 57 3eqtri ⊢ A G B G A G -1 S B = 2 S A
59 58 oveq2i ⊢ 1 2 S A G B G A G -1 S B = 1 2 S 2 S A
60 14 9 6 3pm3.2i ⊢ 1 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ A ∈ X
61 1 3 nvsass ⊢ U ∈ NrmCVec ∧ 1 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ A ∈ X → 1 2 ⋅ 2 S A = 1 2 S 2 S A
62 13 60 61 mp2an ⊢ 1 2 ⋅ 2 S A = 1 2 S 2 S A
63 59 62 eqtr4i ⊢ 1 2 S A G B G A G -1 S B = 1 2 ⋅ 2 S A
64 14 16 32 3pm3.2i ⊢ 1 2 ∈ ℂ ∧ A G B ∈ X ∧ A G -1 S B ∈ X
65 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
66 13 64 65 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
67 ax-1cn ⊢ 1 ∈ ℂ
68 67 9 10 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 13 6 70 mp2an ⊢ 1 S A = A
72 69 71 eqtri ⊢ 1 2 ⋅ 2 S A = A
73 63 66 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 28 14 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 28 14 32 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 13 77 78 mp2an ⊢ -1 ⁢ 1 2 S A G -1 S B = -1 S 1 2 S A G -1 S B
80 14 28 32 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 13 80 81 mp2an ⊢ 1 2 ⁢ -1 S A G -1 S B = 1 2 S -1 S A G -1 S B
83 28 6 30 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 13 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 28 28 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 13 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 13 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 13 28 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 13 101 7 102 mp3an ⊢ -1 S A G B ∈ X
104 14 16 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 13 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 44 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 41 42 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 50 nvrinv ⊢ U ∈ NrmCVec ∧ A ∈ X → A G -1 S A = 0 vec ⁡ U
112 13 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 13 7 7 114 mp3an ⊢ B G B ∈ X
116 1 2 50 nv0lid ⊢ U ∈ NrmCVec ∧ B G B ∈ X → 0 vec ⁡ U G B G B = B G B
117 13 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 39 47 44 vc2OLD ⊢ 1 st ⁡ U ∈ CVec OLD ∧ B ∈ X → B G B = 2 S B
120 38 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 14 9 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 13 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 27 35 130 3eqtr2i ⊢ A G B P C = A P C + B P C