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 syl5rbb 
 |-  ( 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 syl5eq 
 |-  ( 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 )