Step |
Hyp |
Ref |
Expression |
1 |
|
oveq1 |
|- ( ( A +P. D ) = ( B +P. C ) -> ( ( A +P. D ) .P. F ) = ( ( B +P. C ) .P. F ) ) |
2 |
|
distrpr |
|- ( F .P. ( A +P. D ) ) = ( ( F .P. A ) +P. ( F .P. D ) ) |
3 |
|
mulcompr |
|- ( ( A +P. D ) .P. F ) = ( F .P. ( A +P. D ) ) |
4 |
|
mulcompr |
|- ( A .P. F ) = ( F .P. A ) |
5 |
|
mulcompr |
|- ( D .P. F ) = ( F .P. D ) |
6 |
4 5
|
oveq12i |
|- ( ( A .P. F ) +P. ( D .P. F ) ) = ( ( F .P. A ) +P. ( F .P. D ) ) |
7 |
2 3 6
|
3eqtr4i |
|- ( ( A +P. D ) .P. F ) = ( ( A .P. F ) +P. ( D .P. F ) ) |
8 |
|
distrpr |
|- ( F .P. ( B +P. C ) ) = ( ( F .P. B ) +P. ( F .P. C ) ) |
9 |
|
mulcompr |
|- ( ( B +P. C ) .P. F ) = ( F .P. ( B +P. C ) ) |
10 |
|
mulcompr |
|- ( B .P. F ) = ( F .P. B ) |
11 |
|
mulcompr |
|- ( C .P. F ) = ( F .P. C ) |
12 |
10 11
|
oveq12i |
|- ( ( B .P. F ) +P. ( C .P. F ) ) = ( ( F .P. B ) +P. ( F .P. C ) ) |
13 |
8 9 12
|
3eqtr4i |
|- ( ( B +P. C ) .P. F ) = ( ( B .P. F ) +P. ( C .P. F ) ) |
14 |
1 7 13
|
3eqtr3g |
|- ( ( A +P. D ) = ( B +P. C ) -> ( ( A .P. F ) +P. ( D .P. F ) ) = ( ( B .P. F ) +P. ( C .P. F ) ) ) |
15 |
14
|
oveq1d |
|- ( ( A +P. D ) = ( B +P. C ) -> ( ( ( A .P. F ) +P. ( D .P. F ) ) +P. ( C .P. S ) ) = ( ( ( B .P. F ) +P. ( C .P. F ) ) +P. ( C .P. S ) ) ) |
16 |
|
addasspr |
|- ( ( ( B .P. F ) +P. ( C .P. F ) ) +P. ( C .P. S ) ) = ( ( B .P. F ) +P. ( ( C .P. F ) +P. ( C .P. S ) ) ) |
17 |
|
oveq2 |
|- ( ( F +P. S ) = ( G +P. R ) -> ( C .P. ( F +P. S ) ) = ( C .P. ( G +P. R ) ) ) |
18 |
|
distrpr |
|- ( C .P. ( F +P. S ) ) = ( ( C .P. F ) +P. ( C .P. S ) ) |
19 |
|
distrpr |
|- ( C .P. ( G +P. R ) ) = ( ( C .P. G ) +P. ( C .P. R ) ) |
20 |
17 18 19
|
3eqtr3g |
|- ( ( F +P. S ) = ( G +P. R ) -> ( ( C .P. F ) +P. ( C .P. S ) ) = ( ( C .P. G ) +P. ( C .P. R ) ) ) |
21 |
20
|
oveq2d |
|- ( ( F +P. S ) = ( G +P. R ) -> ( ( B .P. F ) +P. ( ( C .P. F ) +P. ( C .P. S ) ) ) = ( ( B .P. F ) +P. ( ( C .P. G ) +P. ( C .P. R ) ) ) ) |
22 |
16 21
|
eqtrid |
|- ( ( F +P. S ) = ( G +P. R ) -> ( ( ( B .P. F ) +P. ( C .P. F ) ) +P. ( C .P. S ) ) = ( ( B .P. F ) +P. ( ( C .P. G ) +P. ( C .P. R ) ) ) ) |
23 |
15 22
|
sylan9eq |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( ( A .P. F ) +P. ( D .P. F ) ) +P. ( C .P. S ) ) = ( ( B .P. F ) +P. ( ( C .P. G ) +P. ( C .P. R ) ) ) ) |
24 |
|
ovex |
|- ( A .P. F ) e. _V |
25 |
|
ovex |
|- ( D .P. F ) e. _V |
26 |
|
ovex |
|- ( C .P. S ) e. _V |
27 |
|
addcompr |
|- ( x +P. y ) = ( y +P. x ) |
28 |
|
addasspr |
|- ( ( x +P. y ) +P. z ) = ( x +P. ( y +P. z ) ) |
29 |
24 25 26 27 28
|
caov32 |
|- ( ( ( A .P. F ) +P. ( D .P. F ) ) +P. ( C .P. S ) ) = ( ( ( A .P. F ) +P. ( C .P. S ) ) +P. ( D .P. F ) ) |
30 |
|
ovex |
|- ( B .P. F ) e. _V |
31 |
|
ovex |
|- ( C .P. G ) e. _V |
32 |
|
ovex |
|- ( C .P. R ) e. _V |
33 |
30 31 32 27 28
|
caov12 |
|- ( ( B .P. F ) +P. ( ( C .P. G ) +P. ( C .P. R ) ) ) = ( ( C .P. G ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) |
34 |
23 29 33
|
3eqtr3g |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( ( A .P. F ) +P. ( C .P. S ) ) +P. ( D .P. F ) ) = ( ( C .P. G ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) ) |
35 |
34
|
oveq2d |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( ( B .P. G ) +P. ( D .P. R ) ) +P. ( ( ( A .P. F ) +P. ( C .P. S ) ) +P. ( D .P. F ) ) ) = ( ( ( B .P. G ) +P. ( D .P. R ) ) +P. ( ( C .P. G ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) ) ) |
36 |
|
oveq2 |
|- ( ( F +P. S ) = ( G +P. R ) -> ( D .P. ( F +P. S ) ) = ( D .P. ( G +P. R ) ) ) |
37 |
|
distrpr |
|- ( D .P. ( F +P. S ) ) = ( ( D .P. F ) +P. ( D .P. S ) ) |
38 |
|
distrpr |
|- ( D .P. ( G +P. R ) ) = ( ( D .P. G ) +P. ( D .P. R ) ) |
39 |
36 37 38
|
3eqtr3g |
|- ( ( F +P. S ) = ( G +P. R ) -> ( ( D .P. F ) +P. ( D .P. S ) ) = ( ( D .P. G ) +P. ( D .P. R ) ) ) |
40 |
39
|
oveq2d |
|- ( ( F +P. S ) = ( G +P. R ) -> ( ( A .P. G ) +P. ( ( D .P. F ) +P. ( D .P. S ) ) ) = ( ( A .P. G ) +P. ( ( D .P. G ) +P. ( D .P. R ) ) ) ) |
41 |
|
addasspr |
|- ( ( ( A .P. G ) +P. ( D .P. G ) ) +P. ( D .P. R ) ) = ( ( A .P. G ) +P. ( ( D .P. G ) +P. ( D .P. R ) ) ) |
42 |
40 41
|
eqtr4di |
|- ( ( F +P. S ) = ( G +P. R ) -> ( ( A .P. G ) +P. ( ( D .P. F ) +P. ( D .P. S ) ) ) = ( ( ( A .P. G ) +P. ( D .P. G ) ) +P. ( D .P. R ) ) ) |
43 |
|
oveq1 |
|- ( ( A +P. D ) = ( B +P. C ) -> ( ( A +P. D ) .P. G ) = ( ( B +P. C ) .P. G ) ) |
44 |
|
distrpr |
|- ( G .P. ( A +P. D ) ) = ( ( G .P. A ) +P. ( G .P. D ) ) |
45 |
|
mulcompr |
|- ( ( A +P. D ) .P. G ) = ( G .P. ( A +P. D ) ) |
46 |
|
mulcompr |
|- ( A .P. G ) = ( G .P. A ) |
47 |
|
mulcompr |
|- ( D .P. G ) = ( G .P. D ) |
48 |
46 47
|
oveq12i |
|- ( ( A .P. G ) +P. ( D .P. G ) ) = ( ( G .P. A ) +P. ( G .P. D ) ) |
49 |
44 45 48
|
3eqtr4i |
|- ( ( A +P. D ) .P. G ) = ( ( A .P. G ) +P. ( D .P. G ) ) |
50 |
|
distrpr |
|- ( G .P. ( B +P. C ) ) = ( ( G .P. B ) +P. ( G .P. C ) ) |
51 |
|
mulcompr |
|- ( ( B +P. C ) .P. G ) = ( G .P. ( B +P. C ) ) |
52 |
|
mulcompr |
|- ( B .P. G ) = ( G .P. B ) |
53 |
|
mulcompr |
|- ( C .P. G ) = ( G .P. C ) |
54 |
52 53
|
oveq12i |
|- ( ( B .P. G ) +P. ( C .P. G ) ) = ( ( G .P. B ) +P. ( G .P. C ) ) |
55 |
50 51 54
|
3eqtr4i |
|- ( ( B +P. C ) .P. G ) = ( ( B .P. G ) +P. ( C .P. G ) ) |
56 |
43 49 55
|
3eqtr3g |
|- ( ( A +P. D ) = ( B +P. C ) -> ( ( A .P. G ) +P. ( D .P. G ) ) = ( ( B .P. G ) +P. ( C .P. G ) ) ) |
57 |
56
|
oveq1d |
|- ( ( A +P. D ) = ( B +P. C ) -> ( ( ( A .P. G ) +P. ( D .P. G ) ) +P. ( D .P. R ) ) = ( ( ( B .P. G ) +P. ( C .P. G ) ) +P. ( D .P. R ) ) ) |
58 |
42 57
|
sylan9eqr |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( A .P. G ) +P. ( ( D .P. F ) +P. ( D .P. S ) ) ) = ( ( ( B .P. G ) +P. ( C .P. G ) ) +P. ( D .P. R ) ) ) |
59 |
|
ovex |
|- ( A .P. G ) e. _V |
60 |
|
ovex |
|- ( D .P. S ) e. _V |
61 |
59 25 60 27 28
|
caov12 |
|- ( ( A .P. G ) +P. ( ( D .P. F ) +P. ( D .P. S ) ) ) = ( ( D .P. F ) +P. ( ( A .P. G ) +P. ( D .P. S ) ) ) |
62 |
|
ovex |
|- ( B .P. G ) e. _V |
63 |
|
ovex |
|- ( D .P. R ) e. _V |
64 |
62 31 63 27 28
|
caov32 |
|- ( ( ( B .P. G ) +P. ( C .P. G ) ) +P. ( D .P. R ) ) = ( ( ( B .P. G ) +P. ( D .P. R ) ) +P. ( C .P. G ) ) |
65 |
58 61 64
|
3eqtr3g |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( D .P. F ) +P. ( ( A .P. G ) +P. ( D .P. S ) ) ) = ( ( ( B .P. G ) +P. ( D .P. R ) ) +P. ( C .P. G ) ) ) |
66 |
65
|
oveq1d |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( ( D .P. F ) +P. ( ( A .P. G ) +P. ( D .P. S ) ) ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) = ( ( ( ( B .P. G ) +P. ( D .P. R ) ) +P. ( C .P. G ) ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) ) |
67 |
|
addasspr |
|- ( ( ( ( B .P. G ) +P. ( D .P. R ) ) +P. ( C .P. G ) ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) = ( ( ( B .P. G ) +P. ( D .P. R ) ) +P. ( ( C .P. G ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) ) |
68 |
66 67
|
eqtrdi |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( ( D .P. F ) +P. ( ( A .P. G ) +P. ( D .P. S ) ) ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) = ( ( ( B .P. G ) +P. ( D .P. R ) ) +P. ( ( C .P. G ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) ) ) |
69 |
35 68
|
eqtr4d |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( ( B .P. G ) +P. ( D .P. R ) ) +P. ( ( ( A .P. F ) +P. ( C .P. S ) ) +P. ( D .P. F ) ) ) = ( ( ( D .P. F ) +P. ( ( A .P. G ) +P. ( D .P. S ) ) ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) ) |
70 |
|
ovex |
|- ( ( B .P. G ) +P. ( D .P. R ) ) e. _V |
71 |
|
ovex |
|- ( ( A .P. F ) +P. ( C .P. S ) ) e. _V |
72 |
70 71 25 27 28
|
caov13 |
|- ( ( ( B .P. G ) +P. ( D .P. R ) ) +P. ( ( ( A .P. F ) +P. ( C .P. S ) ) +P. ( D .P. F ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. F ) +P. ( C .P. S ) ) +P. ( ( B .P. G ) +P. ( D .P. R ) ) ) ) |
73 |
|
addasspr |
|- ( ( ( D .P. F ) +P. ( ( A .P. G ) +P. ( D .P. S ) ) ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. G ) +P. ( D .P. S ) ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) ) |
74 |
69 72 73
|
3eqtr3g |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( D .P. F ) +P. ( ( ( A .P. F ) +P. ( C .P. S ) ) +P. ( ( B .P. G ) +P. ( D .P. R ) ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. G ) +P. ( D .P. S ) ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) ) ) |
75 |
24 26 62 27 28 63
|
caov4 |
|- ( ( ( A .P. F ) +P. ( C .P. S ) ) +P. ( ( B .P. G ) +P. ( D .P. R ) ) ) = ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) |
76 |
75
|
oveq2i |
|- ( ( D .P. F ) +P. ( ( ( A .P. F ) +P. ( C .P. S ) ) +P. ( ( B .P. G ) +P. ( D .P. R ) ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) ) |
77 |
59 60 30 27 28 32
|
caov42 |
|- ( ( ( A .P. G ) +P. ( D .P. S ) ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) = ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) |
78 |
77
|
oveq2i |
|- ( ( D .P. F ) +P. ( ( ( A .P. G ) +P. ( D .P. S ) ) +P. ( ( B .P. F ) +P. ( C .P. R ) ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) |
79 |
74 76 78
|
3eqtr3g |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( D .P. F ) +P. ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) ) |