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 imbitrrid ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ⟨ ( 𝐴 +P 𝐹 ) , ( 𝐵 +P 𝐺 ) ⟩ ~R ⟨ ( 𝐶 +P 𝑅 ) , ( 𝐷 +P 𝑆 ) ⟩ ) )