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
|- ( A e. P. -> ( A .P. 1P ) = A )

Proof

Step Hyp Ref Expression
1 df-rex
 |-  ( E. g e. 1P x = ( f .Q g ) <-> E. g ( g e. 1P /\ x = ( f .Q g ) ) )
2 elprnq
 |-  ( ( A e. P. /\ f e. A ) -> f e. Q. )
3 breq1
 |-  ( x = ( f .Q g ) -> ( x  ( f .Q g ) 
4 df-1p
 |-  1P = { g | g 
5 4 abeq2i
 |-  ( g e. 1P <-> g 
6 ltmnq
 |-  ( f e. Q. -> ( g  ( f .Q g ) 
7 mulidnq
 |-  ( f e. Q. -> ( f .Q 1Q ) = f )
8 7 breq2d
 |-  ( f e. Q. -> ( ( f .Q g )  ( f .Q g ) 
9 6 8 bitrd
 |-  ( f e. Q. -> ( g  ( f .Q g ) 
10 5 9 bitr2id
 |-  ( f e. Q. -> ( ( f .Q g )  g e. 1P ) )
11 3 10 sylan9bbr
 |-  ( ( f e. Q. /\ x = ( f .Q g ) ) -> ( x  g e. 1P ) )
12 2 11 sylan
 |-  ( ( ( A e. P. /\ f e. A ) /\ x = ( f .Q g ) ) -> ( x  g e. 1P ) )
13 12 ex
 |-  ( ( A e. P. /\ f e. A ) -> ( x = ( f .Q g ) -> ( x  g e. 1P ) ) )
14 13 pm5.32rd
 |-  ( ( A e. P. /\ f e. A ) -> ( ( x  ( g e. 1P /\ x = ( f .Q g ) ) ) )
15 14 exbidv
 |-  ( ( A e. P. /\ f e. A ) -> ( E. g ( x  E. g ( g e. 1P /\ x = ( f .Q g ) ) ) )
16 19.42v
 |-  ( E. g ( x  ( x 
17 15 16 bitr3di
 |-  ( ( A e. P. /\ f e. A ) -> ( E. g ( g e. 1P /\ x = ( f .Q g ) ) <-> ( x 
18 1 17 syl5bb
 |-  ( ( A e. P. /\ f e. A ) -> ( E. g e. 1P x = ( f .Q g ) <-> ( x 
19 18 rexbidva
 |-  ( A e. P. -> ( E. f e. A E. g e. 1P x = ( f .Q g ) <-> E. f e. A ( x 
20 1pr
 |-  1P e. P.
21 df-mp
 |-  .P. = ( y e. P. , z e. P. |-> { w | E. u e. y E. v e. z w = ( u .Q v ) } )
22 mulclnq
 |-  ( ( u e. Q. /\ v e. Q. ) -> ( u .Q v ) e. Q. )
23 21 22 genpelv
 |-  ( ( A e. P. /\ 1P e. P. ) -> ( x e. ( A .P. 1P ) <-> E. f e. A E. g e. 1P x = ( f .Q g ) ) )
24 20 23 mpan2
 |-  ( A e. P. -> ( x e. ( A .P. 1P ) <-> E. f e. A E. g e. 1P x = ( f .Q g ) ) )
25 prnmax
 |-  ( ( A e. P. /\ x e. A ) -> E. f e. A x 
26 ltrelnq
 |-  
27 26 brel
 |-  ( x  ( x e. Q. /\ f e. Q. ) )
28 vex
 |-  f e. _V
29 vex
 |-  x e. _V
30 fvex
 |-  ( *Q ` f ) e. _V
31 mulcomnq
 |-  ( y .Q z ) = ( z .Q y )
32 mulassnq
 |-  ( ( y .Q z ) .Q w ) = ( y .Q ( z .Q w ) )
33 28 29 30 31 32 caov12
 |-  ( f .Q ( x .Q ( *Q ` f ) ) ) = ( x .Q ( f .Q ( *Q ` f ) ) )
34 recidnq
 |-  ( f e. Q. -> ( f .Q ( *Q ` f ) ) = 1Q )
35 34 oveq2d
 |-  ( f e. Q. -> ( x .Q ( f .Q ( *Q ` f ) ) ) = ( x .Q 1Q ) )
36 33 35 eqtrid
 |-  ( f e. Q. -> ( f .Q ( x .Q ( *Q ` f ) ) ) = ( x .Q 1Q ) )
37 mulidnq
 |-  ( x e. Q. -> ( x .Q 1Q ) = x )
38 36 37 sylan9eqr
 |-  ( ( x e. Q. /\ f e. Q. ) -> ( f .Q ( x .Q ( *Q ` f ) ) ) = x )
39 38 eqcomd
 |-  ( ( x e. Q. /\ f e. Q. ) -> x = ( f .Q ( x .Q ( *Q ` f ) ) ) )
40 ovex
 |-  ( x .Q ( *Q ` f ) ) e. _V
41 oveq2
 |-  ( g = ( x .Q ( *Q ` f ) ) -> ( f .Q g ) = ( f .Q ( x .Q ( *Q ` f ) ) ) )
42 41 eqeq2d
 |-  ( g = ( x .Q ( *Q ` f ) ) -> ( x = ( f .Q g ) <-> x = ( f .Q ( x .Q ( *Q ` f ) ) ) ) )
43 40 42 spcev
 |-  ( x = ( f .Q ( x .Q ( *Q ` f ) ) ) -> E. g x = ( f .Q g ) )
44 27 39 43 3syl
 |-  ( x  E. g x = ( f .Q g ) )
45 44 a1i
 |-  ( f e. A -> ( x  E. g x = ( f .Q g ) ) )
46 45 ancld
 |-  ( f e. A -> ( x  ( x 
47 46 reximia
 |-  ( E. f e. A x  E. f e. A ( x 
48 25 47 syl
 |-  ( ( A e. P. /\ x e. A ) -> E. f e. A ( x 
49 48 ex
 |-  ( A e. P. -> ( x e. A -> E. f e. A ( x 
50 prcdnq
 |-  ( ( A e. P. /\ f e. A ) -> ( x  x e. A ) )
51 50 adantrd
 |-  ( ( A e. P. /\ f e. A ) -> ( ( x  x e. A ) )
52 51 rexlimdva
 |-  ( A e. P. -> ( E. f e. A ( x  x e. A ) )
53 49 52 impbid
 |-  ( A e. P. -> ( x e. A <-> E. f e. A ( x 
54 19 24 53 3bitr4d
 |-  ( A e. P. -> ( x e. ( A .P. 1P ) <-> x e. A ) )
55 54 eqrdv
 |-  ( A e. P. -> ( A .P. 1P ) = A )