lcv1

Description: Covering property of a subspace plus an atom. ( chcv1 analog.) (Contributed by NM, 10-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lcv1.s	$⊢ S = LSubSp (W)$
2		lcv1.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lcv1.a	$⊢ A = LSAtoms (W)$
4		lcv1.c	$⊢ C = ⋖_{L} (W)$
5		lcv1.w	$⊢ φ \to W \in LVec$
6		lcv1.u	$⊢ φ \to U \in S$
7		lcv1.q	$⊢ φ \to Q \in A$
8		eqid	$⊢ {Base}_{W} = {Base}_{W}$
9		eqid	$⊢ LSpan (W) = LSpan (W)$
10		eqid	$⊢ 0_{W} = 0_{W}$
11	8 9 10 3	islsat	$⊢ W \in LVec \to (Q \in A \leftrightarrow \exists x \in ({Base}_{W} ∖ \{0_{W}\}) Q = LSpan (W) (\{x\}))$
12	5 11	syl	$⊢ φ \to (Q \in A \leftrightarrow \exists x \in ({Base}_{W} ∖ \{0_{W}\}) Q = LSpan (W) (\{x\}))$
13	7 12	mpbid	$⊢ φ \to \exists x \in ({Base}_{W} ∖ \{0_{W}\}) Q = LSpan (W) (\{x\})$
14	13	adantr	$⊢ (φ \land \neg Q \subseteq U) \to \exists x \in ({Base}_{W} ∖ \{0_{W}\}) Q = LSpan (W) (\{x\})$
15	5	adantr	$⊢ (φ \land \neg Q \subseteq U) \to W \in LVec$
16	15	3ad2ant1	$⊢ ((φ \land \neg Q \subseteq U) \land x \in ({Base}_{W} ∖ \{0_{W}\}) \land Q = LSpan (W) (\{x\})) \to W \in LVec$
17	6	adantr	$⊢ (φ \land \neg Q \subseteq U) \to U \in S$
18	17	3ad2ant1	$⊢ ((φ \land \neg Q \subseteq U) \land x \in ({Base}_{W} ∖ \{0_{W}\}) \land Q = LSpan (W) (\{x\})) \to U \in S$
19		eldifi	$⊢ x \in ({Base}_{W} ∖ \{0_{W}\}) \to x \in {Base}_{W}$
20	19	3ad2ant2	$⊢ ((φ \land \neg Q \subseteq U) \land x \in ({Base}_{W} ∖ \{0_{W}\}) \land Q = LSpan (W) (\{x\})) \to x \in {Base}_{W}$
21		simp1r	$⊢ ((φ \land \neg Q \subseteq U) \land x \in ({Base}_{W} ∖ \{0_{W}\}) \land Q = LSpan (W) (\{x\})) \to \neg Q \subseteq U$
22		simp3	$⊢ ((φ \land \neg Q \subseteq U) \land x \in ({Base}_{W} ∖ \{0_{W}\}) \land Q = LSpan (W) (\{x\})) \to Q = LSpan (W) (\{x\})$
23	22	sseq1d	$⊢ ((φ \land \neg Q \subseteq U) \land x \in ({Base}_{W} ∖ \{0_{W}\}) \land Q = LSpan (W) (\{x\})) \to (Q \subseteq U \leftrightarrow LSpan (W) (\{x\}) \subseteq U)$
24	21 23	mtbid	$⊢ ((φ \land \neg Q \subseteq U) \land x \in ({Base}_{W} ∖ \{0_{W}\}) \land Q = LSpan (W) (\{x\})) \to \neg LSpan (W) (\{x\}) \subseteq U$
25	8 1 9 2 4 16 18 20 24	lsmcv2	$⊢ ((φ \land \neg Q \subseteq U) \land x \in ({Base}_{W} ∖ \{0_{W}\}) \land Q = LSpan (W) (\{x\})) \to U C (U \underset{˙}{\oplus} LSpan (W) (\{x\}))$
26	22	oveq2d	$⊢ ((φ \land \neg Q \subseteq U) \land x \in ({Base}_{W} ∖ \{0_{W}\}) \land Q = LSpan (W) (\{x\})) \to U \underset{˙}{\oplus} Q = U \underset{˙}{\oplus} LSpan (W) (\{x\})$
27	25 26	breqtrrd	$⊢ ((φ \land \neg Q \subseteq U) \land x \in ({Base}_{W} ∖ \{0_{W}\}) \land Q = LSpan (W) (\{x\})) \to U C (U \underset{˙}{\oplus} Q)$
28	27	rexlimdv3a	$⊢ (φ \land \neg Q \subseteq U) \to (\exists x \in ({Base}_{W} ∖ \{0_{W}\}) Q = LSpan (W) (\{x\}) \to U C (U \underset{˙}{\oplus} Q))$
29	14 28	mpd	$⊢ (φ \land \neg Q \subseteq U) \to U C (U \underset{˙}{\oplus} Q)$
30	5	adantr	$⊢ (φ \land U C (U \underset{˙}{\oplus} Q)) \to W \in LVec$
31	6	adantr	$⊢ (φ \land U C (U \underset{˙}{\oplus} Q)) \to U \in S$
32		lveclmod	$⊢ W \in LVec \to W \in LMod$
33	5 32	syl	$⊢ φ \to W \in LMod$
34	1 3 33 7	lsatlssel	$⊢ φ \to Q \in S$
35	1 2	lsmcl	$⊢ (W \in LMod \land U \in S \land Q \in S) \to U \underset{˙}{\oplus} Q \in S$
36	33 6 34 35	syl3anc	$⊢ φ \to U \underset{˙}{\oplus} Q \in S$
37	36	adantr	$⊢ (φ \land U C (U \underset{˙}{\oplus} Q)) \to U \underset{˙}{\oplus} Q \in S$
38		simpr	$⊢ (φ \land U C (U \underset{˙}{\oplus} Q)) \to U C (U \underset{˙}{\oplus} Q)$
39	1 4 30 31 37 38	lcvpss	$⊢ (φ \land U C (U \underset{˙}{\oplus} Q)) \to U \subset U \underset{˙}{\oplus} Q$
40	1	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
41	33 40	syl	$⊢ φ \to S \subseteq SubGrp (W)$
42	41 6	sseldd	$⊢ φ \to U \in SubGrp (W)$
43	41 34	sseldd	$⊢ φ \to Q \in SubGrp (W)$
44	2 42 43	lssnle	$⊢ φ \to (\neg Q \subseteq U \leftrightarrow U \subset U \underset{˙}{\oplus} Q)$
45	44	adantr	$⊢ (φ \land U C (U \underset{˙}{\oplus} Q)) \to (\neg Q \subseteq U \leftrightarrow U \subset U \underset{˙}{\oplus} Q)$
46	39 45	mpbird	$⊢ (φ \land U C (U \underset{˙}{\oplus} Q)) \to \neg Q \subseteq U$
47	29 46	impbida	$⊢ φ \to (\neg Q \subseteq U \leftrightarrow U C (U \underset{˙}{\oplus} Q))$

Metamath Proof Explorer

Theorem lcv1

Proof