Metamath Proof Explorer


Theorem addcmpblnr

Description: Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995) (New usage is discouraged.)

Ref Expression
Assertion addcmpblnr ( ( ( ( 𝐴P𝐵P ) ∧ ( 𝐶P𝐷P ) ) ∧ ( ( 𝐹P𝐺P ) ∧ ( 𝑅P𝑆P ) ) ) → ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ⟨ ( 𝐴 +P 𝐹 ) , ( 𝐵 +P 𝐺 ) ⟩ ~R ⟨ ( 𝐶 +P 𝑅 ) , ( 𝐷 +P 𝑆 ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 oveq12 ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( 𝐴 +P 𝐷 ) +P ( 𝐹 +P 𝑆 ) ) = ( ( 𝐵 +P 𝐶 ) +P ( 𝐺 +P 𝑅 ) ) )
2 addclpr ( ( 𝐴P𝐹P ) → ( 𝐴 +P 𝐹 ) ∈ P )
3 addclpr ( ( 𝐵P𝐺P ) → ( 𝐵 +P 𝐺 ) ∈ P )
4 2 3 anim12i ( ( ( 𝐴P𝐹P ) ∧ ( 𝐵P𝐺P ) ) → ( ( 𝐴 +P 𝐹 ) ∈ P ∧ ( 𝐵 +P 𝐺 ) ∈ P ) )
5 4 an4s ( ( ( 𝐴P𝐵P ) ∧ ( 𝐹P𝐺P ) ) → ( ( 𝐴 +P 𝐹 ) ∈ P ∧ ( 𝐵 +P 𝐺 ) ∈ P ) )
6 addclpr ( ( 𝐶P𝑅P ) → ( 𝐶 +P 𝑅 ) ∈ P )
7 addclpr ( ( 𝐷P𝑆P ) → ( 𝐷 +P 𝑆 ) ∈ P )
8 6 7 anim12i ( ( ( 𝐶P𝑅P ) ∧ ( 𝐷P𝑆P ) ) → ( ( 𝐶 +P 𝑅 ) ∈ P ∧ ( 𝐷 +P 𝑆 ) ∈ P ) )
9 8 an4s ( ( ( 𝐶P𝐷P ) ∧ ( 𝑅P𝑆P ) ) → ( ( 𝐶 +P 𝑅 ) ∈ P ∧ ( 𝐷 +P 𝑆 ) ∈ P ) )
10 5 9 anim12i ( ( ( ( 𝐴P𝐵P ) ∧ ( 𝐹P𝐺P ) ) ∧ ( ( 𝐶P𝐷P ) ∧ ( 𝑅P𝑆P ) ) ) → ( ( ( 𝐴 +P 𝐹 ) ∈ P ∧ ( 𝐵 +P 𝐺 ) ∈ P ) ∧ ( ( 𝐶 +P 𝑅 ) ∈ P ∧ ( 𝐷 +P 𝑆 ) ∈ P ) ) )
11 10 an4s ( ( ( ( 𝐴P𝐵P ) ∧ ( 𝐶P𝐷P ) ) ∧ ( ( 𝐹P𝐺P ) ∧ ( 𝑅P𝑆P ) ) ) → ( ( ( 𝐴 +P 𝐹 ) ∈ P ∧ ( 𝐵 +P 𝐺 ) ∈ P ) ∧ ( ( 𝐶 +P 𝑅 ) ∈ P ∧ ( 𝐷 +P 𝑆 ) ∈ P ) ) )
12 enrbreq ( ( ( ( 𝐴 +P 𝐹 ) ∈ P ∧ ( 𝐵 +P 𝐺 ) ∈ P ) ∧ ( ( 𝐶 +P 𝑅 ) ∈ P ∧ ( 𝐷 +P 𝑆 ) ∈ P ) ) → ( ⟨ ( 𝐴 +P 𝐹 ) , ( 𝐵 +P 𝐺 ) ⟩ ~R ⟨ ( 𝐶 +P 𝑅 ) , ( 𝐷 +P 𝑆 ) ⟩ ↔ ( ( 𝐴 +P 𝐹 ) +P ( 𝐷 +P 𝑆 ) ) = ( ( 𝐵 +P 𝐺 ) +P ( 𝐶 +P 𝑅 ) ) ) )
13 11 12 syl ( ( ( ( 𝐴P𝐵P ) ∧ ( 𝐶P𝐷P ) ) ∧ ( ( 𝐹P𝐺P ) ∧ ( 𝑅P𝑆P ) ) ) → ( ⟨ ( 𝐴 +P 𝐹 ) , ( 𝐵 +P 𝐺 ) ⟩ ~R ⟨ ( 𝐶 +P 𝑅 ) , ( 𝐷 +P 𝑆 ) ⟩ ↔ ( ( 𝐴 +P 𝐹 ) +P ( 𝐷 +P 𝑆 ) ) = ( ( 𝐵 +P 𝐺 ) +P ( 𝐶 +P 𝑅 ) ) ) )
14 addcompr ( 𝐹 +P 𝐷 ) = ( 𝐷 +P 𝐹 )
15 14 oveq1i ( ( 𝐹 +P 𝐷 ) +P 𝑆 ) = ( ( 𝐷 +P 𝐹 ) +P 𝑆 )
16 addasspr ( ( 𝐹 +P 𝐷 ) +P 𝑆 ) = ( 𝐹 +P ( 𝐷 +P 𝑆 ) )
17 addasspr ( ( 𝐷 +P 𝐹 ) +P 𝑆 ) = ( 𝐷 +P ( 𝐹 +P 𝑆 ) )
18 15 16 17 3eqtr3i ( 𝐹 +P ( 𝐷 +P 𝑆 ) ) = ( 𝐷 +P ( 𝐹 +P 𝑆 ) )
19 18 oveq2i ( 𝐴 +P ( 𝐹 +P ( 𝐷 +P 𝑆 ) ) ) = ( 𝐴 +P ( 𝐷 +P ( 𝐹 +P 𝑆 ) ) )
20 addasspr ( ( 𝐴 +P 𝐹 ) +P ( 𝐷 +P 𝑆 ) ) = ( 𝐴 +P ( 𝐹 +P ( 𝐷 +P 𝑆 ) ) )
21 addasspr ( ( 𝐴 +P 𝐷 ) +P ( 𝐹 +P 𝑆 ) ) = ( 𝐴 +P ( 𝐷 +P ( 𝐹 +P 𝑆 ) ) )
22 19 20 21 3eqtr4i ( ( 𝐴 +P 𝐹 ) +P ( 𝐷 +P 𝑆 ) ) = ( ( 𝐴 +P 𝐷 ) +P ( 𝐹 +P 𝑆 ) )
23 addcompr ( 𝐺 +P 𝐶 ) = ( 𝐶 +P 𝐺 )
24 23 oveq1i ( ( 𝐺 +P 𝐶 ) +P 𝑅 ) = ( ( 𝐶 +P 𝐺 ) +P 𝑅 )
25 addasspr ( ( 𝐺 +P 𝐶 ) +P 𝑅 ) = ( 𝐺 +P ( 𝐶 +P 𝑅 ) )
26 addasspr ( ( 𝐶 +P 𝐺 ) +P 𝑅 ) = ( 𝐶 +P ( 𝐺 +P 𝑅 ) )
27 24 25 26 3eqtr3i ( 𝐺 +P ( 𝐶 +P 𝑅 ) ) = ( 𝐶 +P ( 𝐺 +P 𝑅 ) )
28 27 oveq2i ( 𝐵 +P ( 𝐺 +P ( 𝐶 +P 𝑅 ) ) ) = ( 𝐵 +P ( 𝐶 +P ( 𝐺 +P 𝑅 ) ) )
29 addasspr ( ( 𝐵 +P 𝐺 ) +P ( 𝐶 +P 𝑅 ) ) = ( 𝐵 +P ( 𝐺 +P ( 𝐶 +P 𝑅 ) ) )
30 addasspr ( ( 𝐵 +P 𝐶 ) +P ( 𝐺 +P 𝑅 ) ) = ( 𝐵 +P ( 𝐶 +P ( 𝐺 +P 𝑅 ) ) )
31 28 29 30 3eqtr4i ( ( 𝐵 +P 𝐺 ) +P ( 𝐶 +P 𝑅 ) ) = ( ( 𝐵 +P 𝐶 ) +P ( 𝐺 +P 𝑅 ) )
32 22 31 eqeq12i ( ( ( 𝐴 +P 𝐹 ) +P ( 𝐷 +P 𝑆 ) ) = ( ( 𝐵 +P 𝐺 ) +P ( 𝐶 +P 𝑅 ) ) ↔ ( ( 𝐴 +P 𝐷 ) +P ( 𝐹 +P 𝑆 ) ) = ( ( 𝐵 +P 𝐶 ) +P ( 𝐺 +P 𝑅 ) ) )
33 13 32 bitrdi ( ( ( ( 𝐴P𝐵P ) ∧ ( 𝐶P𝐷P ) ) ∧ ( ( 𝐹P𝐺P ) ∧ ( 𝑅P𝑆P ) ) ) → ( ⟨ ( 𝐴 +P 𝐹 ) , ( 𝐵 +P 𝐺 ) ⟩ ~R ⟨ ( 𝐶 +P 𝑅 ) , ( 𝐷 +P 𝑆 ) ⟩ ↔ ( ( 𝐴 +P 𝐷 ) +P ( 𝐹 +P 𝑆 ) ) = ( ( 𝐵 +P 𝐶 ) +P ( 𝐺 +P 𝑅 ) ) ) )
34 1 33 syl5ibr ( ( ( ( 𝐴P𝐵P ) ∧ ( 𝐶P𝐷P ) ) ∧ ( ( 𝐹P𝐺P ) ∧ ( 𝑅P𝑆P ) ) ) → ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ⟨ ( 𝐴 +P 𝐹 ) , ( 𝐵 +P 𝐺 ) ⟩ ~R ⟨ ( 𝐶 +P 𝑅 ) , ( 𝐷 +P 𝑆 ) ⟩ ) )