islindf2

Description: Property of an independent family of vectors with prior constrained domain and codomain. (Contributed by Stefan O'Rear, 26-Feb-2015)

	Ref	Expression
Hypotheses	islindf.b	$⊢ B = {Base}_{W}$
	islindf.v	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	islindf.k	$⊢ K = LSpan (W)$
	islindf.s	$⊢ S = Scalar (W)$
	islindf.n	$⊢ N = {Base}_{S}$
	islindf.z	$⊢ \underset{˙}{0} = 0_{S}$
Assertion	islindf2	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to (F LIndF W \leftrightarrow \forall x \in I \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} F (x) \in K (F [I ∖ \{x\}]))$

Proof

Step	Hyp	Ref	Expression
1		islindf.b	$⊢ B = {Base}_{W}$
2		islindf.v	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		islindf.k	$⊢ K = LSpan (W)$
4		islindf.s	$⊢ S = Scalar (W)$
5		islindf.n	$⊢ N = {Base}_{S}$
6		islindf.z	$⊢ \underset{˙}{0} = 0_{S}$
7		simp1	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to W \in Y$
8		simp3	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to F : I ⟶ B$
9		simp2	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to I \in X$
10		fex	$⊢ (F : I ⟶ B \land I \in X) \to F \in V$
11	8 9 10	syl2anc	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to F \in V$
12	1 2 3 4 5 6	islindf	$⊢ (W \in Y \land F \in V) \to (F LIndF W \leftrightarrow (F : dom F ⟶ B \land \forall x \in dom F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} F (x) \in K (F [dom F ∖ \{x\}])))$
13	7 11 12	syl2anc	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to (F LIndF W \leftrightarrow (F : dom F ⟶ B \land \forall x \in dom F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} F (x) \in K (F [dom F ∖ \{x\}])))$
14		ffdm	$⊢ F : I ⟶ B \to (F : dom F ⟶ B \land dom F \subseteq I)$
15	14	simpld	$⊢ F : I ⟶ B \to F : dom F ⟶ B$
16	15	3ad2ant3	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to F : dom F ⟶ B$
17	16	biantrurd	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to (\forall x \in dom F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} F (x) \in K (F [dom F ∖ \{x\}]) \leftrightarrow (F : dom F ⟶ B \land \forall x \in dom F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} F (x) \in K (F [dom F ∖ \{x\}])))$
18		fdm	$⊢ F : I ⟶ B \to dom F = I$
19	18	3ad2ant3	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to dom F = I$
20	19	difeq1d	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to dom F ∖ \{x\} = I ∖ \{x\}$
21	20	imaeq2d	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to F [dom F ∖ \{x\}] = F [I ∖ \{x\}]$
22	21	fveq2d	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to K (F [dom F ∖ \{x\}]) = K (F [I ∖ \{x\}])$
23	22	eleq2d	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to (k \underset{˙}{\cdot} F (x) \in K (F [dom F ∖ \{x\}]) \leftrightarrow k \underset{˙}{\cdot} F (x) \in K (F [I ∖ \{x\}]))$
24	23	notbid	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to (\neg k \underset{˙}{\cdot} F (x) \in K (F [dom F ∖ \{x\}]) \leftrightarrow \neg k \underset{˙}{\cdot} F (x) \in K (F [I ∖ \{x\}]))$
25	24	ralbidv	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to (\forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} F (x) \in K (F [dom F ∖ \{x\}]) \leftrightarrow \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} F (x) \in K (F [I ∖ \{x\}]))$
26	19 25	raleqbidv	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to (\forall x \in dom F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} F (x) \in K (F [dom F ∖ \{x\}]) \leftrightarrow \forall x \in I \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} F (x) \in K (F [I ∖ \{x\}]))$
27	13 17 26	3bitr2d	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to (F LIndF W \leftrightarrow \forall x \in I \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} F (x) \in K (F [I ∖ \{x\}]))$

Metamath Proof Explorer

Theorem islindf2

Proof