ps-2b

Description: Variation of projective geometry axiom ps-2 . (Contributed by NM, 3-Jul-2012)

	Ref	Expression
Hypotheses	ps-2b.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ps-2b.j	$⊢ \underset{˙}{\lor} = join (K)$
	ps-2b.m	$⊢ \underset{˙}{\land} = meet (K)$
	ps-2b.z	$⊢ \underset{˙}{0} = 0. (K)$
	ps-2b.a	$⊢ A = Atoms (K)$
Assertion	ps-2b	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T) \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		ps-2b.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ps-2b.j	$⊢ \underset{˙}{\lor} = join (K)$
3		ps-2b.m	$⊢ \underset{˙}{\land} = meet (K)$
4		ps-2b.z	$⊢ \underset{˙}{0} = 0. (K)$
5		ps-2b.a	$⊢ A = Atoms (K)$
6		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to K \in HL$
7		simp12	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to P \in A$
8		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to Q \in A$
9		simp21	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to R \in A$
10	7 8 9	3jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (P \in A \land Q \in A \land R \in A)$
11		simp22	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to S \in A$
12		simp23	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to T \in A$
13	11 12	jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (S \in A \land T \in A)$
14		simp31	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
15		simp32	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to S \neq T$
16	14 15	jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T)$
17		simp33	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
18	1 2 5	ps-2	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A)) \land ((\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
19	6 10 13 16 17 18	syl32anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
20		simp111	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in HL$
21		hlatl	$⊢ K \in HL \to K \in AtLat$
22	20 21	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in AtLat$
23	20	hllatd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in Lat$
24		simp112	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \in A$
25		simp121	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to R \in A$
26		eqid	$⊢ {Base}_{K} = {Base}_{K}$
27	26 2 5	hlatjcl	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R \in {Base}_{K}$
28	20 24 25 27	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \underset{˙}{\lor} R \in {Base}_{K}$
29		simp122	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \in A$
30		simp123	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to T \in A$
31	26 2 5	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
32	20 29 30 31	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \underset{˙}{\lor} T \in {Base}_{K}$
33	26 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} R \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K}) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T) \in {Base}_{K}$
34	23 28 32 33	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T) \in {Base}_{K}$
35		simp2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to u \in A$
36		simp3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
37	26 5	atbase	$⊢ u \in A \to u \in {Base}_{K}$
38	35 37	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to u \in {Base}_{K}$
39	26 1 3	latlem12	$⊢ (K \in Lat \land (u \in {Base}_{K} \land P \underset{˙}{\lor} R \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K})) \to ((u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \leftrightarrow u \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T)))$
40	23 38 28 32 39	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \leftrightarrow u \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T)))$
41	36 40	mpbid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to u \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T))$
42	26 1 4 5	atlen0	$⊢ ((K \in AtLat \land (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T) \in {Base}_{K} \land u \in A) \land u \underset{˙}{\leq} ((P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T) \neq \underset{˙}{0}$
43	22 34 35 41 42	syl31anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \land u \in A \land (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T) \neq \underset{˙}{0}$
44	43	rexlimdv3a	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (\exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land u \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T) \neq \underset{˙}{0})$
45	19 44	mpd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (\neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land S \neq T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T) \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem ps-2b

Proof