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 ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B ∧ x ∈ 𝑸 → x < 𝑸 g ⋅ 𝑸 h → x ∈ A ⋅ 𝑷 B

Proof

Step Hyp Ref Expression
1 elprnq ⊢ A ∈ 𝑷 ∧ g ∈ A → g ∈ 𝑸
2 elprnq ⊢ B ∈ 𝑷 ∧ h ∈ B → h ∈ 𝑸
3 recclnq ⊢ h ∈ 𝑸 → * 𝑸 ⁡ h ∈ 𝑸
4 3 adantl ⊢ g ∈ 𝑸 ∧ h ∈ 𝑸 → * 𝑸 ⁡ h ∈ 𝑸
5 vex ⊢ x ∈ V
6 ovex ⊢ g ⋅ 𝑸 h ∈ V
7 ltmnq ⊢ w ∈ 𝑸 → y < 𝑸 z ↔ w ⋅ 𝑸 y < 𝑸 w ⋅ 𝑸 z
8 fvex ⊢ * 𝑸 ⁡ h ∈ V
9 mulcomnq ⊢ y ⋅ 𝑸 z = z ⋅ 𝑸 y
10 5 6 7 8 9 caovord2 ⊢ * 𝑸 ⁡ h ∈ 𝑸 → x < 𝑸 g ⋅ 𝑸 h ↔ x ⋅ 𝑸 * 𝑸 ⁡ h < 𝑸 g ⋅ 𝑸 h ⋅ 𝑸 * 𝑸 ⁡ h
11 4 10 syl ⊢ g ∈ 𝑸 ∧ h ∈ 𝑸 → x < 𝑸 g ⋅ 𝑸 h ↔ x ⋅ 𝑸 * 𝑸 ⁡ h < 𝑸 g ⋅ 𝑸 h ⋅ 𝑸 * 𝑸 ⁡ h
12 mulassnq ⊢ g ⋅ 𝑸 h ⋅ 𝑸 * 𝑸 ⁡ h = g ⋅ 𝑸 h ⋅ 𝑸 * 𝑸 ⁡ h
13 recidnq ⊢ h ∈ 𝑸 → h ⋅ 𝑸 * 𝑸 ⁡ h = 1 𝑸
14 13 oveq2d ⊢ h ∈ 𝑸 → g ⋅ 𝑸 h ⋅ 𝑸 * 𝑸 ⁡ h = g ⋅ 𝑸 1 𝑸
15 12 14 syl5eq ⊢ h ∈ 𝑸 → g ⋅ 𝑸 h ⋅ 𝑸 * 𝑸 ⁡ h = g ⋅ 𝑸 1 𝑸
16 mulidnq ⊢ g ∈ 𝑸 → g ⋅ 𝑸 1 𝑸 = g
17 15 16 sylan9eqr ⊢ g ∈ 𝑸 ∧ h ∈ 𝑸 → g ⋅ 𝑸 h ⋅ 𝑸 * 𝑸 ⁡ h = g
18 17 breq2d ⊢ g ∈ 𝑸 ∧ h ∈ 𝑸 → x ⋅ 𝑸 * 𝑸 ⁡ h < 𝑸 g ⋅ 𝑸 h ⋅ 𝑸 * 𝑸 ⁡ h ↔ x ⋅ 𝑸 * 𝑸 ⁡ h < 𝑸 g
19 11 18 bitrd ⊢ g ∈ 𝑸 ∧ h ∈ 𝑸 → x < 𝑸 g ⋅ 𝑸 h ↔ x ⋅ 𝑸 * 𝑸 ⁡ h < 𝑸 g
20 1 2 19 syl2an ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B → x < 𝑸 g ⋅ 𝑸 h ↔ x ⋅ 𝑸 * 𝑸 ⁡ h < 𝑸 g
21 prcdnq ⊢ A ∈ 𝑷 ∧ g ∈ A → x ⋅ 𝑸 * 𝑸 ⁡ h < 𝑸 g → x ⋅ 𝑸 * 𝑸 ⁡ h ∈ A
22 21 adantr ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B → x ⋅ 𝑸 * 𝑸 ⁡ h < 𝑸 g → x ⋅ 𝑸 * 𝑸 ⁡ h ∈ A
23 20 22 sylbid ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B → x < 𝑸 g ⋅ 𝑸 h → x ⋅ 𝑸 * 𝑸 ⁡ h ∈ A
24 df-mp ⊢ ⋅ 𝑷 = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y ⋅ 𝑸 z
25 mulclnq ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y ⋅ 𝑸 z ∈ 𝑸
26 24 25 genpprecl ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → x ⋅ 𝑸 * 𝑸 ⁡ h ∈ A ∧ h ∈ B → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h ∈ A ⋅ 𝑷 B
27 26 exp4b ⊢ A ∈ 𝑷 → B ∈ 𝑷 → x ⋅ 𝑸 * 𝑸 ⁡ h ∈ A → h ∈ B → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h ∈ A ⋅ 𝑷 B
28 27 com34 ⊢ A ∈ 𝑷 → B ∈ 𝑷 → h ∈ B → x ⋅ 𝑸 * 𝑸 ⁡ h ∈ A → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h ∈ A ⋅ 𝑷 B
29 28 imp32 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ h ∈ B → x ⋅ 𝑸 * 𝑸 ⁡ h ∈ A → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h ∈ A ⋅ 𝑷 B
30 29 adantlr ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B → x ⋅ 𝑸 * 𝑸 ⁡ h ∈ A → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h ∈ A ⋅ 𝑷 B
31 23 30 syld ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B → x < 𝑸 g ⋅ 𝑸 h → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h ∈ A ⋅ 𝑷 B
32 31 adantr ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B ∧ x ∈ 𝑸 → x < 𝑸 g ⋅ 𝑸 h → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h ∈ A ⋅ 𝑷 B
33 2 adantl ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B → h ∈ 𝑸
34 mulassnq ⊢ x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h = x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h
35 mulcomnq ⊢ * 𝑸 ⁡ h ⋅ 𝑸 h = h ⋅ 𝑸 * 𝑸 ⁡ h
36 35 13 syl5eq ⊢ h ∈ 𝑸 → * 𝑸 ⁡ h ⋅ 𝑸 h = 1 𝑸
37 36 oveq2d ⊢ h ∈ 𝑸 → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h = x ⋅ 𝑸 1 𝑸
38 34 37 syl5eq ⊢ h ∈ 𝑸 → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h = x ⋅ 𝑸 1 𝑸
39 mulidnq ⊢ x ∈ 𝑸 → x ⋅ 𝑸 1 𝑸 = x
40 38 39 sylan9eq ⊢ h ∈ 𝑸 ∧ x ∈ 𝑸 → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h = x
41 40 eleq1d ⊢ h ∈ 𝑸 ∧ x ∈ 𝑸 → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h ∈ A ⋅ 𝑷 B ↔ x ∈ A ⋅ 𝑷 B
42 33 41 sylan ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B ∧ x ∈ 𝑸 → x ⋅ 𝑸 * 𝑸 ⁡ h ⋅ 𝑸 h ∈ A ⋅ 𝑷 B ↔ x ∈ A ⋅ 𝑷 B
43 32 42 sylibd ⊢ A ∈ 𝑷 ∧ g ∈ A ∧ B ∈ 𝑷 ∧ h ∈ B ∧ x ∈ 𝑸 → x < 𝑸 g ⋅ 𝑸 h → x ∈ A ⋅ 𝑷 B