Theorem prlem936b 5126

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

Hypotheses

Ref	Expression
prlem936b.1	|- (((y .Q B) e. A /\ ph) -> (y +Q z) e. A)
prlem936b.2	|- (((A e. P. /\ (y +Q z) e. A) /\ (x e. Q. /\ z e. Q.)) -> (ps -> ch))
prlem936b.3	|- ((x e. Q. /\ (z e. Q. /\ y e. Q.)) -> (ch <-> th))
prlem936b.4	|- ((((1Q <Q B /\ x e. Q.) /\ y e. Q.) /\ ph) -> (th <-> ta))
prlem936b.5	|- ((A e. P. /\ ta) -> (ps -> -. (x .Q B) e. A))

Assertion

Ref	Expression
prlem936b	|- (((A e. P. /\ z e. Q.) /\ ((ph /\ y e. Q.) /\ (1Q <Q B /\ (y .Q B) e. A))) -> ((x e. A /\ ps) -> (x e. A /\ -. (x .Q B) e. A)))

Proof of Theorem prlem936b

Step	Hyp	Ref	Expression
1		prlem936b.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((A e. P. /\ (y +Q z) e. A) /\ (x e. Q. /\ z e. Q.)) -> (ps -> ch))
2	1	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A e. P. /\ (y +Q z) e. A) -> ((x e. Q. /\ z e. Q.) -> (ps -> ch)))
3		prlem936b.1	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((y .Q B) e. A /\ ph) -> (y +Q z) e. A)
4	2, 3	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A e. P. /\ ((y .Q B) e. A /\ ph)) -> ((x e. Q. /\ z e. Q.) -> (ps -> ch)))
5	4	com12 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. Q. /\ z e. Q.) -> ((A e. P. /\ ((y .Q B) e. A /\ ph)) -> (ps -> ch)))
6	5	ad2ant2lr 410	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) -> ((A e. P. /\ ((y .Q B) e. A /\ ph)) -> (ps -> ch)))
7	6	exp4d 381	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) -> (A e. P. -> ((y .Q B) e. A -> (ph -> (ps -> ch)))))
8	7	com24 37	. . . . . . . . . . . . . . . . . . . . . 22 |- (((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) -> (ph -> ((y .Q B) e. A -> (A e. P. -> (ps -> ch)))))
9	8	imp41 368	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) /\ A e. P.) -> (ps -> ch))
10		prlem936b.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. Q. /\ (z e. Q. /\ y e. Q.)) -> (ch <-> th))
11	10	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) -> (ch <-> th))
12	11	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) -> (ch <-> th))
13		prlem936b.4	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((1Q <Q B /\ x e. Q.) /\ y e. Q.) /\ ph) -> (th <-> ta))
14	13	adantlrl 398	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) -> (th <-> ta))
15	12, 14	bitrd 526	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) -> (ch <-> ta))
16	15	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) /\ A e. P.) -> (ch <-> ta))
17	9, 16	sylibd 202	. . . . . . . . . . . . . . . . . . . 20 |- ((((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) /\ A e. P.) -> (ps -> ta))
18	17	ex 373	. . . . . . . . . . . . . . . . . . 19 |- (((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) -> (A e. P. -> (ps -> ta)))
19	18	imp32 363	. . . . . . . . . . . . . . . . . 18 |- ((((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) /\ (A e. P. /\ ps)) -> ta)
20		prlem936b.5	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. P. /\ ta) -> (ps -> -. (x .Q B) e. A))
21	20	expcom 374	. . . . . . . . . . . . . . . . . . . 20 |- (ta -> (A e. P. -> (ps -> -. (x .Q B) e. A)))
22	21	imp3a 361	. . . . . . . . . . . . . . . . . . 19 |- (ta -> ((A e. P. /\ ps) -> -. (x .Q B) e. A))
23	22	adantld 390	. . . . . . . . . . . . . . . . . 18 |- (ta -> ((((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) /\ (A e. P. /\ ps)) -> -. (x .Q B) e. A))
24	19, 23	mpcom 49	. . . . . . . . . . . . . . . . 17 |- ((((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) /\ (A e. P. /\ ps)) -> -. (x .Q B) e. A)
25	24	exp43 384	. . . . . . . . . . . . . . . 16 |- ((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) -> ((y .Q B) e. A -> (A e. P. -> (ps -> -. (x .Q B) e. A))))
26	25	com3r 35	. . . . . . . . . . . . . . 15 |- (A e. P. -> ((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A))))
27	26	exp4c 380	. . . . . . . . . . . . . 14 |- (A e. P. -> ((1Q <Q B /\ x e. Q.) -> ((z e. Q. /\ y e. Q.) -> (ph -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A))))))
28		elprpq 5067	. . . . . . . . . . . . . 14 |- ((A e. P. /\ x e. A) -> x e. Q.)
29	27, 28	sylan2i 465	. . . . . . . . . . . . 13 |- (A e. P. -> ((1Q <Q B /\ (A e. P. /\ x e. A)) -> ((z e. Q. /\ y e. Q.) -> (ph -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A))))))
30	29	exp4d 381	. . . . . . . . . . . 12 |- (A e. P. -> (1Q <Q B -> (A e. P. -> (x e. A -> ((z e. Q. /\ y e. Q.) -> (ph -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A))))))))
31	30	pm2.43a 66	. . . . . . . . . . 11 |- (A e. P. -> (1Q <Q B -> (x e. A -> ((z e. Q. /\ y e. Q.) -> (ph -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A)))))))
32	31	imp3a 361	. . . . . . . . . 10 |- (A e. P. -> ((1Q <Q B /\ x e. A) -> ((z e. Q. /\ y e. Q.) -> (ph -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A))))))
33	32	com24 37	. . . . . . . . 9 |- (A e. P. -> (ph -> ((z e. Q. /\ y e. Q.) -> ((1Q <Q B /\ x e. A) -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A))))))
34	33	exp4a 378	. . . . . . . 8 |- (A e. P. -> (ph -> (z e. Q. -> (y e. Q. -> ((1Q <Q B /\ x e. A) -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A)))))))
35	34	com23 32	. . . . . . 7 |- (A e. P. -> (z e. Q. -> (ph -> (y e. Q. -> ((1Q <Q B /\ x e. A) -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A)))))))
36	35	imp43 370	. . . . . 6 |- (((A e. P. /\ z e. Q.) /\ (ph /\ y e. Q.)) -> ((1Q <Q B /\ x e. A) -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A))))
37	36	exp3a 375	. . . . 5 |- (((A e. P. /\ z e. Q.) /\ (ph /\ y e. Q.)) -> (1Q <Q B -> (x e. A -> ((y .Q B) e. A -> (ps -> -. (x .Q B) e. A)))))
38	37	com34 36	. . . 4 |- (((A e. P. /\ z e. Q.) /\ (ph /\ y e. Q.)) -> (1Q <Q B -> ((y .Q B) e. A -> (x e. A -> (ps -> -. (x .Q B) e. A)))))
39	38	ex 373	. . 3 |- ((A e. P. /\ z e. Q.) -> ((ph /\ y e. Q.) -> (1Q <Q B -> ((y .Q B) e. A -> (x e. A -> (ps -> -. (x .Q B) e. A))))))
40	39	imp45 372	. 2 |- (((A e. P. /\ z e. Q.) /\ ((ph /\ y e. Q.) /\ (1Q <Q B /\ (y .Q B) e. A))) -> (x e. A -> (ps -> -. (x .Q B) e. A)))
41	40	imdistand 445	1 |- (((A e. P. /\ z e. Q.) /\ ((ph /\ y e. Q.) /\ (1Q <Q B /\ (y .Q B) e. A))) -> ((x e. A /\ ps) -> (x e. A /\ -. (x .Q B) e. A)))

Syntax hints:  -. wn 2   -> w