dvh4dimlem

	Ref	Expression
Hypotheses	dvh3dim.h	$⊢ H = LHyp (K)$
	dvh3dim.u	$⊢ U = DVecH (K) (W)$
	dvh3dim.v	$⊢ V = {Base}_{U}$
	dvh3dim.n	$⊢ N = LSpan (U)$
	dvh3dim.k	$⊢ φ \to (K \in HL \land W \in H)$
	dvh3dim.x	$⊢ φ \to X \in V$
	dvh4dim.y	$⊢ φ \to Y \in V$
	dvhdim.z	$⊢ φ \to Z \in V$
	dvh4dim.o	$⊢ \underset{˙}{0} = 0_{U}$
	dvh4dim.x	$⊢ φ \to X \neq \underset{˙}{0}$
	dvh4dimlem.y	$⊢ φ \to Y \neq \underset{˙}{0}$
	dvh4dimlem.z	$⊢ φ \to Z \neq \underset{˙}{0}$
Assertion	dvh4dimlem	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Y, Z\})$

Proof

Step	Hyp	Ref	Expression
1		dvh3dim.h	$⊢ H = LHyp (K)$
2		dvh3dim.u	$⊢ U = DVecH (K) (W)$
3		dvh3dim.v	$⊢ V = {Base}_{U}$
4		dvh3dim.n	$⊢ N = LSpan (U)$
5		dvh3dim.k	$⊢ φ \to (K \in HL \land W \in H)$
6		dvh3dim.x	$⊢ φ \to X \in V$
7		dvh4dim.y	$⊢ φ \to Y \in V$
8		dvhdim.z	$⊢ φ \to Z \in V$
9		dvh4dim.o	$⊢ \underset{˙}{0} = 0_{U}$
10		dvh4dim.x	$⊢ φ \to X \neq \underset{˙}{0}$
11		dvh4dimlem.y	$⊢ φ \to Y \neq \underset{˙}{0}$
12		dvh4dimlem.z	$⊢ φ \to Z \neq \underset{˙}{0}$
13		eqid	$⊢ LSSum (U) = LSSum (U)$
14		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
15	1 2 5	dvhlmod	$⊢ φ \to U \in LMod$
16		eldifsn	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in V \land X \neq \underset{˙}{0})$
17	6 10 16	sylanbrc	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
18	3 4 9 14 15 17	lsatlspsn	$⊢ φ \to N (\{X\}) \in LSAtoms (U)$
19		eldifsn	$⊢ Y \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (Y \in V \land Y \neq \underset{˙}{0})$
20	7 11 19	sylanbrc	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
21	3 4 9 14 15 20	lsatlspsn	$⊢ φ \to N (\{Y\}) \in LSAtoms (U)$
22		eldifsn	$⊢ Z \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (Z \in V \land Z \neq \underset{˙}{0})$
23	8 12 22	sylanbrc	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
24	3 4 9 14 15 23	lsatlspsn	$⊢ φ \to N (\{Z\}) \in LSAtoms (U)$
25	1 2 13 14 5 18 21 24	dvh4dimat	$⊢ φ \to \exists p \in LSAtoms (U) \neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\})$
26	15	3ad2ant1	$⊢ (φ \land p \in LSAtoms (U) \land \neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\})) \to U \in LMod$
27		simp2	$⊢ (φ \land p \in LSAtoms (U) \land \neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\})) \to p \in LSAtoms (U)$
28	3 4 14	islsati	$⊢ (U \in LMod \land p \in LSAtoms (U)) \to \exists z \in V p = N (\{z\})$
29	26 27 28	syl2anc	$⊢ (φ \land p \in LSAtoms (U) \land \neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\})) \to \exists z \in V p = N (\{z\})$
30		simp2	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to p = N (\{z\})$
31	15	3ad2ant1	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to U \in LMod$
32	6	3ad2ant1	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to X \in V$
33	7	3ad2ant1	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to Y \in V$
34	3 4 13 31 32 33	lsmpr	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to N (\{X, Y\}) = N (\{X\}) LSSum (U) N (\{Y\})$
35	34	oveq1d	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to N (\{X, Y\}) LSSum (U) N (\{Z\}) = (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\})$
36		prssi	$⊢ (X \in V \land Y \in V) \to \{X, Y\} \subseteq V$
37	6 7 36	syl2anc	$⊢ φ \to \{X, Y\} \subseteq V$
38	37	3ad2ant1	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to \{X, Y\} \subseteq V$
39	8	snssd	$⊢ φ \to \{Z\} \subseteq V$
40	39	3ad2ant1	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to \{Z\} \subseteq V$
41	3 4 13	lsmsp2	$⊢ (U \in LMod \land \{X, Y\} \subseteq V \land \{Z\} \subseteq V) \to N (\{X, Y\}) LSSum (U) N (\{Z\}) = N (\{X, Y\} \cup \{Z\})$
42	31 38 40 41	syl3anc	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to N (\{X, Y\}) LSSum (U) N (\{Z\}) = N (\{X, Y\} \cup \{Z\})$
43	35 42	eqtr3d	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\}) = N (\{X, Y\} \cup \{Z\})$
44	30 43	sseq12d	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to (p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\}) \leftrightarrow N (\{z\}) \subseteq N (\{X, Y\} \cup \{Z\}))$
45		eqid	$⊢ LSubSp (U) = LSubSp (U)$
46	37 39	unssd	$⊢ φ \to \{X, Y\} \cup \{Z\} \subseteq V$
47	3 45 4	lspcl	$⊢ (U \in LMod \land \{X, Y\} \cup \{Z\} \subseteq V) \to N (\{X, Y\} \cup \{Z\}) \in LSubSp (U)$
48	15 46 47	syl2anc	$⊢ φ \to N (\{X, Y\} \cup \{Z\}) \in LSubSp (U)$
49	48	3ad2ant1	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to N (\{X, Y\} \cup \{Z\}) \in LSubSp (U)$
50		simp3	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to z \in V$
51	3 45 4 31 49 50	lspsnel5	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to (z \in N (\{X, Y\} \cup \{Z\}) \leftrightarrow N (\{z\}) \subseteq N (\{X, Y\} \cup \{Z\}))$
52	44 51	bitr4d	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to (p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\}) \leftrightarrow z \in N (\{X, Y\} \cup \{Z\}))$
53		df-tp	$⊢ \{X, Y, Z\} = \{X, Y\} \cup \{Z\}$
54	53	fveq2i	$⊢ N (\{X, Y, Z\}) = N (\{X, Y\} \cup \{Z\})$
55	54	eleq2i	$⊢ z \in N (\{X, Y, Z\}) \leftrightarrow z \in N (\{X, Y\} \cup \{Z\})$
56	52 55	bitr4di	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to (p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\}) \leftrightarrow z \in N (\{X, Y, Z\}))$
57	56	notbid	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to (\neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\}) \leftrightarrow \neg z \in N (\{X, Y, Z\}))$
58	57	biimpd	$⊢ (φ \land p = N (\{z\}) \land z \in V) \to (\neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\}) \to \neg z \in N (\{X, Y, Z\}))$
59	58	3exp	$⊢ φ \to (p = N (\{z\}) \to (z \in V \to (\neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\}) \to \neg z \in N (\{X, Y, Z\}))))$
60	59	com24	$⊢ φ \to (\neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\}) \to (z \in V \to (p = N (\{z\}) \to \neg z \in N (\{X, Y, Z\}))))$
61	60	a1d	$⊢ φ \to (p \in LSAtoms (U) \to (\neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\}) \to (z \in V \to (p = N (\{z\}) \to \neg z \in N (\{X, Y, Z\})))))$
62	61	3imp	$⊢ (φ \land p \in LSAtoms (U) \land \neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\})) \to (z \in V \to (p = N (\{z\}) \to \neg z \in N (\{X, Y, Z\})))$
63	62	reximdvai	$⊢ (φ \land p \in LSAtoms (U) \land \neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\})) \to (\exists z \in V p = N (\{z\}) \to \exists z \in V \neg z \in N (\{X, Y, Z\}))$
64	29 63	mpd	$⊢ (φ \land p \in LSAtoms (U) \land \neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\})) \to \exists z \in V \neg z \in N (\{X, Y, Z\})$
65	64	rexlimdv3a	$⊢ φ \to (\exists p \in LSAtoms (U) \neg p \subseteq (N (\{X\}) LSSum (U) N (\{Y\})) LSSum (U) N (\{Z\}) \to \exists z \in V \neg z \in N (\{X, Y, Z\}))$
66	25 65	mpd	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Y, Z\})$

Metamath Proof Explorer

Theorem dvh4dimlem

Proof