lclkrlem2a

Description: Lemma for lclkr . Use lshpat to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2a.h	$⊢ H = LHyp (K)$
	lclkrlem2a.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lclkrlem2a.u	$⊢ U = DVecH (K) (W)$
	lclkrlem2a.v	$⊢ V = {Base}_{U}$
	lclkrlem2a.z	$⊢ \underset{˙}{0} = 0_{U}$
	lclkrlem2a.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	lclkrlem2a.n	$⊢ N = LSpan (U)$
	lclkrlem2a.a	$⊢ A = LSAtoms (U)$
	lclkrlem2a.k	$⊢ φ \to (K \in HL \land W \in H)$
	lclkrlem2a.b	$⊢ φ \to B \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2a.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2a.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lclkrlem2a.e	$⊢ φ \to \underset{˙}{⊥} (\{X\}) \neq \underset{˙}{⊥} (\{Y\})$
	lclkrlem2a.d	$⊢ φ \to \neg X \in \underset{˙}{⊥} (\{B\})$
Assertion	lclkrlem2a	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\}) \in A$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2a.h	$⊢ H = LHyp (K)$
2		lclkrlem2a.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lclkrlem2a.u	$⊢ U = DVecH (K) (W)$
4		lclkrlem2a.v	$⊢ V = {Base}_{U}$
5		lclkrlem2a.z	$⊢ \underset{˙}{0} = 0_{U}$
6		lclkrlem2a.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
7		lclkrlem2a.n	$⊢ N = LSpan (U)$
8		lclkrlem2a.a	$⊢ A = LSAtoms (U)$
9		lclkrlem2a.k	$⊢ φ \to (K \in HL \land W \in H)$
10		lclkrlem2a.b	$⊢ φ \to B \in (V ∖ \{\underset{˙}{0}\})$
11		lclkrlem2a.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
12		lclkrlem2a.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
13		lclkrlem2a.e	$⊢ φ \to \underset{˙}{⊥} (\{X\}) \neq \underset{˙}{⊥} (\{Y\})$
14		lclkrlem2a.d	$⊢ φ \to \neg X \in \underset{˙}{⊥} (\{B\})$
15		eqid	$⊢ LSubSp (U) = LSubSp (U)$
16		eqid	$⊢ LSHyp (U) = LSHyp (U)$
17	1 3 9	dvhlvec	$⊢ φ \to U \in LVec$
18	1 2 3 4 5 16 9 10	dochsnshp	$⊢ φ \to \underset{˙}{⊥} (\{B\}) \in LSHyp (U)$
19	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
20	4 7 5 8 19 11	lsatlspsn	$⊢ φ \to N (\{X\}) \in A$
21	4 7 5 8 19 12	lsatlspsn	$⊢ φ \to N (\{Y\}) \in A$
22	11	eldifad	$⊢ φ \to X \in V$
23	22	snssd	$⊢ φ \to \{X\} \subseteq V$
24	1 3 2 4 7 9 23	dochocsp	$⊢ φ \to \underset{˙}{⊥} (N (\{X\})) = \underset{˙}{⊥} (\{X\})$
25	12	eldifad	$⊢ φ \to Y \in V$
26	25	snssd	$⊢ φ \to \{Y\} \subseteq V$
27	1 3 2 4 7 9 26	dochocsp	$⊢ φ \to \underset{˙}{⊥} (N (\{Y\})) = \underset{˙}{⊥} (\{Y\})$
28	24 27	eqeq12d	$⊢ φ \to (\underset{˙}{⊥} (N (\{X\})) = \underset{˙}{⊥} (N (\{Y\})) \leftrightarrow \underset{˙}{⊥} (\{X\}) = \underset{˙}{⊥} (\{Y\}))$
29		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
30	1 3 4 7 29	dihlsprn	$⊢ ((K \in HL \land W \in H) \land X \in V) \to N (\{X\}) \in ran DIsoH (K) (W)$
31	9 22 30	syl2anc	$⊢ φ \to N (\{X\}) \in ran DIsoH (K) (W)$
32	1 3 4 7 29	dihlsprn	$⊢ ((K \in HL \land W \in H) \land Y \in V) \to N (\{Y\}) \in ran DIsoH (K) (W)$
33	9 25 32	syl2anc	$⊢ φ \to N (\{Y\}) \in ran DIsoH (K) (W)$
34	1 29 2 9 31 33	doch11	$⊢ φ \to (\underset{˙}{⊥} (N (\{X\})) = \underset{˙}{⊥} (N (\{Y\})) \leftrightarrow N (\{X\}) = N (\{Y\}))$
35	28 34	bitr3d	$⊢ φ \to (\underset{˙}{⊥} (\{X\}) = \underset{˙}{⊥} (\{Y\}) \leftrightarrow N (\{X\}) = N (\{Y\}))$
36	35	necon3bid	$⊢ φ \to (\underset{˙}{⊥} (\{X\}) \neq \underset{˙}{⊥} (\{Y\}) \leftrightarrow N (\{X\}) \neq N (\{Y\}))$
37	13 36	mpbid	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
38	10	eldifad	$⊢ φ \to B \in V$
39	38	snssd	$⊢ φ \to \{B\} \subseteq V$
40	1 3 4 15 2	dochlss	$⊢ ((K \in HL \land W \in H) \land \{B\} \subseteq V) \to \underset{˙}{⊥} (\{B\}) \in LSubSp (U)$
41	9 39 40	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{B\}) \in LSubSp (U)$
42	4 15 7 19 41 22	ellspsn5b	$⊢ φ \to (X \in \underset{˙}{⊥} (\{B\}) \leftrightarrow N (\{X\}) \subseteq \underset{˙}{⊥} (\{B\}))$
43	14 42	mtbid	$⊢ φ \to \neg N (\{X\}) \subseteq \underset{˙}{⊥} (\{B\})$
44	15 6 16 8 17 18 20 21 37 43	lshpat	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (\{B\}) \in A$

Metamath Proof Explorer

Theorem lclkrlem2a

Proof