2llnmj

Description: The meet of two lattice lines is an atom iff their join is a lattice plane. (Contributed by NM, 27-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		2llnmj.j	$⊢ \underset{˙}{\lor} = join (K)$
2		2llnmj.m	$⊢ \underset{˙}{\land} = meet (K)$
3		2llnmj.a	$⊢ A = Atoms (K)$
4		2llnmj.n	$⊢ N = LLines (K)$
5		2llnmj.p	$⊢ P = LPlanes (K)$
6		simp1	$⊢ (K \in HL \land X \in N \land Y \in N) \to K \in HL$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 4	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
9	8	3ad2ant2	$⊢ (K \in HL \land X \in N \land Y \in N) \to X \in {Base}_{K}$
10	7 4	llnbase	$⊢ Y \in N \to Y \in {Base}_{K}$
11	10	3ad2ant3	$⊢ (K \in HL \land X \in N \land Y \in N) \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 N \land Y \in N) \to ((X \underset{˙}{\land} Y) ⋖_{K} Y \leftrightarrow X ⋖_{K} (X \underset{˙}{\lor} Y))$
15		simpl1	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X \underset{˙}{\land} Y \in A) \to K \in HL$
16		simpr	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X \underset{˙}{\land} Y \in A) \to X \underset{˙}{\land} Y \in A$
17		simpl3	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X \underset{˙}{\land} Y \in A) \to Y \in N$
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 N \land Y \in N) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
22	21	adantr	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X \underset{˙}{\land} Y \in A) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
23	19 12 3 4	atcvrlln2	$⊢ ((K \in HL \land X \underset{˙}{\land} Y \in A \land Y \in N) \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 N \land Y \in N) \land X \underset{˙}{\land} Y \in A) \to (X \underset{˙}{\land} Y) ⋖_{K} Y$
25		simpl3	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \underset{˙}{\land} Y) ⋖_{K} Y) \to Y \in N$
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 N \land Y \in N) \to X \underset{˙}{\land} Y \in {Base}_{K}$
28	6 27 11	3jca	$⊢ (K \in HL \land X \in N \land Y \in N) \to (K \in HL \land X \underset{˙}{\land} Y \in {Base}_{K} \land Y \in {Base}_{K})$
29	7 12 3 4	atcvrlln	$⊢ ((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 A \leftrightarrow Y \in N)$
30	28 29	sylan	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \underset{˙}{\land} Y) ⋖_{K} Y) \to (X \underset{˙}{\land} Y \in A \leftrightarrow Y \in N)$
31	25 30	mpbird	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (X \underset{˙}{\land} Y) ⋖_{K} Y) \to X \underset{˙}{\land} Y \in A$
32	24 31	impbida	$⊢ (K \in HL \land X \in N \land Y \in N) \to (X \underset{˙}{\land} Y \in A \leftrightarrow (X \underset{˙}{\land} Y) ⋖_{K} Y)$
33		simpl1	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X \underset{˙}{\lor} Y \in P) \to K \in HL$
34		simpl2	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X \underset{˙}{\lor} Y \in P) \to X \in N$
35		simpr	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X \underset{˙}{\lor} Y \in P) \to X \underset{˙}{\lor} Y \in P$
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 N \land Y \in N) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
38	37	adantr	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X \underset{˙}{\lor} Y \in P) \to X \leq_{K} (X \underset{˙}{\lor} Y)$
39	19 12 4 5	llncvrlpln2	$⊢ ((K \in HL \land X \in N \land X \underset{˙}{\lor} Y \in P) \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 N \land Y \in N) \land X \underset{˙}{\lor} Y \in P) \to X ⋖_{K} (X \underset{˙}{\lor} Y)$
41		simpl2	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X ⋖_{K} (X \underset{˙}{\lor} Y)) \to X \in N$
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 N \land Y \in N) \to X \underset{˙}{\lor} Y \in {Base}_{K}$
44	6 9 43	3jca	$⊢ (K \in HL \land X \in N \land Y \in N) \to (K \in HL \land X \in {Base}_{K} \land X \underset{˙}{\lor} Y \in {Base}_{K})$
45	7 12 4 5	llncvrlpln	$⊢ ((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 N \leftrightarrow X \underset{˙}{\lor} Y \in P)$
46	44 45	sylan	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X ⋖_{K} (X \underset{˙}{\lor} Y)) \to (X \in N \leftrightarrow X \underset{˙}{\lor} Y \in P)$
47	41 46	mpbid	$⊢ ((K \in HL \land X \in N \land Y \in N) \land X ⋖_{K} (X \underset{˙}{\lor} Y)) \to X \underset{˙}{\lor} Y \in P$
48	40 47	impbida	$⊢ (K \in HL \land X \in N \land Y \in N) \to (X \underset{˙}{\lor} Y \in P \leftrightarrow X ⋖_{K} (X \underset{˙}{\lor} Y))$
49	14 32 48	3bitr4d	$⊢ (K \in HL \land X \in N \land Y \in N) \to (X \underset{˙}{\land} Y \in A \leftrightarrow X \underset{˙}{\lor} Y \in P)$

Metamath Proof Explorer

Theorem 2llnmj

Proof