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 𝑔 ) ) ) )