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 ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†’ ๐‘ฅ โˆˆ ( ๐ด +P ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 addclprlem1 โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) โˆˆ ๐ด ) )
2 1 adantlr โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) โˆˆ ๐ด ) )
3 addclprlem1 โŠข ( ( ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( โ„Ž +Q ๐‘” ) โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( โ„Ž +Q ๐‘” ) ) ) ยทQ โ„Ž ) โˆˆ ๐ต ) )
4 addcomnq โŠข ( ๐‘” +Q โ„Ž ) = ( โ„Ž +Q ๐‘” )
5 4 breq2i โŠข ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†” ๐‘ฅ <Q ( โ„Ž +Q ๐‘” ) )
6 4 fveq2i โŠข ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) = ( *Q โ€˜ ( โ„Ž +Q ๐‘” ) )
7 6 oveq2i โŠข ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) = ( ๐‘ฅ ยทQ ( *Q โ€˜ ( โ„Ž +Q ๐‘” ) ) )
8 7 oveq1i โŠข ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) = ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( โ„Ž +Q ๐‘” ) ) ) ยทQ โ„Ž )
9 8 eleq1i โŠข ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) โˆˆ ๐ต โ†” ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( โ„Ž +Q ๐‘” ) ) ) ยทQ โ„Ž ) โˆˆ ๐ต )
10 3 5 9 3imtr4g โŠข ( ( ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) โˆˆ ๐ต ) )
11 10 adantll โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) โˆˆ ๐ต ) )
12 2 11 jcad โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†’ ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) โˆˆ ๐ด โˆง ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) โˆˆ ๐ต ) ) )
13 simpl โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) )
14 simpl โŠข ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โ†’ ๐ด โˆˆ P )
15 simpl โŠข ( ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) โ†’ ๐ต โˆˆ P )
16 14 15 anim12i โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โ†’ ( ๐ด โˆˆ P โˆง ๐ต โˆˆ P ) )
17 df-plp โŠข +P = ( ๐‘ค โˆˆ P , ๐‘ฃ โˆˆ P โ†ฆ { ๐‘ฅ โˆฃ โˆƒ ๐‘ฆ โˆˆ ๐‘ค โˆƒ ๐‘ง โˆˆ ๐‘ฃ ๐‘ฅ = ( ๐‘ฆ +Q ๐‘ง ) } )
18 addclnq โŠข ( ( ๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q ) โ†’ ( ๐‘ฆ +Q ๐‘ง ) โˆˆ Q )
19 17 18 genpprecl โŠข ( ( ๐ด โˆˆ P โˆง ๐ต โˆˆ P ) โ†’ ( ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) โˆˆ ๐ด โˆง ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) โˆˆ ๐ต ) โ†’ ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) +Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) ) โˆˆ ( ๐ด +P ๐ต ) ) )
20 13 16 19 3syl โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) โˆˆ ๐ด โˆง ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) โˆˆ ๐ต ) โ†’ ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) +Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) ) โˆˆ ( ๐ด +P ๐ต ) ) )
21 12 20 syld โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†’ ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) +Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) ) โˆˆ ( ๐ด +P ๐ต ) ) )
22 distrnq โŠข ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ( ๐‘” +Q โ„Ž ) ) = ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) +Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) )
23 mulassnq โŠข ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ( ๐‘” +Q โ„Ž ) ) = ( ๐‘ฅ ยทQ ( ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ยทQ ( ๐‘” +Q โ„Ž ) ) )
24 22 23 eqtr3i โŠข ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) +Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) ) = ( ๐‘ฅ ยทQ ( ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ยทQ ( ๐‘” +Q โ„Ž ) ) )
25 mulcomnq โŠข ( ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ยทQ ( ๐‘” +Q โ„Ž ) ) = ( ( ๐‘” +Q โ„Ž ) ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) )
26 elprnq โŠข ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โ†’ ๐‘” โˆˆ Q )
27 elprnq โŠข ( ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) โ†’ โ„Ž โˆˆ Q )
28 26 27 anim12i โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โ†’ ( ๐‘” โˆˆ Q โˆง โ„Ž โˆˆ Q ) )
29 addclnq โŠข ( ( ๐‘” โˆˆ Q โˆง โ„Ž โˆˆ Q ) โ†’ ( ๐‘” +Q โ„Ž ) โˆˆ Q )
30 recidnq โŠข ( ( ๐‘” +Q โ„Ž ) โˆˆ Q โ†’ ( ( ๐‘” +Q โ„Ž ) ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) = 1Q )
31 28 29 30 3syl โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โ†’ ( ( ๐‘” +Q โ„Ž ) ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) = 1Q )
32 25 31 eqtrid โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โ†’ ( ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ยทQ ( ๐‘” +Q โ„Ž ) ) = 1Q )
33 32 oveq2d โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โ†’ ( ๐‘ฅ ยทQ ( ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ยทQ ( ๐‘” +Q โ„Ž ) ) ) = ( ๐‘ฅ ยทQ 1Q ) )
34 mulidnq โŠข ( ๐‘ฅ โˆˆ Q โ†’ ( ๐‘ฅ ยทQ 1Q ) = ๐‘ฅ )
35 33 34 sylan9eq โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ ยทQ ( ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ยทQ ( ๐‘” +Q โ„Ž ) ) ) = ๐‘ฅ )
36 24 35 eqtrid โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) +Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) ) = ๐‘ฅ )
37 36 eleq1d โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) +Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ โ„Ž ) ) โˆˆ ( ๐ด +P ๐ต ) โ†” ๐‘ฅ โˆˆ ( ๐ด +P ๐ต ) ) )
38 21 37 sylibd โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ( ๐ต โˆˆ P โˆง โ„Ž โˆˆ ๐ต ) ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†’ ๐‘ฅ โˆˆ ( ๐ด +P ๐ต ) ) )