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