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 ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) → ( ( 𝐴 +P 𝐷 ) ·P 𝐹 ) = ( ( 𝐵 +P 𝐶 ) ·P 𝐹 ) )
2 distrpr ⊢ ( 𝐹 ·P ( 𝐴 +P 𝐷 ) ) = ( ( 𝐹 ·P 𝐴 ) +P ( 𝐹 ·P 𝐷 ) )
3 mulcompr ⊢ ( ( 𝐴 +P 𝐷 ) ·P 𝐹 ) = ( 𝐹 ·P ( 𝐴 +P 𝐷 ) )
4 mulcompr ⊢ ( 𝐴 ·P 𝐹 ) = ( 𝐹 ·P 𝐴 )
5 mulcompr ⊢ ( 𝐷 ·P 𝐹 ) = ( 𝐹 ·P 𝐷 )
6 4 5 oveq12i ⊢ ( ( 𝐴 ·P 𝐹 ) +P ( 𝐷 ·P 𝐹 ) ) = ( ( 𝐹 ·P 𝐴 ) +P ( 𝐹 ·P 𝐷 ) )
7 2 3 6 3eqtr4i ⊢ ( ( 𝐴 +P 𝐷 ) ·P 𝐹 ) = ( ( 𝐴 ·P 𝐹 ) +P ( 𝐷 ·P 𝐹 ) )
8 distrpr ⊢ ( 𝐹 ·P ( 𝐵 +P 𝐶 ) ) = ( ( 𝐹 ·P 𝐵 ) +P ( 𝐹 ·P 𝐶 ) )
9 mulcompr ⊢ ( ( 𝐵 +P 𝐶 ) ·P 𝐹 ) = ( 𝐹 ·P ( 𝐵 +P 𝐶 ) )
10 mulcompr ⊢ ( 𝐵 ·P 𝐹 ) = ( 𝐹 ·P 𝐵 )
11 mulcompr ⊢ ( 𝐶 ·P 𝐹 ) = ( 𝐹 ·P 𝐶 )
12 10 11 oveq12i ⊢ ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝐹 ) ) = ( ( 𝐹 ·P 𝐵 ) +P ( 𝐹 ·P 𝐶 ) )
13 8 9 12 3eqtr4i ⊢ ( ( 𝐵 +P 𝐶 ) ·P 𝐹 ) = ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝐹 ) )
14 1 7 13 3eqtr3g ⊢ ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) → ( ( 𝐴 ·P 𝐹 ) +P ( 𝐷 ·P 𝐹 ) ) = ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝐹 ) ) )
15 14 oveq1d ⊢ ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) → ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐷 ·P 𝐹 ) ) +P ( 𝐶 ·P 𝑆 ) ) = ( ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝐹 ) ) +P ( 𝐶 ·P 𝑆 ) ) )
16 addasspr ⊢ ( ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝐹 ) ) +P ( 𝐶 ·P 𝑆 ) ) = ( ( 𝐵 ·P 𝐹 ) +P ( ( 𝐶 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) )
17 oveq2 ⊢ ( ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) → ( 𝐶 ·P ( 𝐹 +P 𝑆 ) ) = ( 𝐶 ·P ( 𝐺 +P 𝑅 ) ) )
18 distrpr ⊢ ( 𝐶 ·P ( 𝐹 +P 𝑆 ) ) = ( ( 𝐶 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) )
19 distrpr ⊢ ( 𝐶 ·P ( 𝐺 +P 𝑅 ) ) = ( ( 𝐶 ·P 𝐺 ) +P ( 𝐶 ·P 𝑅 ) )
20 17 18 19 3eqtr3g ⊢ ( ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) → ( ( 𝐶 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) = ( ( 𝐶 ·P 𝐺 ) +P ( 𝐶 ·P 𝑅 ) ) )
21 20 oveq2d ⊢ ( ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) → ( ( 𝐵 ·P 𝐹 ) +P ( ( 𝐶 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) ) = ( ( 𝐵 ·P 𝐹 ) +P ( ( 𝐶 ·P 𝐺 ) +P ( 𝐶 ·P 𝑅 ) ) ) )
22 16 21 syl5eq ⊢ ( ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) → ( ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝐹 ) ) +P ( 𝐶 ·P 𝑆 ) ) = ( ( 𝐵 ·P 𝐹 ) +P ( ( 𝐶 ·P 𝐺 ) +P ( 𝐶 ·P 𝑅 ) ) ) )
23 15 22 sylan9eq ⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐷 ·P 𝐹 ) ) +P ( 𝐶 ·P 𝑆 ) ) = ( ( 𝐵 ·P 𝐹 ) +P ( ( 𝐶 ·P 𝐺 ) +P ( 𝐶 ·P 𝑅 ) ) ) )
24 ovex ⊢ ( 𝐴 ·P 𝐹 ) ∈ V
25 ovex ⊢ ( 𝐷 ·P 𝐹 ) ∈ V
26 ovex ⊢ ( 𝐶 ·P 𝑆 ) ∈ V
27 addcompr ⊢ ( 𝑥 +P 𝑦 ) = ( 𝑦 +P 𝑥 )
28 addasspr ⊢ ( ( 𝑥 +P 𝑦 ) +P 𝑧 ) = ( 𝑥 +P ( 𝑦 +P 𝑧 ) )
29 24 25 26 27 28 caov32 ⊢ ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐷 ·P 𝐹 ) ) +P ( 𝐶 ·P 𝑆 ) ) = ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) +P ( 𝐷 ·P 𝐹 ) )
30 ovex ⊢ ( 𝐵 ·P 𝐹 ) ∈ V
31 ovex ⊢ ( 𝐶 ·P 𝐺 ) ∈ V
32 ovex ⊢ ( 𝐶 ·P 𝑅 ) ∈ V
33 30 31 32 27 28 caov12 ⊢ ( ( 𝐵 ·P 𝐹 ) +P ( ( 𝐶 ·P 𝐺 ) +P ( 𝐶 ·P 𝑅 ) ) ) = ( ( 𝐶 ·P 𝐺 ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) )
34 23 29 33 3eqtr3g ⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) +P ( 𝐷 ·P 𝐹 ) ) = ( ( 𝐶 ·P 𝐺 ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) )
35 34 oveq2d ⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) +P ( 𝐷 ·P 𝐹 ) ) ) = ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) +P ( ( 𝐶 ·P 𝐺 ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) ) )
36 oveq2 ⊢ ( ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) → ( 𝐷 ·P ( 𝐹 +P 𝑆 ) ) = ( 𝐷 ·P ( 𝐺 +P 𝑅 ) ) )
37 distrpr ⊢ ( 𝐷 ·P ( 𝐹 +P 𝑆 ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( 𝐷 ·P 𝑆 ) )
38 distrpr ⊢ ( 𝐷 ·P ( 𝐺 +P 𝑅 ) ) = ( ( 𝐷 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) )
39 36 37 38 3eqtr3g ⊢ ( ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) → ( ( 𝐷 ·P 𝐹 ) +P ( 𝐷 ·P 𝑆 ) ) = ( ( 𝐷 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) )
40 39 oveq2d ⊢ ( ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) → ( ( 𝐴 ·P 𝐺 ) +P ( ( 𝐷 ·P 𝐹 ) +P ( 𝐷 ·P 𝑆 ) ) ) = ( ( 𝐴 ·P 𝐺 ) +P ( ( 𝐷 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) ) )
41 addasspr ⊢ ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝐺 ) ) +P ( 𝐷 ·P 𝑅 ) ) = ( ( 𝐴 ·P 𝐺 ) +P ( ( 𝐷 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) )
42 40 41 eqtr4di ⊢ ( ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) → ( ( 𝐴 ·P 𝐺 ) +P ( ( 𝐷 ·P 𝐹 ) +P ( 𝐷 ·P 𝑆 ) ) ) = ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝐺 ) ) +P ( 𝐷 ·P 𝑅 ) ) )
43 oveq1 ⊢ ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) → ( ( 𝐴 +P 𝐷 ) ·P 𝐺 ) = ( ( 𝐵 +P 𝐶 ) ·P 𝐺 ) )
44 distrpr ⊢ ( 𝐺 ·P ( 𝐴 +P 𝐷 ) ) = ( ( 𝐺 ·P 𝐴 ) +P ( 𝐺 ·P 𝐷 ) )
45 mulcompr ⊢ ( ( 𝐴 +P 𝐷 ) ·P 𝐺 ) = ( 𝐺 ·P ( 𝐴 +P 𝐷 ) )
46 mulcompr ⊢ ( 𝐴 ·P 𝐺 ) = ( 𝐺 ·P 𝐴 )
47 mulcompr ⊢ ( 𝐷 ·P 𝐺 ) = ( 𝐺 ·P 𝐷 )
48 46 47 oveq12i ⊢ ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝐺 ) ) = ( ( 𝐺 ·P 𝐴 ) +P ( 𝐺 ·P 𝐷 ) )
49 44 45 48 3eqtr4i ⊢ ( ( 𝐴 +P 𝐷 ) ·P 𝐺 ) = ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝐺 ) )
50 distrpr ⊢ ( 𝐺 ·P ( 𝐵 +P 𝐶 ) ) = ( ( 𝐺 ·P 𝐵 ) +P ( 𝐺 ·P 𝐶 ) )
51 mulcompr ⊢ ( ( 𝐵 +P 𝐶 ) ·P 𝐺 ) = ( 𝐺 ·P ( 𝐵 +P 𝐶 ) )
52 mulcompr ⊢ ( 𝐵 ·P 𝐺 ) = ( 𝐺 ·P 𝐵 )
53 mulcompr ⊢ ( 𝐶 ·P 𝐺 ) = ( 𝐺 ·P 𝐶 )
54 52 53 oveq12i ⊢ ( ( 𝐵 ·P 𝐺 ) +P ( 𝐶 ·P 𝐺 ) ) = ( ( 𝐺 ·P 𝐵 ) +P ( 𝐺 ·P 𝐶 ) )
55 50 51 54 3eqtr4i ⊢ ( ( 𝐵 +P 𝐶 ) ·P 𝐺 ) = ( ( 𝐵 ·P 𝐺 ) +P ( 𝐶 ·P 𝐺 ) )
56 43 49 55 3eqtr3g ⊢ ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) → ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝐺 ) ) = ( ( 𝐵 ·P 𝐺 ) +P ( 𝐶 ·P 𝐺 ) ) )
57 56 oveq1d ⊢ ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) → ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝐺 ) ) +P ( 𝐷 ·P 𝑅 ) ) = ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐶 ·P 𝐺 ) ) +P ( 𝐷 ·P 𝑅 ) ) )
58 42 57 sylan9eqr ⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( 𝐴 ·P 𝐺 ) +P ( ( 𝐷 ·P 𝐹 ) +P ( 𝐷 ·P 𝑆 ) ) ) = ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐶 ·P 𝐺 ) ) +P ( 𝐷 ·P 𝑅 ) ) )
59 ovex ⊢ ( 𝐴 ·P 𝐺 ) ∈ V
60 ovex ⊢ ( 𝐷 ·P 𝑆 ) ∈ V
61 59 25 60 27 28 caov12 ⊢ ( ( 𝐴 ·P 𝐺 ) +P ( ( 𝐷 ·P 𝐹 ) +P ( 𝐷 ·P 𝑆 ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝑆 ) ) )
62 ovex ⊢ ( 𝐵 ·P 𝐺 ) ∈ V
63 ovex ⊢ ( 𝐷 ·P 𝑅 ) ∈ V
64 62 31 63 27 28 caov32 ⊢ ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐶 ·P 𝐺 ) ) +P ( 𝐷 ·P 𝑅 ) ) = ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) +P ( 𝐶 ·P 𝐺 ) )
65 58 61 64 3eqtr3g ⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( 𝐷 ·P 𝐹 ) +P ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝑆 ) ) ) = ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) +P ( 𝐶 ·P 𝐺 ) ) )
66 65 oveq1d ⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( ( 𝐷 ·P 𝐹 ) +P ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝑆 ) ) ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) = ( ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) +P ( 𝐶 ·P 𝐺 ) ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) )
67 addasspr ⊢ ( ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) +P ( 𝐶 ·P 𝐺 ) ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) = ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) +P ( ( 𝐶 ·P 𝐺 ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) )
68 66 67 eqtrdi ⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( ( 𝐷 ·P 𝐹 ) +P ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝑆 ) ) ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) = ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) +P ( ( 𝐶 ·P 𝐺 ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) ) )
69 35 68 eqtr4d ⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) +P ( 𝐷 ·P 𝐹 ) ) ) = ( ( ( 𝐷 ·P 𝐹 ) +P ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝑆 ) ) ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) )
70 ovex ⊢ ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) ∈ V
71 ovex ⊢ ( ( 𝐴 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) ∈ V
72 70 71 25 27 28 caov13 ⊢ ( ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) +P ( 𝐷 ·P 𝐹 ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) +P ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) ) )
73 addasspr ⊢ ( ( ( 𝐷 ·P 𝐹 ) +P ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝑆 ) ) ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝑆 ) ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) )
74 69 72 73 3eqtr3g ⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) +P ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝑆 ) ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) ) )
75 24 26 62 27 28 63 caov4 ⊢ ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) +P ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) ) = ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) )
76 75 oveq2i ⊢ ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐶 ·P 𝑆 ) ) +P ( ( 𝐵 ·P 𝐺 ) +P ( 𝐷 ·P 𝑅 ) ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) )
77 59 60 30 27 28 32 caov42 ⊢ ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝑆 ) ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) = ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) )
78 77 oveq2i ⊢ ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐷 ·P 𝑆 ) ) +P ( ( 𝐵 ·P 𝐹 ) +P ( 𝐶 ·P 𝑅 ) ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) )
79 74 76 78 3eqtr3g ⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) ) )