Theorem ltexprlem7 5148

Description: Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123.

Hypothesis

Ref	Expression
ltexprlem.1	|- C = {x | E.y(-. y e. A /\ (y +Q x) e. B)}

Assertion

Ref	Expression
ltexprlem7	|- (((A e. P. /\ B e. P.) /\ A (. B) -> B (_ (A +P. C))

Distinct variable groups:   x,y,A   x,B,y   x,C

Proof of Theorem ltexprlem7

Step	Hyp	Ref	Expression
1		ltaddpr 5140	. . . . . . . . . . . . . . 15 |- ((A e. P. /\ C e. P.) -> A <P (A +P. C))
2		addclpr 5120	. . . . . . . . . . . . . . . 16 |- ((A e. P. /\ C e. P.) -> (A +P. C) e. P.)
3		ltprord 5134	. . . . . . . . . . . . . . . 16 |- ((A e. P. /\ (A +P. C) e. P.) -> (A <P (A +P. C) <-> A (. (A +P. C)))
4	2, 3	syldan 467	. . . . . . . . . . . . . . 15 |- ((A e. P. /\ C e. P.) -> (A <P (A +P. C) <-> A (. (A +P. C)))
5	1, 4	mpbid 195	. . . . . . . . . . . . . 14 |- ((A e. P. /\ C e. P.) -> A (. (A +P. C))
6	5	pssssd 2144	. . . . . . . . . . . . 13 |- ((A e. P. /\ C e. P.) -> A (_ (A +P. C))
7	6	sseld 2067	. . . . . . . . . . . 12 |- ((A e. P. /\ C e. P.) -> (w e. A -> w e. (A +P. C)))
8	7	a1d 12	. . . . . . . . . . 11 |- ((A e. P. /\ C e. P.) -> (w e. B -> (w e. A -> w e. (A +P. C))))
9	8	a1d 12	. . . . . . . . . 10 |- ((A e. P. /\ C e. P.) -> (B e. P. -> (w e. B -> (w e. A -> w e. (A +P. C)))))
10	9	com4r 41	. . . . . . . . 9 |- (w e. A -> ((A e. P. /\ C e. P.) -> (B e. P. -> (w e. B -> w e. (A +P. C)))))
11	10	exp3a 375	. . . . . . . 8 |- (w e. A -> (A e. P. -> (C e. P. -> (B e. P. -> (w e. B -> w e. (A +P. C))))))
12		visset 1813	. . . . . . . . . . . . 13 |- w e. V
13	12	prnmadd 5100	. . . . . . . . . . . 12 |- ((B e. P. /\ w e. B) -> E.v(w +Q v) e. B)
14		elprpq 5095	. . . . . . . . . . . . . . . . 17 |- ((B e. P. /\ (w +Q v) e. B) -> (w +Q v) e. Q.)
15		visset 1813	. . . . . . . . . . . . . . . . . 18 |- v e. V
16		dmaddpq 5059	. . . . . . . . . . . . . . . . . 18 |- dom +Q = (Q. X. Q.)
17		0npq 5050	. . . . . . . . . . . . . . . . . 18 |- -. (/) e. Q.
18	15, 16, 17	ndmoprrcl 4046	. . . . . . . . . . . . . . . . 17 |- ((w +Q v) e. Q. -> (w e. Q. /\ v e. Q.))
19	14, 18	syl 10	. . . . . . . . . . . . . . . 16 |- ((B e. P. /\ (w +Q v) e. B) -> (w e. Q. /\ v e. Q.))
20		prlem934 5139	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. P. /\ v e. Q.) -> E.z(z e. A /\ -. (z +Q v) e. A))
21		prub 5098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((A e. P. /\ z e. A) /\ w e. Q.) -> (-. w e. A -> z <Q w))
22		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- z e. V
23	22	ltexpq 5080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((z e. Q. /\ w e. Q.) -> (z <Q w <-> E.x(z +Q x) = w))
24		elprpq 5095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((A e. P. /\ z e. A) -> z e. Q.)
25	23, 24	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((A e. P. /\ z e. A) /\ w e. Q.) -> (z <Q w <-> E.x(z +Q x) = w))
26	21, 25	sylibd 202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((A e. P. /\ z e. A) /\ w e. Q.) -> (-. w e. A -> E.x(z +Q x) = w))
27	26	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((A e. P. /\ z e. A) -> (w e. Q. -> (-. w e. A -> E.x(z +Q x) = w)))
28	27	ad2ant2r 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((A e. P. /\ C e. P.) /\ (z e. A /\ -. (z +Q v) e. A)) -> (w e. Q. -> (-. w e. A -> E.x(z +Q x) = w)))
29		df-plp 5088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- +P. = {<.<.z, v>., u>. | ((z e. P. /\ v e. P.) /\ u = {f | E.g e. z E.h e. v f = (g +Q h)})}
30	29	genpprecl 5104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((A e. P. /\ C e. P.) -> ((z e. A /\ x e. C) -> (z +Q x) e. (A +P. C)))
31		oprex 3983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (z +Q v) e. V
32		eleq1 1534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (y = (z +Q v) -> (y e. A <-> (z +Q v) e. A))
33	32	negbid 611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (y = (z +Q v) -> (-. y e. A <-> -. (z +Q v) e. A))
34		opreq1 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (y = (z +Q v) -> (y +Q x) = ((z +Q v) +Q x))
35	34	eleq1d 1540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (y = (z +Q v) -> ((y +Q x) e. B <-> ((z +Q v) +Q x) e. B))
36	33, 35	anbi12d 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (y = (z +Q v) -> ((-. y e. A /\ (y +Q x) e. B) <-> (-. (z +Q v) e. A /\ ((z +Q v) +Q x) e. B)))
37	31, 36	cla4ev 1869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((-. (z +Q v) e. A /\ ((z +Q v) +Q x) e. B) -> E.y(-. y e. A /\ (y +Q x) e. B))
38		ltexprlem.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- C = {x | E.y(-. y e. A /\ (y +Q x) e. B)}
39	38	abeq2i 1570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x e. C <-> E.y(-. y e. A /\ (y +Q x) e. B))
40	37, 39	sylibr 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((-. (z +Q v) e. A /\ ((z +Q v) +Q x) e. B) -> x e. C)
41		opreq1 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((z +Q x) = w -> ((z +Q x) +Q v) = (w +Q v))
42		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- x e. V
43		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- f e. V
44		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- g e. V
45	43, 44	addcompq 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (f +Q g) = (g +Q f)
46		visset 1813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- h e. V
47	44, 46	addasspq 5063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((f +Q g) +Q h) = (f +Q (g +Q h))
48	22, 15, 42, 45, 47	caopr32 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((z +Q v) +Q x) = ((z +Q x) +Q v)
49	41, 48	syl5eq 1519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((z +Q x) = w -> ((z +Q v) +Q x) = (w +Q v))
50	49	eleq1d 1540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((z +Q x) = w -> (((z +Q v) +Q x) e. B <-> (w +Q v) e. B))
51	50	biimpar 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((z +Q x) = w /\ (w +Q v) e. B) -> ((z +Q v) +Q x) e. B)
52	40, 51	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((-. (z +Q v) e. A /\ ((z +Q x) = w /\ (w +Q v) e. B)) -> x e. C)
53	30, 52	sylan2i 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((A e. P. /\ C e. P.) -> ((z e. A /\ (-. (z +Q v) e. A /\ ((z +Q x) = w /\ (w +Q v) e. B))) -> (z +Q x) e. (A +P. C)))
54	53	exp4d 381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((A e. P. /\ C e. P.) -> (z e. A -> (-. (z +Q v) e. A -> (((z +Q x) = w /\ (w +Q v) e. B) -> (z +Q x) e. (A +P. C)))))
55	54	imp42 369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((A e. P. /\ C e. P.) /\ (z e. A /\ -. (z +Q v) e. A)) /\ ((z +Q x) = w /\ (w +Q v) e. B)) -> (z +Q x) e. (A +P. C))
56		eleq1 1534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((z +Q x) = w -> ((z +Q x) e. (A +P. C) <-> w e. (A +P. C)))
57	56	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((A e. P. /\ C e. P.) /\ (z e. A /\ -. (z +Q v) e. A)) /\ ((z +Q x) = w /\ (w +Q v) e. B)) -> ((z +Q x) e. (A +P. C) <-> w e. (A +P. C)))
58	55, 57	mpbid 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((A e. P. /\ C e. P.) /\ (z e. A /\ -. (z +Q v) e. A)) /\ ((z +Q x) = w /\ (w +Q v) e. B)) -> w e. (A +P. C))
59	58	exp32 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((A e. P. /\ C e. P.) /\ (z e. A /\ -. (z +Q v) e. A)) -> ((z +Q x) = w -> ((w +Q v) e. B -> w e. (A +P. C))))
60	59	19.23adv 1214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((A e. P. /\ C e. P.) /\ (z e. A /\ -. (z +Q v) e. A)) -> (E.x(z +Q x) = w -> ((w +Q v) e. B -> w e. (A +P. C))))
61	28, 60	syl6d 56	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((A e. P. /\ C e. P.) /\ (z e. A /\ -. (z +Q v) e. A)) -> (w e. Q. -> (-. w e. A -> ((w +Q v) e. B -> w e. (A +P. C)))))
62	61	exp31 376	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A e. P. -> (C e. P. -> ((z e. A /\ -. (z +Q v) e. A) -> (w e. Q. -> (-. w e. A -> ((w +Q v) e. B -> w e. (A +P. C)))))))
63	62	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A e. P. -> ((z e. A /\ -. (z +Q v) e. A) -> (C e. P. -> (w e. Q. -> (