Theorem llncvrlpln 40394

Description: An element covering a lattice line is a lattice plane and vice-versa. (Contributed by NM, 26-Jun-2012.)

Hypotheses

Ref	Expression
llncvrlpln.b	⊢ 𝐵 = (Base‘𝐾)
llncvrlpln.c	⊢ 𝐶 = ( ⋖ ‘𝐾)
llncvrlpln.n	⊢ 𝑁 = (LLines‘𝐾)
llncvrlpln.p	⊢ 𝑃 = (LPlanes‘𝐾)

Assertion

Ref	Expression
llncvrlpln	⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → (𝑋 ∈ 𝑁 ↔ 𝑌 ∈ 𝑃))

Proof of Theorem llncvrlpln

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll1 1231	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋 ∈ 𝑁) → 𝐾 ∈ HL)
2		simpll3 1233	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋 ∈ 𝑁) → 𝑌 ∈ 𝐵)
3		simpr 490	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝑁)
4		simplr 781	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋 ∈ 𝑁) → 𝑋𝐶𝑌)
5		llncvrlpln.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
6		llncvrlpln.c	. . . 4 ⊢ 𝐶 = ( ⋖ ‘𝐾)
7		llncvrlpln.n	. . . 4 ⊢ 𝑁 = (LLines‘𝐾)
8		llncvrlpln.p	. . . 4 ⊢ 𝑃 = (LPlanes‘𝐾)
9	5, 6, 7, 8	lplni 40368	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑁) ∧ 𝑋𝐶𝑌) → 𝑌 ∈ 𝑃)
10	1, 2, 3, 4, 9	syl31anc 1400	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋 ∈ 𝑁) → 𝑌 ∈ 𝑃)
11		simpll1 1231	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝐾 ∈ HL)
12		simpll2 1232	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝑋 ∈ 𝐵)
13		eqid 2765	. . . . . . 7 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
14	13, 8	lplnneat 40381	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝑃) → ¬ 𝑌 ∈ (Atoms‘𝐾))
15	11, 14	sylancom 600	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → ¬ 𝑌 ∈ (Atoms‘𝐾))
16		simplr 781	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝑋𝐶𝑌)
17		breq1 5114	. . . . . . . 8 ⊢ (𝑋 = (0.‘𝐾) → (𝑋𝐶𝑌 ↔ (0.‘𝐾)𝐶𝑌))
18	16, 17	syl5ibcom 248	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (𝑋 = (0.‘𝐾) → (0.‘𝐾)𝐶𝑌))
19		simpll3 1233	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝑌 ∈ 𝐵)
20		eqid 2765	. . . . . . . . 9 ⊢ (0.‘𝐾) = (0.‘𝐾)
21	5, 20, 6, 13	isat2 40123	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵) → (𝑌 ∈ (Atoms‘𝐾) ↔ (0.‘𝐾)𝐶𝑌))
22	11, 19, 21	syl2anc 596	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (𝑌 ∈ (Atoms‘𝐾) ↔ (0.‘𝐾)𝐶𝑌))
23	18, 22	sylibrd 262	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (𝑋 = (0.‘𝐾) → 𝑌 ∈ (Atoms‘𝐾)))
24	23	necon3bd 2974	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (¬ 𝑌 ∈ (Atoms‘𝐾) → 𝑋 ≠ (0.‘𝐾)))
25	15, 24	mpd 16	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝑋 ≠ (0.‘𝐾))
26	7, 8	lplnnelln 40382	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝑃) → ¬ 𝑌 ∈ 𝑁)
27	11, 26	sylancom 600	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → ¬ 𝑌 ∈ 𝑁)
28	5, 6, 13, 7	atcvrlln 40356	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → (𝑋 ∈ (Atoms‘𝐾) ↔ 𝑌 ∈ 𝑁))
29	28	adantr 486	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (𝑋 ∈ (Atoms‘𝐾) ↔ 𝑌 ∈ 𝑁))
30	27, 29	mtbird 328	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → ¬ 𝑋 ∈ (Atoms‘𝐾))
31		eqid 2765	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
32	5, 31, 20, 13, 7	llnle 40354	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑋 ≠ (0.‘𝐾) ∧ ¬ 𝑋 ∈ (Atoms‘𝐾))) → ∃𝑧 ∈ 𝑁 𝑧(le‘𝐾)𝑋)
33	11, 12, 25, 30, 32	syl22anc 852	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → ∃𝑧 ∈ 𝑁 𝑧(le‘𝐾)𝑋)
34		simpr3 1215	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧(le‘𝐾)𝑋)
35		simpll1 1231	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝐾 ∈ HL)
36		hlop 40198	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
37	35, 36	syl 18	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝐾 ∈ OP)
38		simpr2 1214	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧 ∈ 𝑁)
39	5, 7	llnbase 40345	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑁 → 𝑧 ∈ 𝐵)
40	38, 39	syl 18	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧 ∈ 𝐵)
41		simpll2 1232	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑋 ∈ 𝐵)
42		simpll3 1233	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑌 ∈ 𝐵)
43		simpr1 1213	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑌 ∈ 𝑃)
44	5, 31, 6	cvrle 40114	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋(le‘𝐾)𝑌)
45	44	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑋(le‘𝐾)𝑌)
46		hlpos 40202	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
47	35, 46	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝐾 ∈ Poset)
48	5, 31	postr 18402	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ (𝑧 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑧(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)𝑌) → 𝑧(le‘𝐾)𝑌))
49	47, 40, 41, 42, 48	syl13anc 1399	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → ((𝑧(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)𝑌) → 𝑧(le‘𝐾)𝑌))
50	34, 45, 49	mp2and 712	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧(le‘𝐾)𝑌)
51	31, 6, 7, 8	llncvrlpln2 40393	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑧 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃) ∧ 𝑧(le‘𝐾)𝑌) → 𝑧𝐶𝑌)
52	35, 38, 43, 50, 51	syl31anc 1400	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧𝐶𝑌)
53		simplr 781	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑋𝐶𝑌)
54	5, 31, 6	cvrcmp2 40120	. . . . . . . . 9 ⊢ ((𝐾 ∈ OP ∧ (𝑧 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑧𝐶𝑌 ∧ 𝑋𝐶𝑌)) → (𝑧(le‘𝐾)𝑋 ↔ 𝑧 = 𝑋))
55	37, 40, 41, 42, 52, 53, 54	syl132anc 1415	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → (𝑧(le‘𝐾)𝑋 ↔ 𝑧 = 𝑋))
56	34, 55	mpbid 235	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧 = 𝑋)
57	56, 38	eqeltrrd 2866	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑋 ∈ 𝑁)
58	57	3exp2 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → (𝑌 ∈ 𝑃 → (𝑧 ∈ 𝑁 → (𝑧(le‘𝐾)𝑋 → 𝑋 ∈ 𝑁))))
59	58	imp 412	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (𝑧 ∈ 𝑁 → (𝑧(le‘𝐾)𝑋 → 𝑋 ∈ 𝑁)))
60	59	rexlimdv 3166	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (∃𝑧 ∈ 𝑁 𝑧(le‘𝐾)𝑋 → 𝑋 ∈ 𝑁))
61	33, 60	mpd 16	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝑋 ∈ 𝑁)
62	10, 61	impbida 813	1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → (𝑋 ∈ 𝑁 ↔ 𝑌 ∈ 𝑃))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∃wrex 3091   class class class wbr 5111  ‘cfv 6540  Basecbs 17295  lecple 17343  Posetcpo 18389  0.cp0 18503  OPcops 40008   ⋖ ccvr 40098  Atomscatm 40099  HLchlt 40186  LLinesclln 40327  LPlanesclpl 40328

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-proset 18376  df-poset 18395  df-plt 18410  df-lub 18426  df-glb 18427  df-join 18428  df-meet 18429  df-p0 18505  df-lat 18514  df-clat 18581  df-oposet 40012  df-ol 40014  df-oml 40015  df-covers 40102  df-ats 40103  df-atl 40134  df-cvlat 40158  df-hlat 40187  df-llines 40334  df-lplanes 40335

This theorem is used by:  2lplnmN  40395  2llnmj  40396  lplncvrlvol  40452  2lplnm2N  40457  2lplnmj  40458