This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prsrlem1

Description: Decomposing signed reals into positive reals. Lemma for addsrpr and mulsrpr . (Contributed by Jim Kingdon, 30-Dec-2019)

Ref Expression
Assertion prsrlem1 ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( ( ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) ) ∧ ( ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) ∧ ( 𝑔 ∈ P ∧ ℎ ∈ P ) ) ) ∧ ( ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) ∧ ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) ) ) )

Proof

Step Hyp Ref Expression
1 enrer ⊢ ~R Er ( P × P )
2 erdm ⊢ ( ~R Er ( P × P ) → dom ~R = ( P × P ) )
3 1 2 ax-mp ⊢ dom ~R = ( P × P )
4 simprll ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R )
5 simpll ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → 𝐴 ∈ ( ( P × P ) / ~R ) )
6 4 5 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
7 ecelqsdm ⊢ ( ( dom ~R = ( P × P ) ∧ [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) ) → ⟨ 𝑤 , 𝑣 ⟩ ∈ ( P × P ) )
8 3 6 7 sylancr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ⟨ 𝑤 , 𝑣 ⟩ ∈ ( P × P ) )
9 opelxp ⊢ ( ⟨ 𝑤 , 𝑣 ⟩ ∈ ( P × P ) ↔ ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) )
10 8 9 sylib ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) )
11 simprrl ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R )
12 11 5 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
13 ecelqsdm ⊢ ( ( dom ~R = ( P × P ) ∧ [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) ) → ⟨ 𝑠 , 𝑓 ⟩ ∈ ( P × P ) )
14 3 12 13 sylancr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ⟨ 𝑠 , 𝑓 ⟩ ∈ ( P × P ) )
15 opelxp ⊢ ( ⟨ 𝑠 , 𝑓 ⟩ ∈ ( P × P ) ↔ ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) )
16 14 15 sylib ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) )
17 10 16 jca ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) ) )
18 simprlr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R )
19 simplr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → 𝐵 ∈ ( ( P × P ) / ~R ) )
20 18 19 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
21 ecelqsdm ⊢ ( ( dom ~R = ( P × P ) ∧ [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ∈ ( ( P × P ) / ~R ) ) → ⟨ 𝑢 , 𝑡 ⟩ ∈ ( P × P ) )
22 3 20 21 sylancr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ⟨ 𝑢 , 𝑡 ⟩ ∈ ( P × P ) )
23 opelxp ⊢ ( ⟨ 𝑢 , 𝑡 ⟩ ∈ ( P × P ) ↔ ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) )
24 22 23 sylib ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) )
25 simprrr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R )
26 25 19 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → [ ⟨ 𝑔 , ℎ ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
27 ecelqsdm ⊢ ( ( dom ~R = ( P × P ) ∧ [ ⟨ 𝑔 , ℎ ⟩ ] ~R ∈ ( ( P × P ) / ~R ) ) → ⟨ 𝑔 , ℎ ⟩ ∈ ( P × P ) )
28 3 26 27 sylancr ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ⟨ 𝑔 , ℎ ⟩ ∈ ( P × P ) )
29 opelxp ⊢ ( ⟨ 𝑔 , ℎ ⟩ ∈ ( P × P ) ↔ ( 𝑔 ∈ P ∧ ℎ ∈ P ) )
30 28 29 sylib ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( 𝑔 ∈ P ∧ ℎ ∈ P ) )
31 24 30 jca ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) ∧ ( 𝑔 ∈ P ∧ ℎ ∈ P ) ) )
32 4 11 eqtr3d ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R )
33 1 a1i ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ~R Er ( P × P ) )
34 33 8 erth ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( ⟨ 𝑤 , 𝑣 ⟩ ~R ⟨ 𝑠 , 𝑓 ⟩ ↔ [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ) )
35 32 34 mpbird ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ⟨ 𝑤 , 𝑣 ⟩ ~R ⟨ 𝑠 , 𝑓 ⟩ )
36 df-enr ⊢ ~R = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( P × P ) ∧ 𝑦 ∈ ( P × P ) ) ∧ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ∃ 𝑑 ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ ) ∧ ( 𝑎 +P 𝑑 ) = ( 𝑏 +P 𝑐 ) ) ) }
37 36 ecopoveq ⊢ ( ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) ) → ( ⟨ 𝑤 , 𝑣 ⟩ ~R ⟨ 𝑠 , 𝑓 ⟩ ↔ ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) ) )
38 10 16 37 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( ⟨ 𝑤 , 𝑣 ⟩ ~R ⟨ 𝑠 , 𝑓 ⟩ ↔ ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) ) )
39 35 38 mpbid ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) )
40 18 25 eqtr3d ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R = [ ⟨ 𝑔 , ℎ ⟩ ] ~R )
41 33 22 erth ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( ⟨ 𝑢 , 𝑡 ⟩ ~R ⟨ 𝑔 , ℎ ⟩ ↔ [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) )
42 40 41 mpbird ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ⟨ 𝑢 , 𝑡 ⟩ ~R ⟨ 𝑔 , ℎ ⟩ )
43 36 ecopoveq ⊢ ( ( ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) ∧ ( 𝑔 ∈ P ∧ ℎ ∈ P ) ) → ( ⟨ 𝑢 , 𝑡 ⟩ ~R ⟨ 𝑔 , ℎ ⟩ ↔ ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) ) )
44 24 30 43 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( ⟨ 𝑢 , 𝑡 ⟩ ~R ⟨ 𝑔 , ℎ ⟩ ↔ ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) ) )
45 42 44 mpbid ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) )
46 39 45 jca ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) ∧ ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) ) )
47 17 31 46 jca31 ⊢ ( ( ( 𝐴 ∈ ( ( P × P ) / ~R ) ∧ 𝐵 ∈ ( ( P × P ) / ~R ) ) ∧ ( ( 𝐴 = [ ⟨ 𝑤 , 𝑣 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑢 , 𝑡 ⟩ ] ~R ) ∧ ( 𝐴 = [ ⟨ 𝑠 , 𝑓 ⟩ ] ~R ∧ 𝐵 = [ ⟨ 𝑔 , ℎ ⟩ ] ~R ) ) ) → ( ( ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑠 ∈ P ∧ 𝑓 ∈ P ) ) ∧ ( ( 𝑢 ∈ P ∧ 𝑡 ∈ P ) ∧ ( 𝑔 ∈ P ∧ ℎ ∈ P ) ) ) ∧ ( ( 𝑤 +P 𝑓 ) = ( 𝑣 +P 𝑠 ) ∧ ( 𝑢 +P ℎ ) = ( 𝑡 +P 𝑔 ) ) ) )