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 + 𝑷 D = B + 𝑷 C ∧ F + 𝑷 S = G + 𝑷 R → D ⋅ 𝑷 F + 𝑷 A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R = D ⋅ 𝑷 F + 𝑷 A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F + 𝑷 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S

Proof

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