lcoss

Description: A set of vectors of a module is a subset of the set of all linear combinations of the set. (Contributed by AV, 18-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

		Ref	Expression
	Assertion	lcoss	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to V \subseteq M LinCo V$

Proof

Step	Hyp	Ref	Expression
1		elelpwi	$⊢ (v \in V \land V \in 𝒫 {Base}_{M}) \to v \in {Base}_{M}$
2	1	expcom	$⊢ V \in 𝒫 {Base}_{M} \to (v \in V \to v \in {Base}_{M})$
3	2	adantl	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (v \in V \to v \in {Base}_{M})$
4	3	imp	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to v \in {Base}_{M}$
5		eqid	$⊢ {Base}_{M} = {Base}_{M}$
6		eqid	$⊢ Scalar (M) = Scalar (M)$
7		eqid	$⊢ 0_{Scalar (M)} = 0_{Scalar (M)}$
8		eqid	$⊢ 1_{Scalar (M)} = 1_{Scalar (M)}$
9		equequ1	$⊢ x = y \to (x = v \leftrightarrow y = v)$
10	9	ifbid	$⊢ x = y \to if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)}) = if (y = v, 1_{Scalar (M)}, 0_{Scalar (M)})$
11	10	cbvmptv	$⊢ (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) = (y \in V ⟼ if (y = v, 1_{Scalar (M)}, 0_{Scalar (M)}))$
12	5 6 7 8 11	mptcfsupp	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land v \in V) \to {finSupp}_{0_{Scalar (M)}} ((x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})))$
13	12	3expa	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to {finSupp}_{0_{Scalar (M)}} ((x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})))$
14		eqid	$⊢ (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)}))$
15	5 6 7 8 14	linc1	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land v \in V) \to (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) V = v$
16	15	3expa	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) V = v$
17	16	eqcomd	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to v = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) V$
18		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
19	6 18 8	lmod1cl	$⊢ M \in LMod \to 1_{Scalar (M)} \in {Base}_{Scalar (M)}$
20	6 18 7	lmod0cl	$⊢ M \in LMod \to 0_{Scalar (M)} \in {Base}_{Scalar (M)}$
21	19 20	ifcld	$⊢ M \in LMod \to if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)}) \in {Base}_{Scalar (M)}$
22	21	ad3antrrr	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \land x \in V) \to if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)}) \in {Base}_{Scalar (M)}$
23	22	fmpttd	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) : V ⟶ {Base}_{Scalar (M)}$
24		fvex	$⊢ {Base}_{Scalar (M)} \in V$
25		simplr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to V \in 𝒫 {Base}_{M}$
26		elmapg	$⊢ ({Base}_{Scalar (M)} \in V \land V \in 𝒫 {Base}_{M}) \to ((x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) \in ({Base}_{Scalar (M)}^{V}) \leftrightarrow (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) : V ⟶ {Base}_{Scalar (M)})$
27	24 25 26	sylancr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to ((x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) \in ({Base}_{Scalar (M)}^{V}) \leftrightarrow (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) : V ⟶ {Base}_{Scalar (M)})$
28	23 27	mpbird	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) \in ({Base}_{Scalar (M)}^{V})$
29		breq1	$⊢ f = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) \to ({finSupp}_{0_{Scalar (M)}} (f) \leftrightarrow {finSupp}_{0_{Scalar (M)}} ((x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)}))))$
30		oveq1	$⊢ f = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) \to f linC (M) V = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) V$
31	30	eqeq2d	$⊢ f = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) \to (v = f linC (M) V \leftrightarrow v = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) V)$
32	29 31	anbi12d	$⊢ f = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) \to (({finSupp}_{0_{Scalar (M)}} (f) \land v = f linC (M) V) \leftrightarrow ({finSupp}_{0_{Scalar (M)}} ((x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)}))) \land v = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) V))$
33	32	adantl	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \land f = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)}))) \to (({finSupp}_{0_{Scalar (M)}} (f) \land v = f linC (M) V) \leftrightarrow ({finSupp}_{0_{Scalar (M)}} ((x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)}))) \land v = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) V))$
34	28 33	rspcedv	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to (({finSupp}_{0_{Scalar (M)}} ((x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)}))) \land v = (x \in V ⟼ if (x = v, 1_{Scalar (M)}, 0_{Scalar (M)})) linC (M) V) \to \exists f \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (f) \land v = f linC (M) V))$
35	13 17 34	mp2and	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to \exists f \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (f) \land v = f linC (M) V)$
36	5 6 18	lcoval	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (v \in (M LinCo V) \leftrightarrow (v \in {Base}_{M} \land \exists f \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (f) \land v = f linC (M) V)))$
37	36	adantr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to (v \in (M LinCo V) \leftrightarrow (v \in {Base}_{M} \land \exists f \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (f) \land v = f linC (M) V)))$
38	4 35 37	mpbir2and	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land v \in V) \to v \in (M LinCo V)$
39	38	ex	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (v \in V \to v \in (M LinCo V))$
40	39	ssrdv	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to V \subseteq M LinCo V$

Metamath Proof Explorer

Theorem lcoss

Proof