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

Metamath Proof Explorer

Theorem 1idpr

Description: 1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of Gleason p. 124. (Contributed by NM, 2-Apr-1996) (New usage is discouraged.)

Ref Expression
Assertion 1idpr ( 𝐴 ∈ P → ( 𝐴 ·P 1P ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 df-rex ⊢ ( ∃ 𝑔 ∈ 1P 𝑥 = ( 𝑓 ·Q 𝑔 ) ↔ ∃ 𝑔 ( 𝑔 ∈ 1P ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
2 elprnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ Q )
3 breq1 ⊢ ( 𝑥 = ( 𝑓 ·Q 𝑔 ) → ( 𝑥 <Q 𝑓 ↔ ( 𝑓 ·Q 𝑔 ) <Q 𝑓 ) )
4 df-1p ⊢ 1P = { 𝑔 ∣ 𝑔 <Q 1Q }
5 4 eqabri ⊢ ( 𝑔 ∈ 1P ↔ 𝑔 <Q 1Q )
6 ltmnq ⊢ ( 𝑓 ∈ Q → ( 𝑔 <Q 1Q ↔ ( 𝑓 ·Q 𝑔 ) <Q ( 𝑓 ·Q 1Q ) ) )
7 mulidnq ⊢ ( 𝑓 ∈ Q → ( 𝑓 ·Q 1Q ) = 𝑓 )
8 7 breq2d ⊢ ( 𝑓 ∈ Q → ( ( 𝑓 ·Q 𝑔 ) <Q ( 𝑓 ·Q 1Q ) ↔ ( 𝑓 ·Q 𝑔 ) <Q 𝑓 ) )
9 6 8 bitrd ⊢ ( 𝑓 ∈ Q → ( 𝑔 <Q 1Q ↔ ( 𝑓 ·Q 𝑔 ) <Q 𝑓 ) )
10 5 9 bitr2id ⊢ ( 𝑓 ∈ Q → ( ( 𝑓 ·Q 𝑔 ) <Q 𝑓 ↔ 𝑔 ∈ 1P ) )
11 3 10 sylan9bbr ⊢ ( ( 𝑓 ∈ Q ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) → ( 𝑥 <Q 𝑓 ↔ 𝑔 ∈ 1P ) )
12 2 11 sylan ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) → ( 𝑥 <Q 𝑓 ↔ 𝑔 ∈ 1P ) )
13 12 ex ⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( 𝑥 = ( 𝑓 ·Q 𝑔 ) → ( 𝑥 <Q 𝑓 ↔ 𝑔 ∈ 1P ) ) )
14 13 pm5.32rd ⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( ( 𝑥 <Q 𝑓 ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ↔ ( 𝑔 ∈ 1P ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
15 14 exbidv ⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( ∃ 𝑔 ( 𝑥 <Q 𝑓 ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ↔ ∃ 𝑔 ( 𝑔 ∈ 1P ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
16 19.42v ⊢ ( ∃ 𝑔 ( 𝑥 <Q 𝑓 ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ↔ ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
17 15 16 bitr3di ⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( ∃ 𝑔 ( 𝑔 ∈ 1P ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ↔ ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
18 1 17 bitrid ⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( ∃ 𝑔 ∈ 1P 𝑥 = ( 𝑓 ·Q 𝑔 ) ↔ ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
19 18 rexbidva ⊢ ( 𝐴 ∈ P → ( ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 1P 𝑥 = ( 𝑓 ·Q 𝑔 ) ↔ ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
20 1pr ⊢ 1P ∈ P
21 df-mp ⊢ ·P = ( 𝑦 ∈ P , 𝑧 ∈ P ↦ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑦 ∃ 𝑣 ∈ 𝑧 𝑤 = ( 𝑢 ·Q 𝑣 ) } )
22 mulclnq ⊢ ( ( 𝑢 ∈ Q ∧ 𝑣 ∈ Q ) → ( 𝑢 ·Q 𝑣 ) ∈ Q )
23 21 22 genpelv ⊢ ( ( 𝐴 ∈ P ∧ 1P ∈ P ) → ( 𝑥 ∈ ( 𝐴 ·P 1P ) ↔ ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 1P 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
24 20 23 mpan2 ⊢ ( 𝐴 ∈ P → ( 𝑥 ∈ ( 𝐴 ·P 1P ) ↔ ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 1P 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
25 prnmax ⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ∈ 𝐴 𝑥 <Q 𝑓 )
26 ltrelnq ⊢ <Q ⊆ ( Q × Q )
27 26 brel ⊢ ( 𝑥 <Q 𝑓 → ( 𝑥 ∈ Q ∧ 𝑓 ∈ Q ) )
28 vex ⊢ 𝑓 ∈ V
29 vex ⊢ 𝑥 ∈ V
30 fvex ⊢ ( *Q ‘ 𝑓 ) ∈ V
31 mulcomnq ⊢ ( 𝑦 ·Q 𝑧 ) = ( 𝑧 ·Q 𝑦 )
32 mulassnq ⊢ ( ( 𝑦 ·Q 𝑧 ) ·Q 𝑤 ) = ( 𝑦 ·Q ( 𝑧 ·Q 𝑤 ) )
33 28 29 30 31 32 caov12 ⊢ ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) = ( 𝑥 ·Q ( 𝑓 ·Q ( *Q ‘ 𝑓 ) ) )
34 recidnq ⊢ ( 𝑓 ∈ Q → ( 𝑓 ·Q ( *Q ‘ 𝑓 ) ) = 1Q )
35 34 oveq2d ⊢ ( 𝑓 ∈ Q → ( 𝑥 ·Q ( 𝑓 ·Q ( *Q ‘ 𝑓 ) ) ) = ( 𝑥 ·Q 1Q ) )
36 33 35 eqtrid ⊢ ( 𝑓 ∈ Q → ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) = ( 𝑥 ·Q 1Q ) )
37 mulidnq ⊢ ( 𝑥 ∈ Q → ( 𝑥 ·Q 1Q ) = 𝑥 )
38 36 37 sylan9eqr ⊢ ( ( 𝑥 ∈ Q ∧ 𝑓 ∈ Q ) → ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) = 𝑥 )
39 38 eqcomd ⊢ ( ( 𝑥 ∈ Q ∧ 𝑓 ∈ Q ) → 𝑥 = ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) )
40 ovex ⊢ ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ∈ V
41 oveq2 ⊢ ( 𝑔 = ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) → ( 𝑓 ·Q 𝑔 ) = ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) )
42 41 eqeq2d ⊢ ( 𝑔 = ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) → ( 𝑥 = ( 𝑓 ·Q 𝑔 ) ↔ 𝑥 = ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) ) )
43 40 42 spcev ⊢ ( 𝑥 = ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) → ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) )
44 27 39 43 3syl ⊢ ( 𝑥 <Q 𝑓 → ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) )
45 44 a1i ⊢ ( 𝑓 ∈ 𝐴 → ( 𝑥 <Q 𝑓 → ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
46 45 ancld ⊢ ( 𝑓 ∈ 𝐴 → ( 𝑥 <Q 𝑓 → ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
47 46 reximia ⊢ ( ∃ 𝑓 ∈ 𝐴 𝑥 <Q 𝑓 → ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
48 25 47 syl ⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
49 48 ex ⊢ ( 𝐴 ∈ P → ( 𝑥 ∈ 𝐴 → ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
50 prcdnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ 𝐴 ) )
51 50 adantrd ⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) → 𝑥 ∈ 𝐴 ) )
52 51 rexlimdva ⊢ ( 𝐴 ∈ P → ( ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) → 𝑥 ∈ 𝐴 ) )
53 49 52 impbid ⊢ ( 𝐴 ∈ P → ( 𝑥 ∈ 𝐴 ↔ ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
54 19 24 53 3bitr4d ⊢ ( 𝐴 ∈ P → ( 𝑥 ∈ ( 𝐴 ·P 1P ) ↔ 𝑥 ∈ 𝐴 ) )
55 54 eqrdv ⊢ ( 𝐴 ∈ P → ( 𝐴 ·P 1P ) = 𝐴 )