Metamath Proof Explorer

Theorem mulcmpblnrlem

Description: Lemma used in lemma showing compatibility of multiplication. (Contributed by NM, 4-Sep-1995) (New usage is discouraged.)

Ref Expression
Assertion mulcmpblnrlem 
|- ( ( ( 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 ) ) ) ) )

Proof

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 syl5eq 
 |-  ( ( 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 ) ) ) ) )