Theorem addclprlem2 5184

Description: Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of [Gleason] p. 123.

Assertion

Ref	Expression
addclprlem2	|- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x <Q (g +Q h) -> x e. (A +P. B)))

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

Proof of Theorem addclprlem2

Step	Hyp	Ref	Expression
1		addclprlem1 5183	. . . . 5 |- (((A e. P. /\ g e. A) /\ x e. Q.) -> (x <Q (g +Q h) -> ((x .Q (*Q` (g +Q h))) .Q g) e. A))
2	1	adantlr 402	. . . 4 |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x <Q (g +Q h) -> ((x .Q (*Q` (g +Q h))) .Q g) e. A))
3		addclprlem1 5183	. . . . . 6 |- (((B e. P. /\ h e. B) /\ x e. Q.) -> (x <Q (h +Q g) -> ((x .Q (*Q` (h +Q g))) .Q h) e. B))
4		visset 1860	. . . . . . . 8 |- g e. V
5		visset 1860	. . . . . . . 8 |- h e. V
6	4, 5	addcompq 5127	. . . . . . 7 |- (g +Q h) = (h +Q g)
7	6	breq2i 2682	. . . . . 6 |- (x <Q (g +Q h) <-> x <Q (h +Q g))
8	6	fveq2i 3784	. . . . . . . . 9 |- (*Q` (g +Q h)) = (*Q` (h +Q g))
9	8	opreq2i 4030	. . . . . . . 8 |- (x .Q (*Q` (g +Q h))) = (x .Q (*Q` (h +Q g)))
10	9	opreq1i 4029	. . . . . . 7 |- ((x .Q (*Q` (g +Q h))) .Q h) = ((x .Q (*Q` (h +Q g))) .Q h)
11	10	eleq1i 1584	. . . . . 6 |- (((x .Q (*Q` (g +Q h))) .Q h) e. B <-> ((x .Q (*Q` (h +Q g))) .Q h) e. B)
12	3, 7, 11	3imtr4g 564	. . . . 5 |- (((B e. P. /\ h e. B) /\ x e. Q.) -> (x <Q (g +Q h) -> ((x .Q (*Q` (g +Q h))) .Q h) e. B))
13	12	adantll 401	. . . 4 |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x <Q (g +Q h) -> ((x .Q (*Q` (g +Q h))) .Q h) e. B))
14	2, 13	jcad 611	. . 3 |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x <Q (g +Q h) -> (((x .Q (*Q` (g +Q h))) .Q g) e. A /\ ((x .Q (*Q` (g +Q h))) .Q h) e. B)))
15		pm3.26 326	. . . 4 |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> ((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)))
16		pm3.26 326	. . . . 5 |- ((A e. P. /\ g e. A) -> A e. P.)
17		pm3.26 326	. . . . 5 |- ((B e. P. /\ h e. B) -> B e. P.)
18	16, 17	anim12i 340	. . . 4 |- (((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) -> (A e. P. /\ B e. P.))
19		df-plp 5153	. . . . 5 |- +P. = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.y e. w E.z e. v x = (y +Q z)})}
20	19	genpprecl 5169	. . . 4 |- ((A e. P. /\ B e. P.) -> ((((x .Q (*Q` (g +Q h))) .Q g) e. A /\ ((x .Q (*Q` (g +Q h))) .Q h) e. B) -> (((x .Q (*Q` (g +Q h))) .Q g) +Q ((x .Q (*Q` (g +Q h))) .Q h)) e. (A +P. B)))
21	15, 18, 20	3syl 20	. . 3 |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> ((((x .Q (*Q` (g +Q h))) .Q g) e. A /\ ((x .Q (*Q` (g +Q h))) .Q h) e. B) -> (((x .Q (*Q` (g +Q h))) .Q g) +Q ((x .Q (*Q` (g +Q h))) .Q h)) e. (A +P. B)))
22	14, 21	syld 27	. 2 |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x <Q (g +Q h) -> (((x .Q (*Q` (g +Q h))) .Q g) +Q ((x .Q (*Q` (g +Q h))) .Q h)) e. (A +P. B)))
23		elprpq 5160	. . . . . . . . 9 |- ((A e. P. /\ g e. A) -> g e. Q.)
24		elprpq 5160	. . . . . . . . 9 |- ((B e. P. /\ h e. B) -> h e. Q.)
25	23, 24	anim12i 340	. . . . . . . 8 |- (((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) -> (g e. Q. /\ h e. Q.))
26		addclpq 5123	. . . . . . . 8 |- ((g e. Q. /\ h e. Q.) -> (g +Q h) e. Q.)
27		recidpq 5136	. . . . . . . 8 |- ((g +Q h) e. Q. -> ((g +Q h) .Q (*Q` (g +Q h))) = 1Q)
28	25, 26, 27	3syl 20	. . . . . . 7 |- (((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) -> ((g +Q h) .Q (*Q` (g +Q h))) = 1Q)
29		fvex 3789	. . . . . . . 8 |- (*Q` (g +Q h)) e. V
30		oprex 4041	. . . . . . . 8 |- (g +Q h) e. V
31	29, 30	mulcompq 5129	. . . . . . 7 |- ((*Q` (g +Q h)) .Q (g +Q h)) = ((g +Q h) .Q (*Q` (g +Q h)))
32	28, 31	syl5eq 1566	. . . . . 6 |- (((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) -> ((*Q` (g +Q h)) .Q (g +Q h)) = 1Q)
33	32	opreq2d 4034	. . . . 5 |- (((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) -> (x .Q ((*Q` (g +Q h)) .Q (g +Q h))) = (x .Q 1Q))
34		mulidpq 5134	. . . . 5 |- (x e. Q. -> (x .Q 1Q) = x)
35	33, 34	sylan9eq 1574	. . . 4 |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x .Q ((*Q` (g +Q h)) .Q (g +Q h))) = x)
36	4, 5	distrpq 5132	. . . . 5 |- ((x .Q (*Q` (g +Q h))) .Q (g +Q h)) = (((x .Q (*Q` (g +Q h))) .Q g) +Q ((x .Q (*Q` (g +Q h))) .Q h))
37	29, 30	mulasspq 5130	. . . . 5 |- ((x .Q (*Q` (g +Q h))) .Q (g +Q h)) = (x .Q ((*Q` (g +Q h)) .Q (g +Q h)))
38	36, 37	eqtr3i 1544	. . . 4 |- (((x .Q (*Q` (g +Q h))) .Q g) +Q ((x .Q (*Q` (g +Q h))) .Q h)) = (x .Q ((*Q` (g +Q h)) .Q (g +Q h)))
39	35, 38	syl5eq 1566	. . 3 |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (((x .Q (*Q` (g +Q h))) .Q g) +Q ((x .Q (*Q` (g +Q h))) .Q h)) = x)
40	39	eleq1d 1587	. 2 |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> ((((x .Q (*Q` (g +Q h))) .Q g) +Q ((x .Q (*Q` (g +Q h))) .Q h)) e. (A +P. B) <-> x e. (A +P. B)))
41	22, 40	sylibd 209	1 |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x <Q (g +Q h) -> x e. (A +P. B)))

Syntax hints:   -> wi 3   /\ wa 230   = wceq 997   e. wcel 999   class class class wbr 2674  ` cfv 3239  (class class class)co 4021  Q.cnq 5044  1Qc1q 5045   +Q cplq 5046   .Q cmq 5047  *Qcrq 5048   <Q cltq 5049  P.cnp 5050   +P. cpp 5052

This theorem is referenced by:  addclpr 5185

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-fv 3255  df-rdg 3990  df-opr 4023  df-oprab 4024  df-1st 4137  df-2nd 4138  df-1o 4191  df-oadd 4193  df-omul 4194  df-er 4319  df-ec 4321  df-qs 4324  df-ni 5065  df-pli 5066  df-mi 5067  df-lti 5068  df-plpq 5100  df-mpq 5101  df-enq 5102  df-nq 5103  df-plq 5104  df-mq 5105  df-rq 5106  df-ltq 5107  df-1q 5108  df-np 5151  df-plp 5153

Copyright terms: Public domain