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	8 9	fexd	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to F \in V$
11	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\}])))$
12	7 10 11	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\}])))$
13		ffdm	$⊢ F : I ⟶ B \to (F : dom F ⟶ B \land dom F \subseteq I)$
14	13	simpld	$⊢ F : I ⟶ B \to F : dom F ⟶ B$
15	14	3ad2ant3	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to F : dom F ⟶ B$
16	15	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\}])))$
17		fdm	$⊢ F : I ⟶ B \to dom F = I$
18	17	3ad2ant3	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to dom F = I$
19	18	difeq1d	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to dom F ∖ \{x\} = I ∖ \{x\}$
20	19	imaeq2d	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to F [dom F ∖ \{x\}] = F [I ∖ \{x\}]$
21	20	fveq2d	$⊢ (W \in Y \land I \in X \land F : I ⟶ B) \to K (F [dom F ∖ \{x\}]) = K (F [I ∖ \{x\}])$
22	21	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\}]))$
23	22	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\}]))$
24	23	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\}]))$
25	18 24	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\}]))$
26	12 16 25	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