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

Metamath Proof Explorer

Theorem map2psrpr

Description: Equivalence for positive signed real. (Contributed by NM, 17-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypothesis map2psrpr.2 ⊢ 𝐶 ∈ R
Assertion map2psrpr ( ( 𝐶 +R -1R ) <R 𝐴 ↔ ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 map2psrpr.2 ⊢ 𝐶 ∈ R
2 ltrelsr ⊢ <R ⊆ ( R × R )
3 2 brel ⊢ ( ( 𝐶 +R -1R ) <R 𝐴 → ( ( 𝐶 +R -1R ) ∈ R ∧ 𝐴 ∈ R ) )
4 3 simprd ⊢ ( ( 𝐶 +R -1R ) <R 𝐴 → 𝐴 ∈ R )
5 ltasr ⊢ ( 𝐶 ∈ R → ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ↔ ( 𝐶 +R -1R ) <R ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) ) )
6 1 5 ax-mp ⊢ ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ↔ ( 𝐶 +R -1R ) <R ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
7 pn0sr ⊢ ( 𝐶 ∈ R → ( 𝐶 +R ( 𝐶 ·R -1R ) ) = 0R )
8 1 7 ax-mp ⊢ ( 𝐶 +R ( 𝐶 ·R -1R ) ) = 0R
9 8 oveq1i ⊢ ( ( 𝐶 +R ( 𝐶 ·R -1R ) ) +R 𝐴 ) = ( 0R +R 𝐴 )
10 addasssr ⊢ ( ( 𝐶 +R ( 𝐶 ·R -1R ) ) +R 𝐴 ) = ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) )
11 addcomsr ⊢ ( 0R +R 𝐴 ) = ( 𝐴 +R 0R )
12 9 10 11 3eqtr3i ⊢ ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) = ( 𝐴 +R 0R )
13 0idsr ⊢ ( 𝐴 ∈ R → ( 𝐴 +R 0R ) = 𝐴 )
14 12 13 eqtrid ⊢ ( 𝐴 ∈ R → ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) = 𝐴 )
15 14 breq2d ⊢ ( 𝐴 ∈ R → ( ( 𝐶 +R -1R ) <R ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) ↔ ( 𝐶 +R -1R ) <R 𝐴 ) )
16 6 15 bitrid ⊢ ( 𝐴 ∈ R → ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ↔ ( 𝐶 +R -1R ) <R 𝐴 ) )
17 m1r ⊢ -1R ∈ R
18 mulclsr ⊢ ( ( 𝐶 ∈ R ∧ -1R ∈ R ) → ( 𝐶 ·R -1R ) ∈ R )
19 1 17 18 mp2an ⊢ ( 𝐶 ·R -1R ) ∈ R
20 addclsr ⊢ ( ( ( 𝐶 ·R -1R ) ∈ R ∧ 𝐴 ∈ R ) → ( ( 𝐶 ·R -1R ) +R 𝐴 ) ∈ R )
21 19 20 mpan ⊢ ( 𝐴 ∈ R → ( ( 𝐶 ·R -1R ) +R 𝐴 ) ∈ R )
22 df-nr ⊢ R = ( ( P × P ) / ~R )
23 breq2 ⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
24 eqeq2 ⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
25 24 rexbidv ⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
26 23 25 imbi12d ⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ) ↔ ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) ) )
27 df-m1r ⊢ -1R = [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R
28 27 breq1i ⊢ ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R )
29 addasspr ⊢ ( ( 1P +P 1P ) +P 𝑦 ) = ( 1P +P ( 1P +P 𝑦 ) )
30 29 breq2i ⊢ ( ( 1P +P 𝑧 ) <P ( ( 1P +P 1P ) +P 𝑦 ) ↔ ( 1P +P 𝑧 ) <P ( 1P +P ( 1P +P 𝑦 ) ) )
31 ltsrpr ⊢ ( [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ( 1P +P 𝑧 ) <P ( ( 1P +P 1P ) +P 𝑦 ) )
32 1pr ⊢ 1P ∈ P
33 ltapr ⊢ ( 1P ∈ P → ( 𝑧 <P ( 1P +P 𝑦 ) ↔ ( 1P +P 𝑧 ) <P ( 1P +P ( 1P +P 𝑦 ) ) ) )
34 32 33 ax-mp ⊢ ( 𝑧 <P ( 1P +P 𝑦 ) ↔ ( 1P +P 𝑧 ) <P ( 1P +P ( 1P +P 𝑦 ) ) )
35 30 31 34 3bitr4i ⊢ ( [ ⟨ 1P , ( 1P +P 1P ) ⟩ ] ~R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ 𝑧 <P ( 1P +P 𝑦 ) )
36 28 35 bitri ⊢ ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ 𝑧 <P ( 1P +P 𝑦 ) )
37 ltexpri ⊢ ( 𝑧 <P ( 1P +P 𝑦 ) → ∃ 𝑥 ∈ P ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) )
38 36 37 sylbi ⊢ ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑥 ∈ P ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) )
39 enreceq ⊢ ( ( ( 𝑥 ∈ P ∧ 1P ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ( 𝑥 +P 𝑧 ) = ( 1P +P 𝑦 ) ) )
40 32 39 mpanl2 ⊢ ( ( 𝑥 ∈ P ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ( 𝑥 +P 𝑧 ) = ( 1P +P 𝑦 ) ) )
41 addcompr ⊢ ( 𝑧 +P 𝑥 ) = ( 𝑥 +P 𝑧 )
42 41 eqeq1i ⊢ ( ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) ↔ ( 𝑥 +P 𝑧 ) = ( 1P +P 𝑦 ) )
43 40 42 bitr4di ⊢ ( ( 𝑥 ∈ P ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) ) )
44 43 ancoms ⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑥 ∈ P ) → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) ) )
45 44 rexbidva ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ ∃ 𝑥 ∈ P ( 𝑧 +P 𝑥 ) = ( 1P +P 𝑦 ) ) )
46 38 45 imbitrrid ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( -1R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ) )
47 22 26 46 ecoptocl ⊢ ( ( ( 𝐶 ·R -1R ) +R 𝐴 ) ∈ R → ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
48 21 47 syl ⊢ ( 𝐴 ∈ R → ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
49 oveq2 ⊢ ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = ( 𝐶 +R ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) )
50 49 14 sylan9eqr ⊢ ( ( 𝐴 ∈ R ∧ [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) ) → ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 )
51 50 ex ⊢ ( 𝐴 ∈ R → ( [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 ) )
52 51 reximdv ⊢ ( 𝐴 ∈ R → ( ∃ 𝑥 ∈ P [ ⟨ 𝑥 , 1P ⟩ ] ~R = ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 ) )
53 48 52 syld ⊢ ( 𝐴 ∈ R → ( -1R <R ( ( 𝐶 ·R -1R ) +R 𝐴 ) → ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 ) )
54 16 53 sylbird ⊢ ( 𝐴 ∈ R → ( ( 𝐶 +R -1R ) <R 𝐴 → ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 ) )
55 4 54 mpcom ⊢ ( ( 𝐶 +R -1R ) <R 𝐴 → ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 )
56 1 mappsrpr ⊢ ( ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) ↔ 𝑥 ∈ P )
57 breq2 ⊢ ( ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 → ( ( 𝐶 +R -1R ) <R ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) ↔ ( 𝐶 +R -1R ) <R 𝐴 ) )
58 56 57 bitr3id ⊢ ( ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 → ( 𝑥 ∈ P ↔ ( 𝐶 +R -1R ) <R 𝐴 ) )
59 58 biimpac ⊢ ( ( 𝑥 ∈ P ∧ ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 ) → ( 𝐶 +R -1R ) <R 𝐴 )
60 59 rexlimiva ⊢ ( ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 → ( 𝐶 +R -1R ) <R 𝐴 )
61 55 60 impbii ⊢ ( ( 𝐶 +R -1R ) <R 𝐴 ↔ ∃ 𝑥 ∈ P ( 𝐶 +R [ ⟨ 𝑥 , 1P ⟩ ] ~R ) = 𝐴 )