ps-2c

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

	Ref	Expression
Hypotheses	2atm.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	2atm.j	$⊢ \underset{˙}{\lor} = join (K)$
	2atm.m	$⊢ \underset{˙}{\land} = meet (K)$
	2atm.a	$⊢ A = Atoms (K)$
Assertion	ps-2c	$⊢ ((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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} 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) \in A$

Proof

Step	Hyp	Ref	Expression
1		2atm.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		2atm.j	$⊢ \underset{˙}{\lor} = join (K)$
3		2atm.m	$⊢ \underset{˙}{\land} = meet (K)$
4		2atm.a	$⊢ A = Atoms (K)$
5		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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to K \in HL$
6		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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to P \in A$
7		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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to R \in A$
8	5	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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to K \in Lat$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
11	6 10	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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to P \in {Base}_{K}$
12		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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to Q \in A$
13	9 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
14	12 13	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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to Q \in {Base}_{K}$
15	9 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
16	7 15	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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to R \in {Base}_{K}$
17		simp31l	$⊢ ((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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} 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)$
18	9 1 2	latnlej1r	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K} \land R \in {Base}_{K}) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to P \neq R$
19	8 11 14 16 17 18	syl131anc	$⊢ ((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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to P \neq R$
20		eqid	$⊢ LLines (K) = LLines (K)$
21	2 4 20	llni2	$⊢ ((K \in HL \land P \in A \land R \in A) \land P \neq R) \to P \underset{˙}{\lor} R \in LLines (K)$
22	5 6 7 19 21	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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to P \underset{˙}{\lor} R \in LLines (K)$
23		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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to S \in A$
24		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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to T \in A$
25		simp31r	$⊢ ((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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to S \neq T$
26	2 4 20	llni2	$⊢ ((K \in HL \land S \in A \land T \in A) \land S \neq T) \to S \underset{˙}{\lor} T \in LLines (K)$
27	5 23 24 25 26	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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to S \underset{˙}{\lor} T \in LLines (K)$
28		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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))) \to P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T$
29		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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} 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))$
30		eqid	$⊢ 0. (K) = 0. (K)$
31	1 2 3 30 4	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 0. (K)$
32	5 6 12 7 23 24 17 25 29 31	syl333anc	$⊢ ((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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} 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 0. (K)$
33	3 30 4 20	2llnmat	$⊢ ((K \in HL \land P \underset{˙}{\lor} R \in LLines (K) \land S \underset{˙}{\lor} T \in LLines (K)) \land (P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \land (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T) \neq 0. (K))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (S \underset{˙}{\lor} T) \in A$
34	5 22 27 28 32 33	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 P \underset{˙}{\lor} R \neq S \underset{˙}{\lor} 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) \in A$

Metamath Proof Explorer

Theorem ps-2c

Proof