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