Metamath Proof Explorer

Theorem addclprlem2

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 addclprlem2 
|- ( ( ( ( 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 addclprlem1 
 |-  ( ( ( A e. P. /\ g e. A ) /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A ) )
2 1 adantlr 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A ) )
3 addclprlem1 
 |-  ( ( ( B e. P. /\ h e. B ) /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` ( h +Q g ) ) ) .Q h ) e. B ) )
4 addcomnq 
 |-  ( g +Q h ) = ( h +Q g )
5 4 breq2i 
 |-  ( x  x
6 4 fveq2i 
 |-  ( *Q ` ( g +Q h ) ) = ( *Q ` ( h +Q g ) )
7 6 oveq2i 
 |-  ( x .Q ( *Q ` ( g +Q h ) ) ) = ( x .Q ( *Q ` ( h +Q g ) ) )
8 7 oveq1i 
 |-  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) = ( ( x .Q ( *Q ` ( h +Q g ) ) ) .Q h )
9 8 eleq1i 
 |-  ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) e. B <-> ( ( x .Q ( *Q ` ( h +Q g ) ) ) .Q h ) e. B )
10 3 5 9 3imtr4g 
 |-  ( ( ( B e. P. /\ h e. B ) /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) e. B ) )
11 10 adantll 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) e. B ) )
12 2 11 jcad 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A /\ ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) e. B ) ) )
13 simpl 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) )
14 simpl 
 |-  ( ( A e. P. /\ g e. A ) -> A e. P. )
15 simpl 
 |-  ( ( B e. P. /\ h e. B ) -> B e. P. )
16 14 15 anim12i 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( A e. P. /\ B e. P. ) )
17 df-plp 
 |-  +P. = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y +Q z ) } )
18 addclnq 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y +Q z ) e. Q. )
19 17 18 genpprecl 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A /\ ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) e. B ) -> ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) +Q ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) ) e. ( A +P. B ) ) )
20 13 16 19 3syl 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A /\ ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) e. B ) -> ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) +Q ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) ) e. ( A +P. B ) ) )
21 12 20 syld 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) +Q ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) ) e. ( A +P. B ) ) )
22 distrnq 
 |-  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q ( g +Q h ) ) = ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) +Q ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) )
23 mulassnq 
 |-  ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q ( g +Q h ) ) = ( x .Q ( ( *Q ` ( g +Q h ) ) .Q ( g +Q h ) ) )
24 22 23 eqtr3i 
 |-  ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) +Q ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) ) = ( x .Q ( ( *Q ` ( g +Q h ) ) .Q ( g +Q h ) ) )
25 mulcomnq 
 |-  ( ( *Q ` ( g +Q h ) ) .Q ( g +Q h ) ) = ( ( g +Q h ) .Q ( *Q ` ( g +Q h ) ) )
26 elprnq 
 |-  ( ( A e. P. /\ g e. A ) -> g e. Q. )
27 elprnq 
 |-  ( ( B e. P. /\ h e. B ) -> h e. Q. )
28 26 27 anim12i 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( g e. Q. /\ h e. Q. ) )
29 addclnq 
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( g +Q h ) e. Q. )
30 recidnq 
 |-  ( ( g +Q h ) e. Q. -> ( ( g +Q h ) .Q ( *Q ` ( g +Q h ) ) ) = 1Q )
31 28 29 30 3syl 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( ( g +Q h ) .Q ( *Q ` ( g +Q h ) ) ) = 1Q )
32 25 31 syl5eq 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( ( *Q ` ( g +Q h ) ) .Q ( g +Q h ) ) = 1Q )
33 32 oveq2d 
 |-  ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) -> ( x .Q ( ( *Q ` ( g +Q h ) ) .Q ( g +Q h ) ) ) = ( x .Q 1Q ) )
34 mulidnq 
 |-  ( x e. Q. -> ( x .Q 1Q ) = x )
35 33 34 sylan9eq 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x .Q ( ( *Q ` ( g +Q h ) ) .Q ( g +Q h ) ) ) = x )
36 24 35 syl5eq 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) +Q ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) ) = x )
37 36 eleq1d 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( ( ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) +Q ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q h ) ) e. ( A +P. B ) <-> x e. ( A +P. B ) ) )
38 21 37 sylibd 
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  x e. ( A +P. B ) ) )