Theorem mulclprlem 5133

Description: Lemma to prove downward closure in positive real multiplication. Part of proof of Proposition 9-3.7 of [Gleason] p. 124.

Assertion

Ref	Expression
mulclprlem	⊢ ((((A ∈ P ⋀ g ∈ A) ⋀ (B ∈ P ⋀ h ∈ B)) ⋀ x ∈ Q) → (x <Q (g ·Q h) → x ∈ (A ·P B)))

Distinct variable groups:   x,g,h   x,A   x,B

Proof of Theorem mulclprlem

Step	Hyp	Ref	Expression
1		recclpq 5084	. . . . . . . . 9 ⊢ (h ∈ Q → (*Q ‘h) ∈ Q)
2	1	adantl 390	. . . . . . . 8 ⊢ ((g ∈ Q ⋀ h ∈ Q) → (*Q ‘h) ∈ Q)
3		visset 1816	. . . . . . . . 9 ⊢ x ∈ V
4		oprex 3989	. . . . . . . . 9 ⊢ (g ·Q h) ∈ V
5		visset 1816	. . . . . . . . . 10 ⊢ y ∈ V
6		visset 1816	. . . . . . . . . 10 ⊢ z ∈ V
7	5, 6	ltmpq 5089	. . . . . . . . 9 ⊢ (w ∈ Q → (y <Q z ↔ (w ·Q y) <Q (w ·Q z)))
8		fvex 3738	. . . . . . . . 9 ⊢ (*Q ‘h) ∈ V
9	5, 6	mulcompq 5076	. . . . . . . . 9 ⊢ (y ·Q z) = (z ·Q y)
10	3, 4, 7, 8, 9	caoprord2 4063	. . . . . . . 8 ⊢ ((*Q ‘h) ∈ Q → (x <Q (g ·Q h) ↔ (x ·Q (*Q ‘h)) <Q ((g ·Q h) ·Q (*Q ‘h))))
11	2, 10	syl 10	. . . . . . 7 ⊢ ((g ∈ Q ⋀ h ∈ Q) → (x <Q (g ·Q h) ↔ (x ·Q (*Q ‘h)) <Q ((g ·Q h) ·Q (*Q ‘h))))
12		recidpq 5083	. . . . . . . . . . 11 ⊢ (h ∈ Q → (h ·Q (*Q ‘h)) = 1Q)
13	12	opreq2d 3982	. . . . . . . . . 10 ⊢ (h ∈ Q → (g ·Q (h ·Q (*Q ‘h))) = (g ·Q 1Q))
14		visset 1816	. . . . . . . . . . 11 ⊢ h ∈ V
15	14, 8	mulasspq 5077	. . . . . . . . . 10 ⊢ ((g ·Q h) ·Q (*Q ‘h)) = (g ·Q (h ·Q (*Q ‘h)))
16	13, 15	syl5eq 1522	. . . . . . . . 9 ⊢ (h ∈ Q → ((g ·Q h) ·Q (*Q ‘h)) = (g ·Q 1Q))
17		mulidpq 5081	. . . . . . . . 9 ⊢ (g ∈ Q → (g ·Q 1Q) = g)
18	16, 17	sylan9eqr 1532	. . . . . . . 8 ⊢ ((g ∈ Q ⋀ h ∈ Q) → ((g ·Q h) ·Q (*Q ‘h)) = g)
19	18	breq2d 2635	. . . . . . 7 ⊢ ((g ∈ Q ⋀ h ∈ Q) → ((x ·Q (*Q ‘h)) <Q ((g ·Q h) ·Q (*Q ‘h)) ↔ (x ·Q (*Q ‘h)) <Q g))
20	11, 19	bitrd 530	. . . . . 6 ⊢ ((g ∈ Q ⋀ h ∈ Q) → (x <Q (g ·Q h) ↔ (x ·Q (*Q ‘h)) <Q g))
21		elprpq 5107	. . . . . 6 ⊢ ((A ∈ P ⋀ g ∈ A) → g ∈ Q)
22		elprpq 5107	. . . . . 6 ⊢ ((B ∈ P ⋀ h ∈ B) → h ∈ Q)
23	20, 21, 22	syl2an 456	. . . . 5 ⊢ (((A ∈ P ⋀ g ∈ A) ⋀ (B ∈ P ⋀ h ∈ B)) → (x <Q (g ·Q h) ↔ (x ·Q (*Q ‘h)) <Q g))
24		prcdpq 5109	. . . . . 6 ⊢ ((A ∈ P ⋀ g ∈ A) → ((x ·Q (*Q ‘h)) <Q g → (x ·Q (*Q ‘h)) ∈ A))
25	24	adantr 391	. . . . 5 ⊢ (((A ∈ P ⋀ g ∈ A) ⋀ (B ∈ P ⋀ h ∈ B)) → ((x ·Q (*Q ‘h)) <Q g → (x ·Q (*Q ‘h)) ∈ A))
26	23, 25	sylbid 203	. . . 4 ⊢ (((A ∈ P ⋀ g ∈ A) ⋀ (B ∈ P ⋀ h ∈ B)) → (x <Q (g ·Q h) → (x ·Q (*Q ‘h)) ∈ A))
27		df-mp 5101	. . . . . . . . 9 ⊢ ·P = {⟨⟨w, v⟩, u⟩∣((w ∈ P ⋀ v ∈ P) ⋀ u = {x∣∃y ∈ w ∃z ∈ v x = (y ·Q z)})}
28	27	genpprecl 5116	. . . . . . . 8 ⊢ ((A ∈ P ⋀ B ∈ P) → (((x ·Q (*Q ‘h)) ∈ A ⋀ h ∈ B) → ((x ·Q (*Q ‘h)) ·Q h) ∈ (A ·P B)))
29	28	exp4b 381	. . . . . . 7 ⊢ (A ∈ P → (B ∈ P → ((x ·Q (*Q ‘h)) ∈ A → (h ∈ B → ((x ·Q (*Q ‘h)) ·Q h) ∈ (A ·P B)))))
30	29	com34 36	. . . . . 6 ⊢ (A ∈ P → (B ∈ P → (h ∈ B → ((x ·Q (*Q ‘h)) ∈ A → ((x ·Q (*Q ‘h)) ·Q h) ∈ (A ·P B)))))
31	30	imp32 363	. . . . 5 ⊢ ((A ∈ P ⋀ (B ∈ P ⋀ h ∈ B)) → ((x ·Q (*Q ‘h)) ∈ A → ((x ·Q (*Q ‘h)) ·Q h) ∈ (A ·P B)))
32	31	adantlr 395	. . . 4 ⊢ (((A ∈ P ⋀ g ∈ A) ⋀ (B ∈ P ⋀ h ∈ B)) → ((x ·Q (*Q ‘h)) ∈ A → ((x ·Q (*Q ‘h)) ·Q h) ∈ (A ·P B)))
33	26, 32	syld 27	. . 3 ⊢ (((A ∈ P ⋀ g ∈ A) ⋀ (B ∈ P ⋀ h ∈ B)) → (x <Q (g ·Q h) → ((x ·Q (*Q ‘h)) ·Q h) ∈ (A ·P B)))
34	33	adantr 391	. 2 ⊢ ((((A ∈ P ⋀ g ∈ A) ⋀ (B ∈ P ⋀ h ∈ B)) ⋀ x ∈ Q) → (x <Q (g ·Q h) → ((x ·Q (*Q ‘h)) ·Q h) ∈ (A ·P B)))
35	8, 14	mulcompq 5076	. . . . . . . 8 ⊢ ((*Q ‘h) ·Q h) = (h ·Q (*Q ‘h))
36	12, 35	syl5eq 1522	. . . . . . 7 ⊢ (h ∈ Q → ((*Q ‘h) ·Q h) = 1Q)
37	36	opreq2d 3982	. . . . . 6 ⊢ (h ∈ Q → (x ·Q ((*Q ‘h) ·Q h)) = (x ·Q 1Q))
38	8, 14	mulasspq 5077	. . . . . 6 ⊢ ((x ·Q (*Q ‘h)) ·Q h) = (x ·Q ((*Q ‘h) ·Q h))
39	37, 38	syl5eq 1522	. . . . 5 ⊢ (h ∈ Q → ((x ·Q (*Q ‘h)) ·Q h) = (x ·Q 1Q))
40		mulidpq 5081	. . . . 5 ⊢ (x ∈ Q → (x ·Q 1Q) = x)
41	39, 40	sylan9eq 1530	. . . 4 ⊢ ((h ∈ Q ⋀ x ∈ Q) → ((x ·Q (*Q ‘h)) ·Q h) = x)
42	41	eleq1d 1543	. . 3 ⊢ ((h ∈ Q ⋀ x ∈ Q) → (((x ·Q (*Q ‘h)) ·Q h) ∈ (A ·P B) ↔ x ∈ (A ·P B)))
43	22	adantl 390	. . 3 ⊢ (((A ∈ P ⋀ g ∈ A) ⋀ (B ∈ P ⋀ h ∈ B)) → h ∈ Q)
44	42, 43	sylan 450	. 2 ⊢ ((((A ∈ P ⋀ g ∈ A) ⋀ (B ∈ P ⋀ h ∈ B)) ⋀ x ∈ Q) → (((x ·Q (*Q ‘h)) ·Q h) ∈ (A ·P B) ↔ x ∈ (A ·P B)))
45	34, 44	sylibd 202	1 ⊢ ((((A ∈ P ⋀ g ∈ A) ⋀ (B ∈ P ⋀ h ∈ B)) ⋀ x ∈ Q) → (x <Q (g ·Q h) → x ∈ (A ·P B)))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ∈ wcel 960   class class class wbr 2624   ‘cfv 3188  (class class class)co 3969  Qcnq 4991  1_Qc1q 4992   ·_Q cmq 4994  *_Qcrq 4995   <_Q cltq 4996  Pcnp 4997   ·_P cmp 5000

This theorem is referenced by:  mulclpr 5134

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-int 2538  df-iun 2572  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-lim 2959  df-suc 2960  df-om 3138  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-fv 3204  df-rdg 3938  df-opr 3971  df-oprab 3972  df-1st 4085  df-2nd 4086  df-1o 4139  df-oadd 4141  df-omul 4142  df-er 4267  df-ec 4269  df-qs 4272  df-ni 5012  df-mi 5014  df-lti 5015  df-mpq 5048  df-enq 5049  df-nq 5050  df-mq 5052  df-rq 5053  df-ltq 5054  df-1q 5055  df-np 5098  df-mp 5101

Copyright terms: Public domain