Metamath Proof Explorer

Theorem addclprlem1

Description: Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of Gleason p. 123. (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion addclprlem1 
|- ( ( ( A e. P. /\ g e. A ) /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A ) )

Proof

Step Hyp Ref Expression
1 elprnq 
 |-  ( ( A e. P. /\ g e. A ) -> g e. Q. )
2 ltrnq 
 |-  ( x  ( *Q ` ( g +Q h ) )
3 ltmnq 
 |-  ( x e. Q. -> ( ( *Q ` ( g +Q h ) )  ( x .Q ( *Q ` ( g +Q h ) ) )
4 ovex 
 |-  ( x .Q ( *Q ` ( g +Q h ) ) ) e. _V
5 ovex 
 |-  ( x .Q ( *Q ` x ) ) e. _V
6 ltmnq 
 |-  ( w e. Q. -> ( y  ( w .Q y )
7 vex 
 |-  g e. _V
8 mulcomnq 
 |-  ( y .Q z ) = ( z .Q y )
9 4 5 6 7 8 caovord2 
 |-  ( g e. Q. -> ( ( x .Q ( *Q ` ( g +Q h ) ) )  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g )
10 3 9 sylan9bbr 
 |-  ( ( g e. Q. /\ x e. Q. ) -> ( ( *Q ` ( g +Q h ) )  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g )
11 2 10 syl5bb 
 |-  ( ( g e. Q. /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g )
12 recidnq 
 |-  ( x e. Q. -> ( x .Q ( *Q ` x ) ) = 1Q )
13 12 oveq1d 
 |-  ( x e. Q. -> ( ( x .Q ( *Q ` x ) ) .Q g ) = ( 1Q .Q g ) )
14 mulcomnq 
 |-  ( 1Q .Q g ) = ( g .Q 1Q )
15 mulidnq 
 |-  ( g e. Q. -> ( g .Q 1Q ) = g )
16 14 15 eqtrid 
 |-  ( g e. Q. -> ( 1Q .Q g ) = g )
17 13 16 sylan9eqr 
 |-  ( ( g e. Q. /\ x e. Q. ) -> ( ( x .Q ( *Q ` x ) ) .Q g ) = g )
18 17 breq2d 
 |-  ( ( g e. Q. /\ x e. Q. ) -> ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g )  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g )
19 11 18 bitrd 
 |-  ( ( g e. Q. /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g )
20 1 19 sylan 
 |-  ( ( ( A e. P. /\ g e. A ) /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g )
21 prcdnq 
 |-  ( ( A e. P. /\ g e. A ) -> ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g )  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A ) )
22 21 adantr 
 |-  ( ( ( A e. P. /\ g e. A ) /\ x e. Q. ) -> ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g )  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A ) )
23 20 22 sylbid 
 |-  ( ( ( A e. P. /\ g e. A ) /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A ) )