llnmlplnN

Description: The intersection of a line with a plane not containing it is an atom. (Contributed by NM, 29-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	llnmlpln.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	llnmlpln.m	$⊢ \underset{˙}{\land} = meet (K)$
	llnmlpln.z	$⊢ \underset{˙}{0} = 0. (K)$
	llnmlpln.a	$⊢ A = Atoms (K)$
	llnmlpln.n	$⊢ N = LLines (K)$
	llnmlpln.p	$⊢ P = LPlanes (K)$
Assertion	llnmlplnN	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \underset{˙}{\land} Y \in A$

Proof

Step	Hyp	Ref	Expression
1		llnmlpln.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		llnmlpln.m	$⊢ \underset{˙}{\land} = meet (K)$
3		llnmlpln.z	$⊢ \underset{˙}{0} = 0. (K)$
4		llnmlpln.a	$⊢ A = Atoms (K)$
5		llnmlpln.n	$⊢ N = LLines (K)$
6		llnmlpln.p	$⊢ P = LPlanes (K)$
7		simprl	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to \neg X \underset{˙}{\leq} Y$
8		simp11	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to K \in HL$
9	8	hllatd	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to K \in Lat$
10		simp12	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to X \in N$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 5	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
13	10 12	syl	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to X \in {Base}_{K}$
14		simp13	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to Y \in P$
15	11 6	lplnbase	$⊢ Y \in P \to Y \in {Base}_{K}$
16	14 15	syl	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to Y \in {Base}_{K}$
17	11 2	latmcl	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to X \underset{˙}{\land} Y \in {Base}_{K}$
18	9 13 16 17	syl3anc	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to X \underset{˙}{\land} Y \in {Base}_{K}$
19		simp2r	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to X \underset{˙}{\land} Y \neq \underset{˙}{0}$
20		simp3	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to \neg X \underset{˙}{\land} Y \in A$
21	11 1 3 4 5	llnle	$⊢ ((K \in HL \land X \underset{˙}{\land} Y \in {Base}_{K}) \land (X \underset{˙}{\land} Y \neq \underset{˙}{0} \land \neg X \underset{˙}{\land} Y \in A)) \to \exists u \in N u \underset{˙}{\leq} (X \underset{˙}{\land} Y)$
22	8 18 19 20 21	syl22anc	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to \exists u \in N u \underset{˙}{\leq} (X \underset{˙}{\land} Y)$
23	9	adantr	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to K \in Lat$
24	18	adantr	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to X \underset{˙}{\land} Y \in {Base}_{K}$
25	13	adantr	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to X \in {Base}_{K}$
26	11 1 2	latmle1	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
27	9 13 16 26	syl3anc	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
28	27	adantr	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
29	11 5	llnbase	$⊢ u \in N \to u \in {Base}_{K}$
30	29	ad2antrl	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to u \in {Base}_{K}$
31		simprr	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to u \underset{˙}{\leq} (X \underset{˙}{\land} Y)$
32	11 1 23 30 24 25 31 28	lattrd	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to u \underset{˙}{\leq} X$
33		simpl11	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to K \in HL$
34		simprl	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to u \in N$
35		simpl12	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to X \in N$
36	1 5	llncmp	$⊢ (K \in HL \land u \in N \land X \in N) \to (u \underset{˙}{\leq} X \leftrightarrow u = X)$
37	33 34 35 36	syl3anc	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to (u \underset{˙}{\leq} X \leftrightarrow u = X)$
38	32 37	mpbid	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to u = X$
39	38 31	eqbrtrrd	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to X \underset{˙}{\leq} (X \underset{˙}{\land} Y)$
40	11 1 23 24 25 28 39	latasymd	$⊢ (((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \land (u \in N \land u \underset{˙}{\leq} (X \underset{˙}{\land} Y))) \to X \underset{˙}{\land} Y = X$
41	22 40	rexlimddv	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to X \underset{˙}{\land} Y = X$
42	11 1 2	latleeqm1	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\land} Y = X)$
43	9 13 16 42	syl3anc	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to (X \underset{˙}{\leq} Y \leftrightarrow X \underset{˙}{\land} Y = X)$
44	41 43	mpbird	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0}) \land \neg X \underset{˙}{\land} Y \in A) \to X \underset{˙}{\leq} Y$
45	44	3expia	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to (\neg X \underset{˙}{\land} Y \in A \to X \underset{˙}{\leq} Y)$
46	7 45	mt3d	$⊢ ((K \in HL \land X \in N \land Y \in P) \land (\neg X \underset{˙}{\leq} Y \land X \underset{˙}{\land} Y \neq \underset{˙}{0})) \to X \underset{˙}{\land} Y \in A$

Metamath Proof Explorer

Theorem llnmlplnN

Proof