Theorem ltexprlem7 3942

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 group(s):   x,y,A   x,B,y   x,C

Proof of Theorem ltexprlem7

Step	Hyp	Ref	Expression
1		ltaddpr 3934	. . . . . . . . . . . . . . 15 |- ((A e. P. /\ C e. P.) -> A <P (A +P. C))
2		ltprord 3928	. . . . . . . . . . . . . . . . 17 |- ((A e. P. /\ (A +P. C) e. P.) -> (A <P (A +P. C) <-> A (. (A +P. C)))
3		addclpr 3914	. . . . . . . . . . . . . . . . 17 |- ((A e. P. /\ C e. P.) -> (A +P. C) e. P.)
4	2, 3	sylan2 346	. . . . . . . . . . . . . . . 16 |- ((A e. P. /\ (A e. P. /\ C e. P.)) -> (A <P (A +P. C) <-> A (. (A +P. C)))
5	4	anabss5 384	. . . . . . . . . . . . . . 15 |- ((A e. P. /\ C e. P.) -> (A <P (A +P. C) <-> A (. (A +P. C)))
6	1, 5	mpbid 170	. . . . . . . . . . . . . 14 |- ((A e. P. /\ C e. P.) -> A (. (A +P. C))
7	6	pssssd 1568	. . . . . . . . . . . . 13 |- ((A e. P. /\ C e. P.) -> A (_ (A +P. C))
8	7	sseld 1506	. . . . . . . . . . . 12 |- ((A e. P. /\ C e. P.) -> (w e. A -> w e. (A +P. C)))
9	8	a1d 14	. . . . . . . . . . 11 |- ((A e. P. /\ C e. P.) -> (w e. B -> (w e. A -> w e. (A +P. C))))
10	9	a1d 14	. . . . . . . . . 10 |- ((A e. P. /\ C e. P.) -> (B e. P. -> (w e. B -> (w e. A -> w e. (A +P. C)))))
11	10	com4r 41	. . . . . . . . 9 |- (w e. A -> ((A e. P. /\ C e. P.) -> (B e. P. -> (w e. B -> w e. (A +P. C)))))
12	11	exp3a 292	. . . . . . . 8 |- (w e. A -> (A e. P. -> (C e. P. -> (B e. P. -> (w e. B -> w e. (A +P. C))))))
13		visset 1350	. . . . . . . . . . . . 13 |- w e. V
14	13	prnmadd 3894	. . . . . . . . . . . 12 |- ((B e. P. /\ w e. B) -> E.v(w +Q v) e. B)
15		elprpq 3889	. . . . . . . . . . . . . . . . 17 |- ((B e. P. /\ (w +Q v) e. B) -> (w +Q v) e. Q.)
16		visset 1350	. . . . . . . . . . . . . . . . . 18 |- v e. V
17		dmaddpq 3853	. . . . . . . . . . . . . . . . . 18 |- dom +Q = (Q. X. Q.)
18		0npq 3844	. . . . . . . . . . . . . . . . . 18 |- -. (/) e. Q.
19	16, 17, 18	ndmoprrcl 3060	. . . . . . . . . . . . . . . . 17 |- ((w +Q v) e. Q. -> (w e. Q. /\ v e. Q.))
20	15, 19	syl 12	. . . . . . . . . . . . . . . 16 |- ((B e. P. /\ (w +Q v) e. B) -> (w e. Q. /\ v e. Q.))
21		prlem934 3933	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. P. /\ v e. Q.) -> E.z(z e. A /\ -. (z +Q v) e. A))
22		prub 3892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((A e. P. /\ z e. A) /\ w e. Q.) -> (-. w e. A -> z <Q w))
23		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- z e. V
24	23	ltexpq 3874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((z e. Q. /\ w e. Q.) -> (z <Q w <-> E.x(z +Q x) = w))
25		elprpq 3889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((A e. P. /\ z e. A) -> z e. Q.)
26	24, 25	sylan 343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((A e. P. /\ z e. A) /\ w e. Q.) -> (z <Q w <-> E.x(z +Q x) = w))
27	22, 26	sylibd 177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((A e. P. /\ z e. A) /\ w e. Q.) -> (-. w e. A -> E.x(z +Q x) = w))
28	27	exp 291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((A e. P. /\ z e. A) -> (w e. Q. -> (-. w e. A -> E.x(z +Q x) = w)))
29	28	adantlr 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((A e. P. /\ C e. P.) /\ z e. A) -> (w e. Q. -> (-. w e. A -> E.x(z +Q x) = w)))
30	29	adantrr 312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))
31		df-plp 3882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)})}
32	31	genpprecl 3898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((A e. P. /\ C e. P.) -> ((z e. A /\ x e. C) -> (z +Q x) e. (A +P. C)))
33		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (z +Q v) e. V
34		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (y = (z +Q v) -> (y e. A <-> (z +Q v) e. A))
35	34	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (y = (z +Q v) -> (-. y e. A <-> -. (z +Q v) e. A))
36		opreq1 3006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (y = (z +Q v) -> (y +Q x) = ((z +Q v) +Q x))
37	36	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (y = (z +Q v) -> ((y +Q x) e. B <-> ((z +Q v) +Q x) e. B))
38	35, 37	anbi12d 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))
39	33, 38	cla4ev 1401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((-. (z +Q v) e. A /\ ((z +Q v) +Q x) e. B) -> E.y(-. y e. A /\ (y +Q x) e. B))
40		ltexprlem.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- C = {x | E.y(-. y e. A /\ (y +Q x) e. B)}
41	40	cleqabi 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x e. C <-> E.y(-. y e. A /\ (y +Q x) e. B))
42	39, 41	sylibr 175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((-. (z +Q v) e. A /\ ((z +Q v) +Q x) e. B) -> x e. C)
43		opreq1 3006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((z +Q x) = w -> ((z +Q x) +Q v) = (w +Q v))
44		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- x e. V
45		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- f e. V
46		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- g e. V
47	45, 46	addcompq 3856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (f +Q g) = (g +Q f)
48		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- h e. V
49	46, 48	addasspq 3857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((f +Q g) +Q h) = (f +Q (g +Q h))
50	23, 16, 44, 47, 49	caopr32 3074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((z +Q v) +Q x) = ((z +Q x) +Q v)
51	43, 50	syl5eq 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((z +Q x) = w -> ((z +Q v) +Q x) = (w +Q v))
52	51	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((z +Q x) = w -> (((z +Q v) +Q x) e. B <-> (w +Q v) e. B))
53	52	biimpar 325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((z +Q x) = w /\ (w +Q v) e. B) -> ((z +Q v) +Q x) e. B)
54	42, 53	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((-. (z +Q v) e. A /\ ((z +Q x) = w /\ (w +Q v) e. B)) -> x e. C)
55	32, 54	sylan2i 357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))
56	55	exp4d 298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))))
57	56	imp42 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))
58		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((z +Q x) = w -> ((z +Q x) e. (A +P. C) <-> w e. (A +P. C)))
59	58	ad2antrl 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))
60	57, 59	mpbid 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))
61	60	exp32 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
62	61	19.23adv 954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
63	30, 62	syl6d 54	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))))
64	63	exp31 293	. . . . . . . . . . . . . . . . . . . . . . . . . . 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)))))))
65	64	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A e. P. -> ((z e. A /\ -. (z +Q v