2atmat

Description: The meet of two intersecting lines (expressed as joins of atoms) is an atom. (Contributed by NM, 21-Nov-2012)

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

Proof

Step	Hyp	Ref	Expression
1		2atmat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		2atmat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		2atmat.m	$⊢ \underset{˙}{\land} = meet (K)$
4		2atmat.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 P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to K \in HL$
6	5	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to K \in Lat$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
9	8	3ad2ant1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
10		simp21	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \in A$
11	7 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
12	10 11	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \in {Base}_{K}$
13		simp22	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to S \in A$
14	7 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
15	13 14	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to S \in {Base}_{K}$
16	7 2	latjass	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in {Base}_{K} \land S \in {Base}_{K})) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
17	6 9 12 15 16	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
18		simp33	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
19	7 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}$
20	6 9 12 19	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}$
21	7 1 2	latleeqj2	$⊢ (K \in Lat \land S \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
22	6 15 20 21	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
23	18 22	mpbid	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
24	17 23	eqtr3d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
25		simp23	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \neq Q$
26		simp32	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
27		simp12	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \in A$
28		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to Q \in A$
29		eqid	$⊢ LPlanes (K) = LPlanes (K)$
30	1 2 4 29	islpln2a	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in LPlanes (K) \leftrightarrow (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
31	5 27 28 10 30	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in LPlanes (K) \leftrightarrow (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
32	25 26 31	mpbir2and	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in LPlanes (K)$
33	24 32	eqeltrd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) \in LPlanes (K)$
34		eqid	$⊢ LLines (K) = LLines (K)$
35	2 4 34	llni2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to P \underset{˙}{\lor} Q \in LLines (K)$
36	5 27 28 25 35	syl31anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \underset{˙}{\lor} Q \in LLines (K)$
37		simp31	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \neq S$
38	2 4 34	llni2	$⊢ ((K \in HL \land R \in A \land S \in A) \land R \neq S) \to R \underset{˙}{\lor} S \in LLines (K)$
39	5 10 13 37 38	syl31anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \underset{˙}{\lor} S \in LLines (K)$
40	2 3 4 34 29	2llnmj	$⊢ (K \in HL \land P \underset{˙}{\lor} Q \in LLines (K) \land R \underset{˙}{\lor} S \in LLines (K)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) \in LPlanes (K))$
41	5 36 39 40	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) \in LPlanes (K))$
42	33 41	mpbird	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \neq Q) \land (R \neq S \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A$

Metamath Proof Explorer

Theorem 2atmat

Proof