Theorem prlem936 5127

Description: Lemma 9-3.6 of [Gleason] p. 124.

Hypothesis

Ref	Expression
prlem936.1	|- B e. V

Assertion

Ref	Expression
prlem936	|- ((A e. P. /\ 1Q <Q B) -> E.x(x e. A /\ -. (x .Q B) e. A))

Distinct variable groups:   x,A   x,B

Proof of Theorem prlem936

Step	Hyp	Ref	Expression
1		prn0 5065	. . . 4 |- (A e. P. -> A =/= (/))
2		ne0 2278	. . . 4 |- (A =/= (/) <-> E.y y e. A)
3	1, 2	sylib 198	. . 3 |- (A e. P. -> E.y y e. A)
4		prlem934 5111	. . . . . . . . . . . . . . . . 17 |- ((A e. P. /\ z e. Q.) -> E.x(x e. A /\ -. (x +Q z) e. A))
5		eleq1 1526	. . . . . . . . . . . . . . . . . . . . 21 |- ((y +Q z) = (y .Q B) -> ((y +Q z) e. A <-> (y .Q B) e. A))
6	5	biimparc 419	. . . . . . . . . . . . . . . . . . . 20 |- (((y .Q B) e. A /\ (y +Q z) = (y .Q B)) -> (y +Q z) e. A)
7		prub 5070	. . . . . . . . . . . . . . . . . . . . 21 |- (((A e. P. /\ (y +Q z) e. A) /\ (x +Q z) e. Q.) -> (-. (x +Q z) e. A -> (y +Q z) <Q (x +Q z)))
8		addclpq 5030	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. Q. /\ z e. Q.) -> (x +Q z) e. Q.)
9	7, 8	sylan2 451	. . . . . . . . . . . . . . . . . . . 20 |- (((A e. P. /\ (y +Q z) e. A) /\ (x e. Q. /\ z e. Q.)) -> (-. (x +Q z) e. A -> (y +Q z) <Q (x +Q z)))
10		prlem936a 5125	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. Q. /\ (z e. Q. /\ y e. Q.)) -> ((y +Q z) <Q (x +Q z) <-> (x +Q z) <Q ((x .Q (*Q` y)) .Q (y +Q z))))
11		opreq2 3954	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y +Q z) = (y .Q B) -> ((x .Q (*Q` y)) .Q (y +Q z)) = ((x .Q (*Q` y)) .Q (y .Q B)))
12		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- y e. V
13		fvex 3717	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (*Q` y) e. V
14		prlem936.1	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- B e. V
15		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- z e. V
16		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- w e. V
17	15, 16	mulcompq 5036	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z .Q w) = (w .Q z)
18		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- v e. V
19	16, 18	mulasspq 5037	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((z .Q w) .Q v) = (z .Q (w .Q v))
20		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- x e. V
21	12, 13, 14, 17, 19, 20	caopr42 4052	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y .Q (*Q` y)) .Q (B .Q x)) = ((y .Q B) .Q (x .Q (*Q` y)))
22		oprex 3968	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (B .Q x) e. V
23		oprex 3968	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y .Q (*Q` y)) e. V
24	22, 23	mulcompq 5036	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B .Q x) .Q (y .Q (*Q` y))) = ((y .Q (*Q` y)) .Q (B .Q x))
25		oprex 3968	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x .Q (*Q` y)) e. V
26		oprex 3968	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y .Q B) e. V
27	25, 26	mulcompq 5036	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x .Q (*Q` y)) .Q (y .Q B)) = ((y .Q B) .Q (x .Q (*Q` y)))
28	21, 24, 27	3eqtr4 1497	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((B .Q x) .Q (y .Q (*Q` y))) = ((x .Q (*Q` y)) .Q (y .Q B))
29	11, 28	syl6eqr 1517	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y +Q z) = (y .Q B) -> ((x .Q (*Q` y)) .Q (y +Q z)) = ((B .Q x) .Q (y .Q (*Q` y))))
30		recidpq 5043	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. Q. -> (y .Q (*Q` y)) = 1Q)
31	30	opreq2d 3961	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. Q. -> ((B .Q x) .Q (y .Q (*Q` y))) = ((B .Q x) .Q 1Q))
32		ltrelpq 5023	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- <Q (_ (Q. X. Q.)
33	14, 32	brel 3213	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (1Q <Q B -> (1Q e. Q. /\ B e. Q.))
34	33	pm3.27d 325	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (1Q <Q B -> B e. Q.)
35	34	anim1i 334	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((1Q <Q B /\ x e. Q.) -> (B e. Q. /\ x e. Q.))
36		mulclpq 5032	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. Q. /\ x e. Q.) -> (B .Q x) e. Q.)
37		mulidpq 5041	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B .Q x) e. Q. -> ((B .Q x) .Q 1Q) = (B .Q x))
38	20, 14	mulcompq 5036	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x .Q B) = (B .Q x)
39	37, 38	syl6eqr 1517	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B .Q x) e. Q. -> ((B .Q x) .Q 1Q) = (x .Q B))
40	35, 36, 39	3syl 20	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((1Q <Q B /\ x e. Q.) -> ((B .Q x) .Q 1Q) = (x .Q B))
41	31, 40	sylan9eqr 1521	. . . . . . . . . . . . . . . . . . . . . 22 |- (((1Q <Q B /\ x e. Q.) /\ y e. Q.) -> ((B .Q x) .Q (y .Q (*Q` y))) = (x .Q B))
42	29, 41	sylan9eqr 1521	. . . . . . . . . . . . . . . . . . . . 21 |- ((((1Q <Q B /\ x e. Q.) /\ y e. Q.) /\ (y +Q z) = (y .Q B)) -> ((x .Q (*Q` y)) .Q (y +Q z)) = (x .Q B))
43	42	breq2d 2620	. . . . . . . . . . . . . . . . . . . 20 |- ((((1Q <Q B /\ x e. Q.) /\ y e. Q.) /\ (y +Q z) = (y .Q B)) -> ((x +Q z) <Q ((x .Q (*Q` y)) .Q (y +Q z)) <-> (x +Q z) <Q (x .Q B)))
44		prcdpq 5069	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. P. /\ (x .Q B) e. A) -> ((x +Q z) <Q (x .Q B) -> (x +Q z) e. A))
45	44	ex 373	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. P. -> ((x .Q B) e. A -> ((x +Q z) <Q (x .Q B) -> (x +Q z) e. A)))
46	45	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 |- (A e. P. -> ((x +Q z) <Q (x .Q B) -> ((x .Q B) e. A -> (x +Q z) e. A)))
47	46	imp 350	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. P. /\ (x +Q z) <Q (x .Q B)) -> ((x .Q B) e. A -> (x +Q z) e. A))
48	47	con3d 95	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. P. /\ (x +Q z) <Q (x .Q B)) -> (-. (x +Q z) e. A -> -. (x .Q B) e. A))
49	6, 9, 10, 43, 48	prlem936b 5126	. . . . . . . . . . . . . . . . . . 19 |- (((A e. P. /\ z e. Q.) /\ (((y +Q z) = (y .Q B) /\ y e. Q.) /\ (1Q <Q B /\ (y .Q B) e. A))) -> ((x e. A /\ -. (x +Q z) e. A) -> (x e. A /\ -. (x .Q B) e. A)))
50	49	19.22dv 1285	. . . . . . . . . . . . . . . . . 18 |- (((A e. P. /\ z e. Q.) /\ (((y +Q z) = (y .Q B) /\ y e. Q.) /\ (1Q <Q B /\ (y .Q B) e. A))) -> (E.x(x e. A /\ -. (x +Q z) e. A) -> E.x(x e. A /\ -. (x .Q B) e. A)))
51	50	ex 373	. . . . . . . . . . . . . . . . 17 |- ((A e. P. /\ z e. Q.) -> ((((y +Q z) = (y .Q B) /\ y e. Q.) /\ (1Q <Q B /\ (y .Q B) e. A)) -> (E.x(x e. A /\ -. (x +Q z) e. A) -> E.x(x e. A /\ -. (x .Q B) e. A))))
52	4, 51	mpid 47	. . . . . . . . . . . . . . . 16 |- ((A e. P. /\ z e. Q.) -> ((((y +Q z) = (y .Q B) /\ y e. Q.) /\ (1Q <Q B /\ (y .Q B) e. A)) -> E.x(x e. A /\ -. (x .Q B) e. A)))
53	52	exp4d 381	. . . . . . . . . . . . . . 15 |- ((A e. P. /\ z e. Q.) -> (((y +Q z) = (y .Q B) /\ y e. Q.) -> (1Q <Q B -> ((y .Q B) e. A -> E.x(x e. A /\ -. (x .Q B) e. A)))))
54	53	exp4b 379	. . . . . . . . . . . . . 14 |- (A e. P. -> (z e. Q. -> ((y +Q z) = (y .Q B) -> (y e. Q. -> (1Q <Q B -> ((y .Q B) e. A -> E.x(x e. A /\ -. (x .Q B) e. A)))))))
55	54	imp3a 361	. . . . . . . . . . . . 13 |- (A e. P. -> ((z e. Q. /\ (y +Q z) = (y .Q B)) -> (y e. Q. -> (1Q <Q B -> ((y .Q B) e. A -> E.x(x e. A /\ -. (x .Q B) e. A))))))
56	55	19.23adv 1209	. . . . . . . . . . . 12 |- (A e. P. -> (E.z(z e. Q. /\ (y +Q z) = (y .Q B)) -> (y e. Q. -> (1Q <Q B -> ((y .Q B) e. A -> E.x(x e. A /\ -. (x .Q B) e. A))))))
57		1q 5029	. . . . . . . . . . . . . . . . 17 |- 1Q e. Q.
58	57	elisseti 1809	. . . . . . . . . . . . . . . 16 |- 1Q e. V
59	58, 14	ltmpq 5049	. . . . . . . . . . . . . . 15 |- (y e. Q. -> (1Q <Q B <-> (y .Q 1Q) <Q (y .Q B)))
60		mulidpq 5041	. . . . . . . . . . . . . . . 16 |- (y e. Q. -> (y .Q 1Q) = y)
61	60	breq1d 2619	. . . . . . . . . . . . . . 15 |- (y e. Q. -> ((y .Q 1Q) <Q (y .Q B) <-> y <Q (y .Q B)))
62	59, 61	bitrd 526	. . . . . . . . . . . . . 14 |- (y e. Q. -> (1Q <Q B <-> y <Q (y .Q B)))
63	26, 32	brel 3213	. . . . . . . . . . . . . . 15 |- (y <Q (y .Q B) -> (y e. Q. /\ (y .Q B) e. Q.))
64	12	ltexpq2 5053	. . . . . . . . . . . . . . . 16 |- ((y e. Q.