# 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 syl6eqr ( ( 𝐹 +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 syl6eq ( ( ( 𝐴 +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 𝑆 ) ) ) ) )