Theorem prlem936 3949

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

Proof of Theorem prlem936

Step	Hyp	Ref	Expression
1		prn0 3887	. . . 4 |- (A e. P. -> -. A = (/))
2		n0 1714	. . . 4 |- (-. A = (/) <-> E.y y e. A)
3	1, 2	sylib 173	. . 3 |- (A e. P. -> E.y y e. A)
4		prlem934 3933	. . . . . . . . . . . . . . . . 17 |- ((A e. P. /\ z e. Q.) -> E.x(x e. A /\ -. (x +Q z) e. A))
5		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y +Q z) = (y .Q B) -> ((y +Q z) e. A <-> (y .Q B) e. A))
6	5	biimparc 327	. . . . . . . . . . . . . . . . . . . . 21 |- (((y .Q B) e. A /\ (y +Q z) = (y .Q B)) -> (y +Q z) e. A)
7		prub 3892	. . . . . . . . . . . . . . . . . . . . . 22 |- (((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 3852	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. Q. /\ z e. Q.) -> (x +Q z) e. Q.)
9	7, 8	sylan2 346	. . . . . . . . . . . . . . . . . . . . 21 |- (((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 3947	. . . . . . . . . . . . . . . . . . . . 21 |- ((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 3007	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y +Q z) = (y .Q B) -> ((x .Q (*Q` y)) .Q (y +Q z)) = ((x .Q (*Q` y)) .Q (y .Q B)))
12		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- y e. V
13		fvex 2838	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (*Q` y) e. V
14		prlem936.1	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- B e. V
15		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- z e. V
16		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- w e. V
17	15, 16	mulcompq 3858	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z .Q w) = (w .Q z)
18		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- v e. V
19	16, 18	mulasspq 3859	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((z .Q w) .Q v) = (z .Q (w .Q v))
20		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- x e. V
21	12, 13, 14, 17, 19, 20	caopr42 3080	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y .Q (*Q` y)) .Q (B .Q x)) = ((y .Q B) .Q (x .Q (*Q` y)))
22		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (B .Q x) e. V
23		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y .Q (*Q` y)) e. V
24	22, 23	mulcompq 3858	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B .Q x) .Q (y .Q (*Q` y))) = ((y .Q (*Q` y)) .Q (B .Q x))
25		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x .Q (*Q` y)) e. V
26		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y .Q B) e. V
27	25, 26	mulcompq 3858	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x .Q (*Q` y)) .Q (y .Q B)) = ((y .Q B) .Q (x .Q (*Q` y)))
28	21, 24, 27	3eqtr4 1126	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B .Q x) .Q (y .Q (*Q` y))) = ((x .Q (*Q` y)) .Q (y .Q B))
29	11, 28	syl6eqr 1142	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y +Q z) = (y .Q B) -> ((x .Q (*Q` y)) .Q (y +Q z)) = ((B .Q x) .Q (y .Q (*Q` y))))
30		recidpq 3865	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. Q. -> (y .Q (*Q` y)) = 1Q)
31	30	opreq2d 3013	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. Q. -> ((B .Q x) .Q (y .Q (*Q` y))) = ((B .Q x) .Q 1Q))
32		ltrelpq 3845	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- <Q (_ (Q. X. Q.)
33	14, 32	brel 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (1Q <Q B -> (1Q e. Q. /\ B e. Q.))
34	33	pm3.27d 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (1Q <Q B -> B e. Q.)
35	34	anim1i 269	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((1Q <Q B /\ x e. Q.) -> (B e. Q. /\ x e. Q.))
36		mulclpq 3854	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. Q. /\ x e. Q.) -> (B .Q x) e. Q.)
37		mulidpq 3863	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B .Q x) e. Q. -> ((B .Q x) .Q 1Q) = (B .Q x))
38	20, 14	mulcompq 3858	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x .Q B) = (B .Q x)
39	37, 38	syl6eqr 1142	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B .Q x) e. Q. -> ((B .Q x) .Q 1Q) = (x .Q B))
40	35, 36, 39	3syl 21	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((1Q <Q B /\ x e. Q.) -> ((B .Q x) .Q 1Q) = (x .Q B))
41	31, 40	sylan9eqr 1145	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((1Q <Q B /\ x e. Q.) /\ y e. Q.) -> ((B .Q x) .Q (y .Q (*Q` y))) = (x .Q B))
42	29, 41	sylan9eqr 1145	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((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 2072	. . . . . . . . . . . . . . . . . . . . 21 |- ((((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 3891	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. P. /\ (x .Q B) e. A) -> ((x +Q z) <Q (x .Q B) -> (x +Q z) e. A))
45	44	exp 291	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A e. P. -> ((x .Q B) e. A -> ((x +Q z) <Q (x .Q B) -> (x +Q z) e. A)))
46	45	com23 32	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. P. -> ((x +Q z) <Q (x .Q B) -> ((x .Q B) e. A -> (x +Q z) e. A)))
47	46	imp 277	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. P. /\ (x +Q z) <Q (x .Q B)) -> ((x .Q B) e. A -> (x +Q z) e. A))
48	47	con3d 87	. . . . . . . . . . . . . . . . . . . . 21 |- ((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 3948	. . . . . . . . . . . . . . . . . . . 20 |- (((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 947	. . . . . . . . . . . . . . . . . . 19 |- (((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	exp 291	. . . . . . . . . . . . . . . . . 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))))
52	51	com23 32	. . . . . . . . . . . . . . . . 17 |- ((A e. P. /\ z e. Q.) -> (E.x(x e. A /\ -. (x +Q z) e. A) -> ((((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	4, 52	mpd 46	. . . . . . . . . . . . . . . 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)))
54	53	exp4d 298	. . . . . . . . . . . . . . 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)))))
55	54	exp4b 296	. . . . . . . . . . . . . 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)))))))
56	55	imp3a 279	. . . . . . . . . . . . 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))))))
57	56	19.23adv 954	. . . . . . . . . . . 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))))))
58		1q 3851	. . . . . . . . . . . . . . . . 17 |- 1Q e. Q.
59	58	elisseti 1355	. . . . . . . . . . . . . . . 16 |- 1Q e. V
60	59, 14	ltmpq 3871	. . . . . . . . . . . . . . 15 |- (y e. Q. -> (1Q <Q B <-> (y .Q 1Q) <Q (y .Q B)))
61		mulidpq 3863	. . . . . . . . . . . . . . . 16 |- (y e. Q. -> (y .Q 1Q) = y)
62	61	breq1d 2071	. . . . . . . . . . . . . . 15 |- (y e. Q. -> ((y .Q 1Q) <Q (y .Q B) <-> y <Q (y .Q B)))
63	60, 62	bitrd 406	. . . . . . . . . . . . . 14 |- (y e. Q. -> (1Q <Q B <-> y <Q (y .Q B)))
64	26, 32	brel 2459	. . . . . . . . . . . . . . 15 |- (y <Q (y .Q B