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 eqtrid ⊢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∈vx=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 eqtrid ⊢h∈𝑸→*𝑸⁡h⋅𝑸h=1𝑸
37 36 oveq2d ⊢h∈𝑸→x⋅𝑸*𝑸⁡h⋅𝑸h=x⋅𝑸1𝑸
38 34 37 eqtrid ⊢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