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 syl5eq ⊢ ( ( ( 𝐴 ∈ 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 syl5eq ⊢ ( ( ( ( 𝐴 ∈ 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 𝐵 ) ) )