2lplnmj

Description: The meet of two lattice planes is a lattice line iff their join is a lattice volume. (Contributed by NM, 13-Jul-2012)

	Ref	Expression
Hypotheses	2lplnmj.j	$⊢ \underset{˙}{\lor} = join (K)$
	2lplnmj.m	$⊢ \underset{˙}{\land} = meet (K)$
	2lplnmj.n	$⊢ N = LLines (K)$
	2lplnmj.p	$⊢ P = LPlanes (K)$
	2lplnmj.v	$⊢ V = LVols (K)$
Assertion	2lplnmj	$⊢ (K \in HL \land X \in P \land Y \in P) \to (X \underset{˙}{\land} Y \in N \leftrightarrow X \underset{˙}{\lor} Y \in V)$

Proof

Step	Hyp	Ref	Expression
1		2lplnmj.j	$⊢ \underset{˙}{\lor} = join (K)$
2		2lplnmj.m	$⊢ \underset{˙}{\land} = meet (K)$
3		2lplnmj.n	$⊢ N = LLines (K)$
4		2lplnmj.p	$⊢ P = LPlanes (K)$
5		2lplnmj.v	$⊢ V = LVols (K)$
6		simp1	$⊢ (K \in HL \land X \in P \land Y \in P) \to K \in HL$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 4	lplnbase	$⊢ X \in P \to X \in {Base}_{K}$
9	8	3ad2ant2	$⊢ (K \in HL \land X \in P \land Y \in P) \to X \in {Base}_{K}$
10	7 4	lplnbase	$⊢ Y \in P \to Y \in {Base}_{K}$
11	10	3ad2ant3	$⊢ (K \in HL \land X \in P \land Y \in P) \to Y \in {Base}_{K}$
12		eqid	$⊢ ⋖_{K} = ⋖_{K}$
13	7 1 2 12	cvrexch	$⊢ (K \in HL \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to ((X \underset{˙}{\land} Y) ⋖_{K} Y \leftrightarrow X ⋖_{K} (X \underset{˙}{\lor} Y))$
14	6 9 11 13	syl3anc	$⊢ (K \in HL \land X \in P \land Y \in P) \to ((X \underset{˙}{\land} Y) ⋖_{K} Y \leftrightarrow X ⋖_{K} (X \underset{˙}{\lor} Y))$
15		simpl1	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X \underset{˙}{\land} Y \in N) \to K \in HL$
16		simpr	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X \underset{˙}{\land} Y \in N) \to X \underset{˙}{\land} Y \in N$
17		simpl3	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X \underset{˙}{\land} Y \in N) \to Y \in P$
18		hllat	$⊢ K \in HL \to K \in Lat$
19		eqid	$⊢ \leq_{K} = \leq_{K}$
20	7 19 2	latmle2	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
21	18 8 10 20	syl3an	$⊢ (K \in HL \land X \in P \land Y \in P) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
22	21	adantr	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X \underset{˙}{\land} Y \in N) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
23	19 12 3 4	llncvrlpln2	$⊢ ((K \in HL \land X \underset{˙}{\land} Y \in N \land Y \in P) \land (X \underset{˙}{\land} Y) \leq_{K} Y) \to (X \underset{˙}{\land} Y) ⋖_{K} Y$
24	15 16 17 22 23	syl31anc	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X \underset{˙}{\land} Y \in N) \to (X \underset{˙}{\land} Y) ⋖_{K} Y$
25		simpl3	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (X \underset{˙}{\land} Y) ⋖_{K} Y) \to Y \in P$
26	7 2	latmcl	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to X \underset{˙}{\land} Y \in {Base}_{K}$
27	18 8 10 26	syl3an	$⊢ (K \in HL \land X \in P \land Y \in P) \to X \underset{˙}{\land} Y \in {Base}_{K}$
28	6 27 11	3jca	$⊢ (K \in HL \land X \in P \land Y \in P) \to (K \in HL \land X \underset{˙}{\land} Y \in {Base}_{K} \land Y \in {Base}_{K})$
29	7 12 3 4	llncvrlpln	$⊢ ((K \in HL \land X \underset{˙}{\land} Y \in {Base}_{K} \land Y \in {Base}_{K}) \land (X \underset{˙}{\land} Y) ⋖_{K} Y) \to (X \underset{˙}{\land} Y \in N \leftrightarrow Y \in P)$
30	28 29	sylan	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (X \underset{˙}{\land} Y) ⋖_{K} Y) \to (X \underset{˙}{\land} Y \in N \leftrightarrow Y \in P)$
31	25 30	mpbird	$⊢ ((K \in HL \land X \in P \land Y \in P) \land (X \underset{˙}{\land} Y) ⋖_{K} Y) \to X \underset{˙}{\land} Y \in N$
32	24 31	impbida	$⊢ (K \in HL \land X \in P \land Y \in P) \to (X \underset{˙}{\land} Y \in N \leftrightarrow (X \underset{˙}{\land} Y) ⋖_{K} Y)$
33		simpl1	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X \underset{˙}{\lor} Y \in V) \to K \in HL$
34		simpl2	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X \underset{˙}{\lor} Y \in V) \to X \in P$
35		simpr	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X \underset{˙}{\lor} Y \in V) \to X \underset{˙}{\lor} Y \in V$
36	7 19 1	latlej1	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
37	18 8 10 36	syl3an	$⊢ (K \in HL \land X \in P \land Y \in P) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
38	37	adantr	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X \underset{˙}{\lor} Y \in V) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
39	19 12 4 5	lplncvrlvol2	$⊢ ((K \in HL \land X \in P \land X \underset{˙}{\lor} Y \in V) \land X \leq_{K} (X \underset{˙}{\lor} Y)) \to X ⋖_{K} (X \underset{˙}{\lor} Y)$
40	33 34 35 38 39	syl31anc	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X \underset{˙}{\lor} Y \in V) \to X ⋖_{K} (X \underset{˙}{\lor} Y)$
41		simpl2	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X ⋖_{K} (X \underset{˙}{\lor} Y)) \to X \in P$
42	7 1	latjcl	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to X \underset{˙}{\lor} Y \in {Base}_{K}$
43	18 8 10 42	syl3an	$⊢ (K \in HL \land X \in P \land Y \in P) \to X \underset{˙}{\lor} Y \in {Base}_{K}$
44	6 9 43	3jca	$⊢ (K \in HL \land X \in P \land Y \in P) \to (K \in HL \land X \in {Base}_{K} \land X \underset{˙}{\lor} Y \in {Base}_{K})$
45	7 12 4 5	lplncvrlvol	$⊢ ((K \in HL \land X \in {Base}_{K} \land X \underset{˙}{\lor} Y \in {Base}_{K}) \land X ⋖_{K} (X \underset{˙}{\lor} Y)) \to (X \in P \leftrightarrow X \underset{˙}{\lor} Y \in V)$
46	44 45	sylan	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X ⋖_{K} (X \underset{˙}{\lor} Y)) \to (X \in P \leftrightarrow X \underset{˙}{\lor} Y \in V)$
47	41 46	mpbid	$⊢ ((K \in HL \land X \in P \land Y \in P) \land X ⋖_{K} (X \underset{˙}{\lor} Y)) \to X \underset{˙}{\lor} Y \in V$
48	40 47	impbida	$⊢ (K \in HL \land X \in P \land Y \in P) \to (X \underset{˙}{\lor} Y \in V \leftrightarrow X ⋖_{K} (X \underset{˙}{\lor} Y))$
49	14 32 48	3bitr4d	$⊢ (K \in HL \land X \in P \land Y \in P) \to (X \underset{˙}{\land} Y \in N \leftrightarrow X \underset{˙}{\lor} Y \in V)$

Metamath Proof Explorer

Theorem 2lplnmj

Proof