dochexmidlem4

	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$
	dochexmidlem4.pp	$⊢ φ \to p \in A$
	dochexmidlem4.qq	$⊢ φ \to q \in A$
	dochexmidlem4.z	$⊢ \underset{˙}{0} = 0_{U}$
	dochexmidlem4.m	$⊢ M = X \underset{˙}{\oplus} p$
	dochexmidlem4.xn	$⊢ φ \to X \neq \{\underset{˙}{0}\}$
	dochexmidlem4.pl	$⊢ φ \to q \subseteq \underset{˙}{⊥} (X) \cap M$
Assertion	dochexmidlem4	$⊢ φ \to p \subseteq X \underset{˙}{\oplus} \underset{˙}{⊥} (X)$

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		dochexmidlem4.pp	$⊢ φ \to p \in A$
12		dochexmidlem4.qq	$⊢ φ \to q \in A$
13		dochexmidlem4.z	$⊢ \underset{˙}{0} = 0_{U}$
14		dochexmidlem4.m	$⊢ M = X \underset{˙}{\oplus} p$
15		dochexmidlem4.xn	$⊢ φ \to X \neq \{\underset{˙}{0}\}$
16		dochexmidlem4.pl	$⊢ φ \to q \subseteq \underset{˙}{⊥} (X) \cap M$
17	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
18	5 8 17 11	lsatlssel	$⊢ φ \to p \in S$
19		inss2	$⊢ \underset{˙}{⊥} (X) \cap M \subseteq M$
20	16 19	sstrdi	$⊢ φ \to q \subseteq M$
21	20 14	sseqtrdi	$⊢ φ \to q \subseteq X \underset{˙}{\oplus} p$
22	13 5 7 8 17 10 18 12 15 21	lsmsat	$⊢ φ \to \exists r \in A (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p)$
23	9	3ad2ant1	$⊢ (φ \land r \in A \land (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p)) \to (K \in HL \land W \in H)$
24	10	3ad2ant1	$⊢ (φ \land r \in A \land (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p)) \to X \in S$
25	11	3ad2ant1	$⊢ (φ \land r \in A \land (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p)) \to p \in A$
26	12	3ad2ant1	$⊢ (φ \land r \in A \land (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p)) \to q \in A$
27		simp2	$⊢ (φ \land r \in A \land (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p)) \to r \in A$
28		inss1	$⊢ \underset{˙}{⊥} (X) \cap M \subseteq \underset{˙}{⊥} (X)$
29	16 28	sstrdi	$⊢ φ \to q \subseteq \underset{˙}{⊥} (X)$
30	29	3ad2ant1	$⊢ (φ \land r \in A \land (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p)) \to q \subseteq \underset{˙}{⊥} (X)$
31		simp3l	$⊢ (φ \land r \in A \land (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p)) \to r \subseteq X$
32		simp3r	$⊢ (φ \land r \in A \land (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p)) \to q \subseteq r \underset{˙}{\oplus} p$
33	1 2 3 4 5 6 7 8 23 24 25 26 27 30 31 32	dochexmidlem3	$⊢ (φ \land r \in A \land (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p)) \to p \subseteq X \underset{˙}{\oplus} \underset{˙}{⊥} (X)$
34	33	rexlimdv3a	$⊢ φ \to (\exists r \in A (r \subseteq X \land q \subseteq r \underset{˙}{\oplus} p) \to p \subseteq X \underset{˙}{\oplus} \underset{˙}{⊥} (X))$
35	22 34	mpd	$⊢ φ \to p \subseteq X \underset{˙}{\oplus} \underset{˙}{⊥} (X)$

Metamath Proof Explorer

Theorem dochexmidlem4

Proof