lsmsatcv

Description: Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of Kalmbach p. 153. ( spansncvi analog.) Explicit atom version of lsmcv . (Contributed by NM, 29-Oct-2014)

	Ref	Expression
Hypotheses	lsmsatcv.s	$⊢ S = LSubSp (W)$
	lsmsatcv.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsmsatcv.a	$⊢ A = LSAtoms (W)$
	lsmsatcv.w	$⊢ φ \to W \in LVec$
	lsmsatcv.t	$⊢ φ \to T \in S$
	lsmsatcv.u	$⊢ φ \to U \in S$
	lsmsatcv.x	$⊢ φ \to Q \in A$
Assertion	lsmsatcv	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} Q) \to U = T \underset{˙}{\oplus} Q$

Proof

Step	Hyp	Ref	Expression
1		lsmsatcv.s	$⊢ S = LSubSp (W)$
2		lsmsatcv.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lsmsatcv.a	$⊢ A = LSAtoms (W)$
4		lsmsatcv.w	$⊢ φ \to W \in LVec$
5		lsmsatcv.t	$⊢ φ \to T \in S$
6		lsmsatcv.u	$⊢ φ \to U \in S$
7		lsmsatcv.x	$⊢ φ \to Q \in A$
8		eqid	$⊢ {Base}_{W} = {Base}_{W}$
9		eqid	$⊢ LSpan (W) = LSpan (W)$
10	8 9 3	islsati	$⊢ (W \in LVec \land Q \in A) \to \exists v \in {Base}_{W} Q = LSpan (W) (\{v\})$
11	4 7 10	syl2anc	$⊢ φ \to \exists v \in {Base}_{W} Q = LSpan (W) (\{v\})$
12	4	adantr	$⊢ (φ \land v \in {Base}_{W}) \to W \in LVec$
13	5	adantr	$⊢ (φ \land v \in {Base}_{W}) \to T \in S$
14	6	adantr	$⊢ (φ \land v \in {Base}_{W}) \to U \in S$
15		simpr	$⊢ (φ \land v \in {Base}_{W}) \to v \in {Base}_{W}$
16	8 1 9 2 12 13 14 15	lsmcv	$⊢ ((φ \land v \in {Base}_{W}) \land T \subset U \land U \subseteq T \underset{˙}{\oplus} LSpan (W) (\{v\})) \to U = T \underset{˙}{\oplus} LSpan (W) (\{v\})$
17	16	3expib	$⊢ (φ \land v \in {Base}_{W}) \to ((T \subset U \land U \subseteq T \underset{˙}{\oplus} LSpan (W) (\{v\})) \to U = T \underset{˙}{\oplus} LSpan (W) (\{v\}))$
18	17	3adant3	$⊢ (φ \land v \in {Base}_{W} \land Q = LSpan (W) (\{v\})) \to ((T \subset U \land U \subseteq T \underset{˙}{\oplus} LSpan (W) (\{v\})) \to U = T \underset{˙}{\oplus} LSpan (W) (\{v\}))$
19		oveq2	$⊢ Q = LSpan (W) (\{v\}) \to T \underset{˙}{\oplus} Q = T \underset{˙}{\oplus} LSpan (W) (\{v\})$
20	19	sseq2d	$⊢ Q = LSpan (W) (\{v\}) \to (U \subseteq T \underset{˙}{\oplus} Q \leftrightarrow U \subseteq T \underset{˙}{\oplus} LSpan (W) (\{v\}))$
21	20	anbi2d	$⊢ Q = LSpan (W) (\{v\}) \to ((T \subset U \land U \subseteq T \underset{˙}{\oplus} Q) \leftrightarrow (T \subset U \land U \subseteq T \underset{˙}{\oplus} LSpan (W) (\{v\})))$
22	19	eqeq2d	$⊢ Q = LSpan (W) (\{v\}) \to (U = T \underset{˙}{\oplus} Q \leftrightarrow U = T \underset{˙}{\oplus} LSpan (W) (\{v\}))$
23	21 22	imbi12d	$⊢ Q = LSpan (W) (\{v\}) \to (((T \subset U \land U \subseteq T \underset{˙}{\oplus} Q) \to U = T \underset{˙}{\oplus} Q) \leftrightarrow ((T \subset U \land U \subseteq T \underset{˙}{\oplus} LSpan (W) (\{v\})) \to U = T \underset{˙}{\oplus} LSpan (W) (\{v\})))$
24	23	3ad2ant3	$⊢ (φ \land v \in {Base}_{W} \land Q = LSpan (W) (\{v\})) \to (((T \subset U \land U \subseteq T \underset{˙}{\oplus} Q) \to U = T \underset{˙}{\oplus} Q) \leftrightarrow ((T \subset U \land U \subseteq T \underset{˙}{\oplus} LSpan (W) (\{v\})) \to U = T \underset{˙}{\oplus} LSpan (W) (\{v\})))$
25	18 24	mpbird	$⊢ (φ \land v \in {Base}_{W} \land Q = LSpan (W) (\{v\})) \to ((T \subset U \land U \subseteq T \underset{˙}{\oplus} Q) \to U = T \underset{˙}{\oplus} Q)$
26	25	rexlimdv3a	$⊢ φ \to (\exists v \in {Base}_{W} Q = LSpan (W) (\{v\}) \to ((T \subset U \land U \subseteq T \underset{˙}{\oplus} Q) \to U = T \underset{˙}{\oplus} Q))$
27	11 26	mpd	$⊢ φ \to ((T \subset U \land U \subseteq T \underset{˙}{\oplus} Q) \to U = T \underset{˙}{\oplus} Q)$
28	27	3impib	$⊢ (φ \land T \subset U \land U \subseteq T \underset{˙}{\oplus} Q) \to U = T \underset{˙}{\oplus} Q$

Metamath Proof Explorer

Theorem lsmsatcv

Proof