Metamath Proof Explorer

Theorem ltsrpr

Description: Ordering of signed reals in terms of positive reals. (Contributed by NM, 20-Feb-1996) (Revised by Mario Carneiro, 12-Aug-2015) (New usage is discouraged.)

Ref Expression
Assertion ltsrpr ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R <R [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ↔ ( 𝐴 +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 df-nr ⊢ R = ( ( P × P ) / ~R )
5 ltrelsr ⊢ <R ⊆ ( R × R )
6 ltrelpr ⊢ <P ⊆ ( P × P )
7 0npr ⊢ ¬ ∅ ∈ P
8 dmplp ⊢ dom +P = ( P × P )
9 enrex ⊢ ~R ∈ V
10 df-ltr ⊢ <R = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) ) ) }
11 addclpr ⊢ ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑤 +P 𝑣 ) ∈ P )
12 11 ad2ant2lr ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( 𝑤 +P 𝑣 ) ∈ P )
13 addclpr ⊢ ( ( 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐵 +P 𝐶 ) ∈ P )
14 13 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( 𝐵 +P 𝐶 ) ∈ P )
15 12 14 anim12ci ⊢ ( ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) ∧ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ) → ( ( 𝐵 +P 𝐶 ) ∈ P ∧ ( 𝑤 +P 𝑣 ) ∈ P ) )
16 15 an4s ⊢ ( ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ) ∧ ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ) → ( ( 𝐵 +P 𝐶 ) ∈ P ∧ ( 𝑤 +P 𝑣 ) ∈ P ) )
17 enreceq ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ↔ ( 𝑧 +P 𝐵 ) = ( 𝑤 +P 𝐴 ) ) )
18 enreceq ⊢ ( ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ↔ ( 𝑣 +P 𝐷 ) = ( 𝑢 +P 𝐶 ) ) )
19 eqcom ⊢ ( ( 𝑣 +P 𝐷 ) = ( 𝑢 +P 𝐶 ) ↔ ( 𝑢 +P 𝐶 ) = ( 𝑣 +P 𝐷 ) )
20 18 19 bitrdi ⊢ ( ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ↔ ( 𝑢 +P 𝐶 ) = ( 𝑣 +P 𝐷 ) ) )
21 17 20 bi2anan9 ⊢ ( ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ) ∧ ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ) → ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) ↔ ( ( 𝑧 +P 𝐵 ) = ( 𝑤 +P 𝐴 ) ∧ ( 𝑢 +P 𝐶 ) = ( 𝑣 +P 𝐷 ) ) ) )
22 oveq12 ⊢ ( ( ( 𝑧 +P 𝐵 ) = ( 𝑤 +P 𝐴 ) ∧ ( 𝑢 +P 𝐶 ) = ( 𝑣 +P 𝐷 ) ) → ( ( 𝑧 +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 addcompr ⊢ ( 𝑣 +P 𝐴 ) = ( 𝐴 +P 𝑣 )
33 32 oveq1i ⊢ ( ( 𝑣 +P 𝐴 ) +P 𝐷 ) = ( ( 𝐴 +P 𝑣 ) +P 𝐷 )
34 addasspr ⊢ ( ( 𝑣 +P 𝐴 ) +P 𝐷 ) = ( 𝑣 +P ( 𝐴 +P 𝐷 ) )
35 addasspr ⊢ ( ( 𝐴 +P 𝑣 ) +P 𝐷 ) = ( 𝐴 +P ( 𝑣 +P 𝐷 ) )
36 33 34 35 3eqtr3i ⊢ ( 𝑣 +P ( 𝐴 +P 𝐷 ) ) = ( 𝐴 +P ( 𝑣 +P 𝐷 ) )
37 36 oveq2i ⊢ ( 𝑤 +P ( 𝑣 +P ( 𝐴 +P 𝐷 ) ) ) = ( 𝑤 +P ( 𝐴 +P ( 𝑣 +P 𝐷 ) ) )
38 addasspr ⊢ ( ( 𝑤 +P 𝑣 ) +P ( 𝐴 +P 𝐷 ) ) = ( 𝑤 +P ( 𝑣 +P ( 𝐴 +P 𝐷 ) ) )
39 addasspr ⊢ ( ( 𝑤 +P 𝐴 ) +P ( 𝑣 +P 𝐷 ) ) = ( 𝑤 +P ( 𝐴 +P ( 𝑣 +P 𝐷 ) ) )
40 37 38 39 3eqtr4i ⊢ ( ( 𝑤 +P 𝑣 ) +P ( 𝐴 +P 𝐷 ) ) = ( ( 𝑤 +P 𝐴 ) +P ( 𝑣 +P 𝐷 ) )
41 22 31 40 3eqtr4g ⊢ ( ( ( 𝑧 +P 𝐵 ) = ( 𝑤 +P 𝐴 ) ∧ ( 𝑢 +P 𝐶 ) = ( 𝑣 +P 𝐷 ) ) → ( ( 𝑧 +P 𝑢 ) +P ( 𝐵 +P 𝐶 ) ) = ( ( 𝑤 +P 𝑣 ) +P ( 𝐴 +P 𝐷 ) ) )
42 21 41 syl6bi ⊢ ( ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ) ∧ ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ) → ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) → ( ( 𝑧 +P 𝑢 ) +P ( 𝐵 +P 𝐶 ) ) = ( ( 𝑤 +P 𝑣 ) +P ( 𝐴 +P 𝐷 ) ) ) )
43 ovex ⊢ ( 𝑧 +P 𝑢 ) ∈ V
44 ovex ⊢ ( 𝐵 +P 𝐶 ) ∈ V
45 ltapr ⊢ ( 𝑓 ∈ P → ( 𝑥 <P 𝑦 ↔ ( 𝑓 +P 𝑥 ) <P ( 𝑓 +P 𝑦 ) ) )
46 ovex ⊢ ( 𝑤 +P 𝑣 ) ∈ V
47 addcompr ⊢ ( 𝑥 +P 𝑦 ) = ( 𝑦 +P 𝑥 )
48 ovex ⊢ ( 𝐴 +P 𝐷 ) ∈ V
49 43 44 45 46 47 48 caovord3 ⊢ ( ( ( ( 𝐵 +P 𝐶 ) ∈ P ∧ ( 𝑤 +P 𝑣 ) ∈ P ) ∧ ( ( 𝑧 +P 𝑢 ) +P ( 𝐵 +P 𝐶 ) ) = ( ( 𝑤 +P 𝑣 ) +P ( 𝐴 +P 𝐷 ) ) ) → ( ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) ↔ ( 𝐴 +P 𝐷 ) <P ( 𝐵 +P 𝐶 ) ) )
50 16 42 49 syl6an ⊢ ( ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ) ∧ ( ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ) → ( ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R ∧ [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) → ( ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) ↔ ( 𝐴 +P 𝐷 ) <P ( 𝐵 +P 𝐶 ) ) ) )
51 9 1 4 10 50 brecop ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R <R [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ↔ ( 𝐴 +P 𝐷 ) <P ( 𝐵 +P 𝐶 ) ) )
52 3 4 5 6 7 8 51 brecop2 ⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R <R [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ↔ ( 𝐴 +P 𝐷 ) <P ( 𝐵 +P 𝐶 ) )