Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem prlem936b 3948

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

**Hypotheses**
Ref	Expression
prlem936b.1	⊢ (((y ·_Q B) ∈ A ∧ φ) → (y +_Q z) ∈ A)
prlem936b.2	⊢ (((A ∈ P ∧ (y +_Q z) ∈ A) ∧ (x ∈ Q ∧ z ∈ Q)) → (ψ → χ))
prlem936b.3	⊢ ((x ∈ Q ∧ (z ∈ Q ∧ y ∈ Q)) → (χ ↔ θ))
prlem936b.4	⊢ ((((1_Q <_Q B ∧ x ∈ Q) ∧ y ∈ Q) ∧ φ) → (θ ↔ τ))
prlem936b.5	⊢ ((A ∈ P ∧ τ) → (ψ → ¬ (x ·_Q B) ∈ A))

**Assertion**
Ref	Expression
prlem936b	⊢ (((A ∈ P ∧ z ∈ Q) ∧ ((φ ∧ y ∈ Q) ∧ (1_Q <_Q B ∧ (y ·_Q B) ∈ A))) → ((x ∈ A ∧ ψ) → (x ∈ A ∧ ¬ (x ·_Q B) ∈ A)))

**Proof of Theorem prlem936b**
Step	Hyp	Ref	Expression
1		prlem936b.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((A ∈ P ∧ (y +_Q z) ∈ A) ∧ (x ∈ Q ∧ z ∈ Q)) → (ψ → χ))
2	1	exp 291	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((A ∈ P ∧ (y +_Q z) ∈ A) → ((x ∈ Q ∧ z ∈ Q) → (ψ → χ)))
3		prlem936b.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((y ·_Q B) ∈ A ∧ φ) → (y +_Q z) ∈ A)
4	2, 3	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((A ∈ P ∧ ((y ·_Q B) ∈ A ∧ φ)) → ((x ∈ Q ∧ z ∈ Q) → (ψ → χ)))
5	4	com12 13	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((x ∈ Q ∧ z ∈ Q) → ((A ∈ P ∧ ((y ·_Q B) ∈ A ∧ φ)) → (ψ → χ)))
6	5	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1_Q <_Q B ∧ x ∈ Q) ∧ z ∈ Q) → ((A ∈ P ∧ ((y ·_Q B) ∈ A ∧ φ)) → (ψ → χ)))
7	6	adantrr 312	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) → ((A ∈ P ∧ ((y ·_Q B) ∈ A ∧ φ)) → (ψ → χ)))
8	7	exp4d 298	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) → (A ∈ P → ((y ·_Q B) ∈ A → (φ → (ψ → χ)))))
9	8	com24 37	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) → (φ → ((y ·_Q B) ∈ A → (A ∈ P → (ψ → χ)))))
10	9	imp41 286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) ∧ (y ·_Q B) ∈ A) ∧ A ∈ P) → (ψ → χ))
11		prlem936b.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((x ∈ Q ∧ (z ∈ Q ∧ y ∈ Q)) → (χ ↔ θ))
12	11	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) → (χ ↔ θ))
13	12	adantr 306	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) → (χ ↔ θ))
14		prlem936b.4	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((1_Q <_Q B ∧ x ∈ Q) ∧ y ∈ Q) ∧ φ) → (θ ↔ τ))
15	14	adantlrl 314	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) → (θ ↔ τ))
16	13, 15	bitrd 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) → (χ ↔ τ))
17	16	ad2antll 320	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) ∧ (y ·_Q B) ∈ A) ∧ A ∈ P) → (χ ↔ τ))
18	10, 17	sylibd 177	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) ∧ (y ·_Q B) ∈ A) ∧ A ∈ P) → (ψ → τ))
19	18	exp 291	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) ∧ (y ·_Q B) ∈ A) → (A ∈ P → (ψ → τ)))
20	19	imp32 281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) ∧ (y ·_Q B) ∈ A) ∧ (A ∈ P ∧ ψ)) → τ)
21		prlem936b.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((A ∈ P ∧ τ) → (ψ → ¬ (x ·_Q B) ∈ A))
22	21	exp 291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (A ∈ P → (τ → (ψ → ¬ (x ·_Q B) ∈ A)))
23	22	com12 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (τ → (A ∈ P → (ψ → ¬ (x ·_Q B) ∈ A)))
24	23	imp3a 279	. . . . . . . . . . . . . . . . . . 19 ⊢ (τ → ((A ∈ P ∧ ψ) → ¬ (x ·_Q B) ∈ A))
25	24	adantld 307	. . . . . . . . . . . . . . . . . 18 ⊢ (τ → ((((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) ∧ (y ·_Q B) ∈ A) ∧ (A ∈ P ∧ ψ)) → ¬ (x ·_Q B) ∈ A))
26	20, 25	mpcom 49	. . . . . . . . . . . . . . . . 17 ⊢ ((((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) ∧ (y ·_Q B) ∈ A) ∧ (A ∈ P ∧ ψ)) → ¬ (x ·_Q B) ∈ A)
27	26	exp43 301	. . . . . . . . . . . . . . . 16 ⊢ ((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) → ((y ·_Q B) ∈ A → (A ∈ P → (ψ → ¬ (x ·_Q B) ∈ A))))
28	27	com3r 35	. . . . . . . . . . . . . . 15 ⊢ (A ∈ P → ((((1_Q <_Q B ∧ x ∈ Q) ∧ (z ∈ Q ∧ y ∈ Q)) ∧ φ) → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A))))
29	28	exp4c 297	. . . . . . . . . . . . . 14 ⊢ (A ∈ P → ((1_Q <_Q B ∧ x ∈ Q) → ((z ∈ Q ∧ y ∈ Q) → (φ → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A))))))
30		elprpq 3889	. . . . . . . . . . . . . 14 ⊢ ((A ∈ P ∧ x ∈ A) → x ∈ Q)
31	29, 30	sylan2i 357	. . . . . . . . . . . . 13 ⊢ (A ∈ P → ((1_Q <_Q B ∧ (A ∈ P ∧ x ∈ A)) → ((z ∈ Q ∧ y ∈ Q) → (φ → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A))))))
32	31	exp4d 298	. . . . . . . . . . . 12 ⊢ (A ∈ P → (1_Q <_Q B → (A ∈ P → (x ∈ A → ((z ∈ Q ∧ y ∈ Q) → (φ → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A))))))))
33	32	pm2.43a 60	. . . . . . . . . . 11 ⊢ (A ∈ P → (1_Q <_Q B → (x ∈ A → ((z ∈ Q ∧ y ∈ Q) → (φ → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A)))))))
34	33	imp3a 279	. . . . . . . . . 10 ⊢ (A ∈ P → ((1_Q <_Q B ∧ x ∈ A) → ((z ∈ Q ∧ y ∈ Q) → (φ → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A))))))
35	34	com24 37	. . . . . . . . 9 ⊢ (A ∈ P → (φ → ((z ∈ Q ∧ y ∈ Q) → ((1_Q <_Q B ∧ x ∈ A) → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A))))))
36	35	exp4a 295	. . . . . . . 8 ⊢ (A ∈ P → (φ → (z ∈ Q → (y ∈ Q → ((1_Q <_Q B ∧ x ∈ A) → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A)))))))
37	36	com23 32	. . . . . . 7 ⊢ (A ∈ P → (z ∈ Q → (φ → (y ∈ Q → ((1_Q <_Q B ∧ x ∈ A) → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A)))))))
38	37	imp43 288	. . . . . 6 ⊢ (((A ∈ P ∧ z ∈ Q) ∧ (φ ∧ y ∈ Q)) → ((1_Q <_Q B ∧ x ∈ A) → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A))))
39	38	exp3a 292	. . . . 5 ⊢ (((A ∈ P ∧ z ∈ Q) ∧ (φ ∧ y ∈ Q)) → (1_Q <_Q B → (x ∈ A → ((y ·_Q B) ∈ A → (ψ → ¬ (x ·_Q B) ∈ A)))))
40	39	com34 36	. . . 4 ⊢ (((A ∈ P ∧ z ∈ Q) ∧ (φ ∧ y ∈ Q)) → (1_Q <_Q B → ((y ·_Q B) ∈ A → (x ∈ A → (ψ → ¬ (x ·_Q B) ∈ A)))))
41	40	exp 291	. . 3 ⊢ ((A ∈ P ∧ z ∈ Q) → ((φ ∧ y ∈ Q) → (1_Q <_Q B → ((y ·_Q B) ∈ A → (x ∈ A → (ψ → ¬ (x ·_Q B) ∈ A))))))
42	41	imp45 290	. 2 ⊢ (((A ∈ P ∧ z ∈ Q) ∧ ((φ ∧ y ∈ Q) ∧ (1_Q <_Q B ∧ (y ·_Q B) ∈ A))) → (x ∈ A → (ψ → ¬ (x ·_Q B) ∈ A)))
43	42	imdistand 342	1 ⊢ (((A ∈ P ∧ z ∈ Q) ∧ ((φ ∧ y ∈ Q) ∧ (1_Q <_Q B ∧ (y ·_Q B) ∈ A))) → ((x ∈ A ∧ ψ) → (x ∈ A ∧ ¬ (x ·_Q B) ∈ A)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∈ wcel 1092 class class class wbr 2054 (class class class)co 3001 Qcnq 3773 1_Qc1q 3774 +_Q cplq 3775 ·_Q cmq 3776 <_Q cltq 3778 Pcnp 3779

This theorem is referenced by: prlem936 3949

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fv 2438 df-rdg 2970 df-qs 3205 df-ni 3794 df-nq 3832 df-np 3880

metamath.org