islininds

Description: The property of being a linearly independent subset. (Contributed by AV, 13-Apr-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	islininds.b	$⊢ B = {Base}_{M}$
	islininds.z	$⊢ Z = 0_{M}$
	islininds.r	$⊢ R = Scalar (M)$
	islininds.e	$⊢ E = {Base}_{R}$
	islininds.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	islininds	$⊢ (S \in V \land M \in W) \to (S linIndS M \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})))$

Proof

Step	Hyp	Ref	Expression
1		islininds.b	$⊢ B = {Base}_{M}$
2		islininds.z	$⊢ Z = 0_{M}$
3		islininds.r	$⊢ R = Scalar (M)$
4		islininds.e	$⊢ E = {Base}_{R}$
5		islininds.0	$⊢ \underset{˙}{0} = 0_{R}$
6		simpl	$⊢ (s = S \land m = M) \to s = S$
7		fveq2	$⊢ m = M \to {Base}_{m} = {Base}_{M}$
8	7 1	eqtr4di	$⊢ m = M \to {Base}_{m} = B$
9	8	adantl	$⊢ (s = S \land m = M) \to {Base}_{m} = B$
10	9	pweqd	$⊢ (s = S \land m = M) \to 𝒫 {Base}_{m} = 𝒫 B$
11	6 10	eleq12d	$⊢ (s = S \land m = M) \to (s \in 𝒫 {Base}_{m} \leftrightarrow S \in 𝒫 B)$
12		fveq2	$⊢ m = M \to Scalar (m) = Scalar (M)$
13	12 3	eqtr4di	$⊢ m = M \to Scalar (m) = R$
14	13	fveq2d	$⊢ m = M \to {Base}_{Scalar (m)} = {Base}_{R}$
15	14 4	eqtr4di	$⊢ m = M \to {Base}_{Scalar (m)} = E$
16	15	adantl	$⊢ (s = S \land m = M) \to {Base}_{Scalar (m)} = E$
17	16 6	oveq12d	$⊢ (s = S \land m = M) \to {Base}_{Scalar (m)}^{s} = E^{S}$
18	12	adantl	$⊢ (s = S \land m = M) \to Scalar (m) = Scalar (M)$
19	18 3	eqtr4di	$⊢ (s = S \land m = M) \to Scalar (m) = R$
20	19	fveq2d	$⊢ (s = S \land m = M) \to 0_{Scalar (m)} = 0_{R}$
21	20 5	eqtr4di	$⊢ (s = S \land m = M) \to 0_{Scalar (m)} = \underset{˙}{0}$
22	21	breq2d	$⊢ (s = S \land m = M) \to ({finSupp}_{0_{Scalar (m)}} (f) \leftrightarrow {finSupp}_{\underset{˙}{0}} (f))$
23		fveq2	$⊢ m = M \to linC (m) = linC (M)$
24	23	adantl	$⊢ (s = S \land m = M) \to linC (m) = linC (M)$
25		eqidd	$⊢ (s = S \land m = M) \to f = f$
26	24 25 6	oveq123d	$⊢ (s = S \land m = M) \to f linC (m) s = f linC (M) S$
27		fveq2	$⊢ m = M \to 0_{m} = 0_{M}$
28	27	adantl	$⊢ (s = S \land m = M) \to 0_{m} = 0_{M}$
29	28 2	eqtr4di	$⊢ (s = S \land m = M) \to 0_{m} = Z$
30	26 29	eqeq12d	$⊢ (s = S \land m = M) \to (f linC (m) s = 0_{m} \leftrightarrow f linC (M) S = Z)$
31	22 30	anbi12d	$⊢ (s = S \land m = M) \to (({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) s = 0_{m}) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))$
32	13	fveq2d	$⊢ m = M \to 0_{Scalar (m)} = 0_{R}$
33	32 5	eqtr4di	$⊢ m = M \to 0_{Scalar (m)} = \underset{˙}{0}$
34	33	adantl	$⊢ (s = S \land m = M) \to 0_{Scalar (m)} = \underset{˙}{0}$
35	34	eqeq2d	$⊢ (s = S \land m = M) \to (f (x) = 0_{Scalar (m)} \leftrightarrow f (x) = \underset{˙}{0})$
36	6 35	raleqbidv	$⊢ (s = S \land m = M) \to (\forall x \in s f (x) = 0_{Scalar (m)} \leftrightarrow \forall x \in S f (x) = \underset{˙}{0})$
37	31 36	imbi12d	$⊢ (s = S \land m = M) \to ((({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) s = 0_{m}) \to \forall x \in s f (x) = 0_{Scalar (m)}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))$
38	17 37	raleqbidv	$⊢ (s = S \land m = M) \to (\forall f \in ({Base}_{Scalar (m)}^{s}) (({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) s = 0_{m}) \to \forall x \in s f (x) = 0_{Scalar (m)}) \leftrightarrow \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))$
39	11 38	anbi12d	$⊢ (s = S \land m = M) \to ((s \in 𝒫 {Base}_{m} \land \forall f \in ({Base}_{Scalar (m)}^{s}) (({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) s = 0_{m}) \to \forall x \in s f (x) = 0_{Scalar (m)})) \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})))$
40		df-lininds	$⊢ linIndS = \{⟨s, m⟩ \| (s \in 𝒫 {Base}_{m} \land \forall f \in ({Base}_{Scalar (m)}^{s}) (({finSupp}_{0_{Scalar (m)}} (f) \land f linC (m) s = 0_{m}) \to \forall x \in s f (x) = 0_{Scalar (m)}))\}$
41	39 40	brabga	$⊢ (S \in V \land M \in W) \to (S linIndS M \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})))$

Metamath Proof Explorer

Theorem islininds

Proof