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 ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 ·Q ℎ ) → 𝑥 ∈ ( 𝐴 ·P 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 elprnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) → 𝑔 ∈ Q )
2 elprnq ⊢ ( ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) → ℎ ∈ Q )
3 recclnq ⊢ ( ℎ ∈ Q → ( *Q ‘ ℎ ) ∈ Q )
4 3 adantl ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( *Q ‘ ℎ ) ∈ Q )
5 vex ⊢ 𝑥 ∈ V
6 ovex ⊢ ( 𝑔 ·Q ℎ ) ∈ V
7 ltmnq ⊢ ( 𝑤 ∈ Q → ( 𝑦 <Q 𝑧 ↔ ( 𝑤 ·Q 𝑦 ) <Q ( 𝑤 ·Q 𝑧 ) ) )
8 fvex ⊢ ( *Q ‘ ℎ ) ∈ V
9 mulcomnq ⊢ ( 𝑦 ·Q 𝑧 ) = ( 𝑧 ·Q 𝑦 )
10 5 6 7 8 9 caovord2 ⊢ ( ( *Q ‘ ℎ ) ∈ Q → ( 𝑥 <Q ( 𝑔 ·Q ℎ ) ↔ ( 𝑥 ·Q ( *Q ‘ ℎ ) ) <Q ( ( 𝑔 ·Q ℎ ) ·Q ( *Q ‘ ℎ ) ) ) )
11 4 10 syl ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑥 <Q ( 𝑔 ·Q ℎ ) ↔ ( 𝑥 ·Q ( *Q ‘ ℎ ) ) <Q ( ( 𝑔 ·Q ℎ ) ·Q ( *Q ‘ ℎ ) ) ) )
12 mulassnq ⊢ ( ( 𝑔 ·Q ℎ ) ·Q ( *Q ‘ ℎ ) ) = ( 𝑔 ·Q ( ℎ ·Q ( *Q ‘ ℎ ) ) )
13 recidnq ⊢ ( ℎ ∈ Q → ( ℎ ·Q ( *Q ‘ ℎ ) ) = 1Q )
14 13 oveq2d ⊢ ( ℎ ∈ Q → ( 𝑔 ·Q ( ℎ ·Q ( *Q ‘ ℎ ) ) ) = ( 𝑔 ·Q 1Q ) )
15 12 14 syl5eq ⊢ ( ℎ ∈ Q → ( ( 𝑔 ·Q ℎ ) ·Q ( *Q ‘ ℎ ) ) = ( 𝑔 ·Q 1Q ) )
16 mulidnq ⊢ ( 𝑔 ∈ Q → ( 𝑔 ·Q 1Q ) = 𝑔 )
17 15 16 sylan9eqr ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( ( 𝑔 ·Q ℎ ) ·Q ( *Q ‘ ℎ ) ) = 𝑔 )
18 17 breq2d ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) <Q ( ( 𝑔 ·Q ℎ ) ·Q ( *Q ‘ ℎ ) ) ↔ ( 𝑥 ·Q ( *Q ‘ ℎ ) ) <Q 𝑔 ) )
19 11 18 bitrd ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑥 <Q ( 𝑔 ·Q ℎ ) ↔ ( 𝑥 ·Q ( *Q ‘ ℎ ) ) <Q 𝑔 ) )
20 1 2 19 syl2an ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( 𝑥 <Q ( 𝑔 ·Q ℎ ) ↔ ( 𝑥 ·Q ( *Q ‘ ℎ ) ) <Q 𝑔 ) )
21 prcdnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) <Q 𝑔 → ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ∈ 𝐴 ) )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) <Q 𝑔 → ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ∈ 𝐴 ) )
23 20 22 sylbid ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( 𝑥 <Q ( 𝑔 ·Q ℎ ) → ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ∈ 𝐴 ) )
24 df-mp ⊢ ·P = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 ·Q 𝑧 ) } )
25 mulclnq ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 ·Q 𝑧 ) ∈ Q )
26 24 25 genpprecl ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) ∈ ( 𝐴 ·P 𝐵 ) ) )
27 26 exp4b ⊢ ( 𝐴 ∈ P → ( 𝐵 ∈ P → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ∈ 𝐴 → ( ℎ ∈ 𝐵 → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) ∈ ( 𝐴 ·P 𝐵 ) ) ) ) )
28 27 com34 ⊢ ( 𝐴 ∈ P → ( 𝐵 ∈ P → ( ℎ ∈ 𝐵 → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ∈ 𝐴 → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) ∈ ( 𝐴 ·P 𝐵 ) ) ) ) )
29 28 imp32 ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ∈ 𝐴 → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) ∈ ( 𝐴 ·P 𝐵 ) ) )
30 29 adantlr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ∈ 𝐴 → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) ∈ ( 𝐴 ·P 𝐵 ) ) )
31 23 30 syld ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( 𝑥 <Q ( 𝑔 ·Q ℎ ) → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) ∈ ( 𝐴 ·P 𝐵 ) ) )
32 31 adantr ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 ·Q ℎ ) → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) ∈ ( 𝐴 ·P 𝐵 ) ) )
33 2 adantl ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ℎ ∈ Q )
34 mulassnq ⊢ ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) = ( 𝑥 ·Q ( ( *Q ‘ ℎ ) ·Q ℎ ) )
35 mulcomnq ⊢ ( ( *Q ‘ ℎ ) ·Q ℎ ) = ( ℎ ·Q ( *Q ‘ ℎ ) )
36 35 13 syl5eq ⊢ ( ℎ ∈ Q → ( ( *Q ‘ ℎ ) ·Q ℎ ) = 1Q )
37 36 oveq2d ⊢ ( ℎ ∈ Q → ( 𝑥 ·Q ( ( *Q ‘ ℎ ) ·Q ℎ ) ) = ( 𝑥 ·Q 1Q ) )
38 34 37 syl5eq ⊢ ( ℎ ∈ Q → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) = ( 𝑥 ·Q 1Q ) )
39 mulidnq ⊢ ( 𝑥 ∈ Q → ( 𝑥 ·Q 1Q ) = 𝑥 )
40 38 39 sylan9eq ⊢ ( ( ℎ ∈ Q ∧ 𝑥 ∈ Q ) → ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) = 𝑥 )
41 40 eleq1d ⊢ ( ( ℎ ∈ Q ∧ 𝑥 ∈ Q ) → ( ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) ∈ ( 𝐴 ·P 𝐵 ) ↔ 𝑥 ∈ ( 𝐴 ·P 𝐵 ) ) )
42 33 41 sylan ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) → ( ( ( 𝑥 ·Q ( *Q ‘ ℎ ) ) ·Q ℎ ) ∈ ( 𝐴 ·P 𝐵 ) ↔ 𝑥 ∈ ( 𝐴 ·P 𝐵 ) ) )
43 32 42 sylibd ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 ·Q ℎ ) → 𝑥 ∈ ( 𝐴 ·P 𝐵 ) ) )