dochexmidlem1

Description: Lemma for dochexmid . Holland's proof implicitly requires q =/= r , which we prove here. (Contributed by NM, 14-Jan-2015)

	Ref	Expression
Hypotheses	dochexmidlem1.h	$⊢ H = LHyp (K)$
	dochexmidlem1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochexmidlem1.u	$⊢ U = DVecH (K) (W)$
	dochexmidlem1.v	$⊢ V = {Base}_{U}$
	dochexmidlem1.s	$⊢ S = LSubSp (U)$
	dochexmidlem1.n	$⊢ N = LSpan (U)$
	dochexmidlem1.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dochexmidlem1.a	$⊢ A = LSAtoms (U)$
	dochexmidlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
	dochexmidlem1.x	$⊢ φ \to X \in S$
	dochexmidlem1.pp	$⊢ φ \to p \in A$
	dochexmidlem1.qq	$⊢ φ \to q \in A$
	dochexmidlem1.rr	$⊢ φ \to r \in A$
	dochexmidlem1.ql	$⊢ φ \to q \subseteq \underset{˙}{⊥} (X)$
	dochexmidlem1.rl	$⊢ φ \to r \subseteq X$
Assertion	dochexmidlem1	$⊢ φ \to q \neq r$

Proof

Step	Hyp	Ref	Expression
1		dochexmidlem1.h	$⊢ H = LHyp (K)$
2		dochexmidlem1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochexmidlem1.u	$⊢ U = DVecH (K) (W)$
4		dochexmidlem1.v	$⊢ V = {Base}_{U}$
5		dochexmidlem1.s	$⊢ S = LSubSp (U)$
6		dochexmidlem1.n	$⊢ N = LSpan (U)$
7		dochexmidlem1.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
8		dochexmidlem1.a	$⊢ A = LSAtoms (U)$
9		dochexmidlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
10		dochexmidlem1.x	$⊢ φ \to X \in S$
11		dochexmidlem1.pp	$⊢ φ \to p \in A$
12		dochexmidlem1.qq	$⊢ φ \to q \in A$
13		dochexmidlem1.rr	$⊢ φ \to r \in A$
14		dochexmidlem1.ql	$⊢ φ \to q \subseteq \underset{˙}{⊥} (X)$
15		dochexmidlem1.rl	$⊢ φ \to r \subseteq X$
16		eqid	$⊢ 0_{U} = 0_{U}$
17	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
18	16 8 17 13	lsatn0	$⊢ φ \to r \neq \{0_{U}\}$
19	5 8 17 13	lsatlssel	$⊢ φ \to r \in S$
20	16 5	lssle0	$⊢ (U \in LMod \land r \in S) \to (r \subseteq \{0_{U}\} \leftrightarrow r = \{0_{U}\})$
21	17 19 20	syl2anc	$⊢ φ \to (r \subseteq \{0_{U}\} \leftrightarrow r = \{0_{U}\})$
22	21	necon3bbid	$⊢ φ \to (\neg r \subseteq \{0_{U}\} \leftrightarrow r \neq \{0_{U}\})$
23	18 22	mpbird	$⊢ φ \to \neg r \subseteq \{0_{U}\}$
24	1 3 5 16 2	dochnoncon	$⊢ ((K \in HL \land W \in H) \land X \in S) \to X \cap \underset{˙}{⊥} (X) = \{0_{U}\}$
25	9 10 24	syl2anc	$⊢ φ \to X \cap \underset{˙}{⊥} (X) = \{0_{U}\}$
26	25	sseq2d	$⊢ φ \to (r \subseteq X \cap \underset{˙}{⊥} (X) \leftrightarrow r \subseteq \{0_{U}\})$
27	23 26	mtbird	$⊢ φ \to \neg r \subseteq X \cap \underset{˙}{⊥} (X)$
28		sseq1	$⊢ q = r \to (q \subseteq \underset{˙}{⊥} (X) \leftrightarrow r \subseteq \underset{˙}{⊥} (X))$
29	14 28	syl5ibcom	$⊢ φ \to (q = r \to r \subseteq \underset{˙}{⊥} (X))$
30	29 15	jctild	$⊢ φ \to (q = r \to (r \subseteq X \land r \subseteq \underset{˙}{⊥} (X)))$
31		ssin	$⊢ (r \subseteq X \land r \subseteq \underset{˙}{⊥} (X)) \leftrightarrow r \subseteq X \cap \underset{˙}{⊥} (X)$
32	30 31	imbitrdi	$⊢ φ \to (q = r \to r \subseteq X \cap \underset{˙}{⊥} (X))$
33	32	necon3bd	$⊢ φ \to (\neg r \subseteq X \cap \underset{˙}{⊥} (X) \to q \neq r)$
34	27 33	mpd	$⊢ φ \to q \neq r$

Metamath Proof Explorer

Theorem dochexmidlem1

Proof