Theorem prlem936b 3948

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	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((A e. P. /\ (y +Q z) e. A) /\ (x e. Q. /\ z e. Q.)) -> (ps -> ch))
2	1	exp 291	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((A e. P. /\ (y +Q z) e. A) -> ((x e. Q. /\ z e. Q.) -> (ps -> ch)))
3		prlem936b.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((y .Q B) e. A /\ ph) -> (y +Q z) e. A)
4	2, 3	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A e. P. /\ ((y .Q B) e. A /\ ph)) -> ((x e. Q. /\ z e. Q.) -> (ps -> ch)))
5	4	com12 13	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x e. Q. /\ z e. Q.) -> ((A e. P. /\ ((y .Q B) e. A /\ ph)) -> (ps -> ch)))
6	5	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((1Q <Q B /\ x e. Q.) /\ z e. Q.) -> ((A e. P. /\ ((y .Q B) e. A /\ ph)) -> (ps -> ch)))
7	6	adantrr 312	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((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	exp4d 298	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) -> (A e. P. -> ((y .Q B) e. A -> (ph -> (ps -> ch)))))
9	8	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)))))
10	9	imp41 286	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) /\ A e. P.) -> (ps -> ch))
11		prlem936b.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. Q. /\ (z e. Q. /\ y e. Q.)) -> (ch <-> th))
12	11	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) -> (ch <-> th))
13	12	adantr 306	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) -> (ch <-> th))
14		prlem936b.4	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((1Q <Q B /\ x e. Q.) /\ y e. Q.) /\ ph) -> (th <-> ta ))
15	14	adantlrl 314	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) -> (th <-> ta ))
16	13, 15	bitrd 406	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) -> (ch <-> ta ))
17	16	ad2antll 320	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) /\ A e. P.) -> (ch <-> ta ))
18	10, 17	sylibd 177	. . . . . . . . . . . . . . . . . . . 20 |- ((((((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	exp 291	. . . . . . . . . . . . . . . . . . 19 |- (((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) -> (A e. P. -> (ps -> ta )))
20	19	imp32 281	. . . . . . . . . . . . . . . . . 18 |- ((((((1Q <Q B /\ x e. Q.) /\ (z e. Q. /\ y e. Q.)) /\ ph) /\ (y .Q B) e. A) /\ (A e. P. /\ ps)) -> ta )
21		prlem936b.5	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. P. /\ ta ) -> (ps -> -. (x .Q B) e. A))
22	21	exp 291	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. P. -> (ta -> (ps -> -. (x .Q B) e. A)))
23	22	com12 13	. . . . . . . . . . . . . . . . . . . 20 |- (ta -> (A e. P. -> (ps -> -. (x .Q B) e. A)))
24	23	imp3a 279	. . . . . . . . . . . . . . . . . . 19 |- (ta -> ((A e. P. /\ ps) -> -. (x .Q B) e. A))
25	24	adantld 307	. . . . . . . . . . . . . . . . . 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))
26	20, 25	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)
27	26	exp43 301	. . . . . . . . . . . . . . . 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))))
28	27	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))))
29	28	exp4c 297	. . . . . . . . . . . . . 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))))))
30		elprpq 3889	. . . . . . . . . . . . . 14 |- ((A e. P. /\ x e. A) -> x e. Q.)
31	29, 30	sylan2i 357	. . . . . . . . . . . . 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))))))
32	31	exp4d 298	. . . . . . . . . . . 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))))))))
33	32	pm2.43a 60	. . . . . . . . . . 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)))))))
34	33	imp3a 279	. . . . . . . . . 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))))))
35	34	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))))))
36	35	exp4a 295	. . . . . . . 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)))))))
37	36	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)))))))
38	37	imp43 288	. . . . . 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))))
39	38	exp3a 292	. . . . 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)))))
40	39	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)))))
41	40	exp 291	. . 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))))))
42	41	imp45 290	. 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)))
43	42	imdistand 342	1 |- (((A e. P. /\ z e. Q.) /\ ((ph /\ y e. Q.) /\ (1Q <Q B /\ (y