l1cvpat

Description: A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. ( 1cvrjat analog.) (Contributed by NM, 11-Jan-2015)

	Ref	Expression
Hypotheses	l1cvpat.v	$⊢ V = {Base}_{W}$
	l1cvpat.s	$⊢ S = LSubSp (W)$
	l1cvpat.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	l1cvpat.a	$⊢ A = LSAtoms (W)$
	l1cvpat.c	$⊢ C = ⋖_{L} (W)$
	l1cvpat.w	$⊢ φ \to W \in LVec$
	l1cvpat.u	$⊢ φ \to U \in S$
	l1cvpat.q	$⊢ φ \to Q \in A$
	l1cvpat.l	$⊢ φ \to U C V$
	l1cvpat.m	$⊢ φ \to \neg Q \subseteq U$
Assertion	l1cvpat	$⊢ φ \to U \underset{˙}{\oplus} Q = V$

Proof

Step	Hyp	Ref	Expression
1		l1cvpat.v	$⊢ V = {Base}_{W}$
2		l1cvpat.s	$⊢ S = LSubSp (W)$
3		l1cvpat.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		l1cvpat.a	$⊢ A = LSAtoms (W)$
5		l1cvpat.c	$⊢ C = ⋖_{L} (W)$
6		l1cvpat.w	$⊢ φ \to W \in LVec$
7		l1cvpat.u	$⊢ φ \to U \in S$
8		l1cvpat.q	$⊢ φ \to Q \in A$
9		l1cvpat.l	$⊢ φ \to U C V$
10		l1cvpat.m	$⊢ φ \to \neg Q \subseteq U$
11		eqid	$⊢ LSpan (W) = LSpan (W)$
12		eqid	$⊢ 0_{W} = 0_{W}$
13	1 11 12 4	islsat	$⊢ W \in LVec \to (Q \in A \leftrightarrow \exists v \in (V ∖ \{0_{W}\}) Q = LSpan (W) (\{v\}))$
14	6 13	syl	$⊢ φ \to (Q \in A \leftrightarrow \exists v \in (V ∖ \{0_{W}\}) Q = LSpan (W) (\{v\}))$
15	8 14	mpbid	$⊢ φ \to \exists v \in (V ∖ \{0_{W}\}) Q = LSpan (W) (\{v\})$
16		eldifi	$⊢ v \in (V ∖ \{0_{W}\}) \to v \in V$
17		lveclmod	$⊢ W \in LVec \to W \in LMod$
18	6 17	syl	$⊢ φ \to W \in LMod$
19	18	3ad2ant1	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to W \in LMod$
20	7	3ad2ant1	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to U \in S$
21		simp2	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to v \in V$
22	1 2 11 19 20 21	lspsnel5	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to (v \in U \leftrightarrow LSpan (W) (\{v\}) \subseteq U)$
23	22	notbid	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to (\neg v \in U \leftrightarrow \neg LSpan (W) (\{v\}) \subseteq U)$
24		eqid	$⊢ LSHyp (W) = LSHyp (W)$
25	6	3ad2ant1	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to W \in LVec$
26	1 2 24 5 6	islshpcv	$⊢ φ \to (U \in LSHyp (W) \leftrightarrow (U \in S \land U C V))$
27	7 9 26	mpbir2and	$⊢ φ \to U \in LSHyp (W)$
28	27	3ad2ant1	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to U \in LSHyp (W)$
29	1 11 3 24 25 28 21	lshpnelb	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to (\neg v \in U \leftrightarrow U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)$
30	29	biimpd	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to (\neg v \in U \to U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)$
31	23 30	sylbird	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to (\neg LSpan (W) (\{v\}) \subseteq U \to U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)$
32		sseq1	$⊢ Q = LSpan (W) (\{v\}) \to (Q \subseteq U \leftrightarrow LSpan (W) (\{v\}) \subseteq U)$
33	32	notbid	$⊢ Q = LSpan (W) (\{v\}) \to (\neg Q \subseteq U \leftrightarrow \neg LSpan (W) (\{v\}) \subseteq U)$
34		oveq2	$⊢ Q = LSpan (W) (\{v\}) \to U \underset{˙}{\oplus} Q = U \underset{˙}{\oplus} LSpan (W) (\{v\})$
35	34	eqeq1d	$⊢ Q = LSpan (W) (\{v\}) \to (U \underset{˙}{\oplus} Q = V \leftrightarrow U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)$
36	33 35	imbi12d	$⊢ Q = LSpan (W) (\{v\}) \to ((\neg Q \subseteq U \to U \underset{˙}{\oplus} Q = V) \leftrightarrow (\neg LSpan (W) (\{v\}) \subseteq U \to U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
37	36	3ad2ant3	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to ((\neg Q \subseteq U \to U \underset{˙}{\oplus} Q = V) \leftrightarrow (\neg LSpan (W) (\{v\}) \subseteq U \to U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
38	31 37	mpbird	$⊢ (φ \land v \in V \land Q = LSpan (W) (\{v\})) \to (\neg Q \subseteq U \to U \underset{˙}{\oplus} Q = V)$
39	38	3exp	$⊢ φ \to (v \in V \to (Q = LSpan (W) (\{v\}) \to (\neg Q \subseteq U \to U \underset{˙}{\oplus} Q = V)))$
40	16 39	syl5	$⊢ φ \to (v \in (V ∖ \{0_{W}\}) \to (Q = LSpan (W) (\{v\}) \to (\neg Q \subseteq U \to U \underset{˙}{\oplus} Q = V)))$
41	40	rexlimdv	$⊢ φ \to (\exists v \in (V ∖ \{0_{W}\}) Q = LSpan (W) (\{v\}) \to (\neg Q \subseteq U \to U \underset{˙}{\oplus} Q = V))$
42	15 10 41	mp2d	$⊢ φ \to U \underset{˙}{\oplus} Q = V$

Metamath Proof Explorer

Theorem l1cvpat

Proof