2lplnmN

Description: If the join of two lattice planes covers one of them, their meet is a lattice line. (Contributed by NM, 30-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2lplnm.j	$⊢ \underset{˙}{\lor} = join (K)$
	2lplnm.m	$⊢ \underset{˙}{\land} = meet (K)$
	2lplnm.c	$⊢ C = ⋖_{K}$
	2lplnm.n	$⊢ N = LLines (K)$
	2lplnm.p	$⊢ P = LPlanes (K)$
Assertion	2lplnmN	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X C (X \underset{˙}{\lor} Y)) \to X \underset{˙}{\land} Y \in N$

Proof

Step	Hyp	Ref	Expression
1		2lplnm.j	$⊢ \underset{˙}{\lor} = join (K)$
2		2lplnm.m	$⊢ \underset{˙}{\land} = meet (K)$
3		2lplnm.c	$⊢ C = ⋖_{K}$
4		2lplnm.n	$⊢ N = LLines (K)$
5		2lplnm.p	$⊢ P = LPlanes (K)$
6		simpl3	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X C (X \underset{˙}{\lor} Y)) \to Y \in P$
7		simpl1	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X C (X \underset{˙}{\lor} Y)) \to K \in HL$
8		hllat	$⊢ K \in HL \to K \in Lat$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 5	lplnbase	$⊢ X \in P \to X \in {Base}_{K}$
11	9 5	lplnbase	$⊢ Y \in P \to Y \in {Base}_{K}$
12	9 2	latmcl	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to X \underset{˙}{\land} Y \in {Base}_{K}$
13	8 10 11 12	syl3an	$⊢ (K \in HL \land X \in P \land Y \in P) \to X \underset{˙}{\land} Y \in {Base}_{K}$
14	13	adantr	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X C (X \underset{˙}{\lor} Y)) \to X \underset{˙}{\land} Y \in {Base}_{K}$
15	11	3ad2ant3	$⊢ (K \in HL \land X \in P \land Y \in P) \to Y \in {Base}_{K}$
16	15	adantr	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X C (X \underset{˙}{\lor} Y)) \to Y \in {Base}_{K}$
17		simp1	$⊢ (K \in HL \land X \in P \land Y \in P) \to K \in HL$
18	10	3ad2ant2	$⊢ (K \in HL \land X \in P \land Y \in P) \to X \in {Base}_{K}$
19	9 1 2 3	cvrexch	$⊢ (K \in HL \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to ((X \underset{˙}{\land} Y) C Y \leftrightarrow X C (X \underset{˙}{\lor} Y))$
20	17 18 15 19	syl3anc	$⊢ (K \in HL \land X \in P \land Y \in P) \to ((X \underset{˙}{\land} Y) C Y \leftrightarrow X C (X \underset{˙}{\lor} Y))$
21	20	biimpar	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X C (X \underset{˙}{\lor} Y)) \to (X \underset{˙}{\land} Y) C Y$
22	9 3 4 5	llncvrlpln	$⊢ ((K \in HL \land X \underset{˙}{\land} Y \in {Base}_{K} \land Y \in {Base}_{K}) \land (X \underset{˙}{\land} Y) C Y) \to (X \underset{˙}{\land} Y \in N \leftrightarrow Y \in P)$
23	7 14 16 21 22	syl31anc	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X C (X \underset{˙}{\lor} Y)) \to (X \underset{˙}{\land} Y \in N \leftrightarrow Y \in P)$
24	6 23	mpbird	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X C (X \underset{˙}{\lor} Y)) \to X \underset{˙}{\land} Y \in N$

Metamath Proof Explorer

Theorem 2lplnmN

Proof