Metamath Proof Explorer

Theorem mulclprlem

Description: Lemma to prove downward closure in positive real multiplication. Part of proof of Proposition 9-3.7 of Gleason p. 124. (Contributed by NM, 14-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion mulclprlem 
|- ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  x e. ( A .P. B ) ) )

Proof

Step Hyp Ref Expression
1 elprnq 
 |-  ( ( A e. P. /\ g e. A ) -> g e. Q. )
2 elprnq 
 |-  ( ( B e. P. /\ h e. B ) -> h e. Q. )
3 recclnq 
 |-  ( h e. Q. -> ( *Q ` h ) e. Q. )
4 3 adantl 
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( *Q ` h ) e. Q. )
5 vex 
 |-  x e. _V
6 ovex 
 |-  ( g .Q h ) e. _V
7 ltmnq 
 |-  ( w e. Q. -> ( y  ( w .Q y )
8 fvex 
 |-  ( *Q ` h ) e. _V
9 mulcomnq 
 |-  ( y .Q z ) = ( z .Q y )
10 5 6 7 8 9 caovord2 
 |-  ( ( *Q ` h ) e. Q. -> ( x  ( x .Q ( *Q ` h ) )
11 4 10 syl 
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( x  ( x .Q ( *Q ` h ) )
12 mulassnq 
 |-  ( ( g .Q h ) .Q ( *Q ` h ) ) = ( g .Q ( h .Q ( *Q ` h ) ) )
13 recidnq 
 |-  ( h e. Q. -> ( h .Q ( *Q ` h ) ) = 1Q )
14 13 oveq2d 
 |-  ( h e. Q. -> ( g .Q ( h .Q ( *Q ` h ) ) ) = ( g .Q 1Q ) )
15 12 14 syl5eq 
 |-  ( h e. Q. -> ( ( g .Q h ) .Q ( *Q ` h ) ) = ( g .Q 1Q ) )
16 mulidnq 
 |-  ( g e. Q. -> ( g .Q 1Q ) = g )
17 15 16 sylan9eqr 
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( ( g .Q h ) .Q ( *Q ` h ) ) = g )
18 17 breq2d 
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( ( x .Q ( *Q ` h ) )  ( x .Q ( *Q ` h ) )
19 11 18 bitrd 
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( x  ( x .Q ( *Q ` h ) )
20 1 2 19 syl2an 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( x  ( x .Q ( *Q ` h ) )
21 prcdnq 
 |-  ( ( A e. P. /\ g e. A ) -> ( ( x .Q ( *Q ` h ) )  ( x .Q ( *Q ` h ) ) e. A ) )
22 21 adantr 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( ( x .Q ( *Q ` h ) )  ( x .Q ( *Q ` h ) ) e. A ) )
23 20 22 sylbid 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( x  ( x .Q ( *Q ` h ) ) e. A ) )
24 df-mp 
 |-  .P. = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y .Q z ) } )
25 mulclnq 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y .Q z ) e. Q. )
26 24 25 genpprecl 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( ( x .Q ( *Q ` h ) ) e. A /\ h e. B ) -> ( ( x .Q ( *Q ` h ) ) .Q h ) e. ( A .P. B ) ) )
27 26 exp4b 
 |-  ( A e. P. -> ( B e. P. -> ( ( x .Q ( *Q ` h ) ) e. A -> ( h e. B -> ( ( x .Q ( *Q ` h ) ) .Q h ) e. ( A .P. B ) ) ) ) )
28 27 com34 
 |-  ( A e. P. -> ( B e. P. -> ( h e. B -> ( ( x .Q ( *Q ` h ) ) e. A -> ( ( x .Q ( *Q ` h ) ) .Q h ) e. ( A .P. B ) ) ) ) )
29 28 imp32 
 |-  ( ( A e. P. /\ ( B e. P. /\ h e. B ) ) -> ( ( x .Q ( *Q ` h ) ) e. A -> ( ( x .Q ( *Q ` h ) ) .Q h ) e. ( A .P. B ) ) )
30 29 adantlr 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( ( x .Q ( *Q ` h ) ) e. A -> ( ( x .Q ( *Q ` h ) ) .Q h ) e. ( A .P. B ) ) )
31 23 30 syld 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( x  ( ( x .Q ( *Q ` h ) ) .Q h ) e. ( A .P. B ) ) )
32 31 adantr 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` h ) ) .Q h ) e. ( A .P. B ) ) )
33 2 adantl 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> h e. Q. )
34 mulassnq 
 |-  ( ( x .Q ( *Q ` h ) ) .Q h ) = ( x .Q ( ( *Q ` h ) .Q h ) )
35 mulcomnq 
 |-  ( ( *Q ` h ) .Q h ) = ( h .Q ( *Q ` h ) )
36 35 13 syl5eq 
 |-  ( h e. Q. -> ( ( *Q ` h ) .Q h ) = 1Q )
37 36 oveq2d 
 |-  ( h e. Q. -> ( x .Q ( ( *Q ` h ) .Q h ) ) = ( x .Q 1Q ) )
38 34 37 syl5eq 
 |-  ( h e. Q. -> ( ( x .Q ( *Q ` h ) ) .Q h ) = ( x .Q 1Q ) )
39 mulidnq 
 |-  ( x e. Q. -> ( x .Q 1Q ) = x )
40 38 39 sylan9eq 
 |-  ( ( h e. Q. /\ x e. Q. ) -> ( ( x .Q ( *Q ` h ) ) .Q h ) = x )
41 40 eleq1d 
 |-  ( ( h e. Q. /\ x e. Q. ) -> ( ( ( x .Q ( *Q ` h ) ) .Q h ) e. ( A .P. B ) <-> x e. ( A .P. B ) ) )
42 33 41 sylan 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( ( ( x .Q ( *Q ` h ) ) .Q h ) e. ( A .P. B ) <-> x e. ( A .P. B ) ) )
43 32 42 sylibd 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  x e. ( A .P. B ) ) )