islinds2

Description: Expanded property of an independent set of vectors. (Contributed by Stefan O'Rear, 24-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	islinds2	$⊢ W \in Y \to (F \in LIndS (W) \leftrightarrow (F \subseteq B \land \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{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	1	islinds	$⊢ W \in Y \to (F \in LIndS (W) \leftrightarrow (F \subseteq B \land ({I ↾}_{F}) LIndF W))$
8	1	fvexi	$⊢ B \in V$
9	8	ssex	$⊢ F \subseteq B \to F \in V$
10	9	adantl	$⊢ (W \in Y \land F \subseteq B) \to F \in V$
11		resiexg	$⊢ F \in V \to {I ↾}_{F} \in V$
12	10 11	syl	$⊢ (W \in Y \land F \subseteq B) \to {I ↾}_{F} \in V$
13	1 2 3 4 5 6	islindf	$⊢ (W \in Y \land {I ↾}_{F} \in V) \to (({I ↾}_{F}) LIndF W \leftrightarrow (({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B \land \forall x \in dom ({I ↾}_{F}) \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}])))$
14	12 13	syldan	$⊢ (W \in Y \land F \subseteq B) \to (({I ↾}_{F}) LIndF W \leftrightarrow (({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B \land \forall x \in dom ({I ↾}_{F}) \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}])))$
15	14	pm5.32da	$⊢ W \in Y \to ((F \subseteq B \land ({I ↾}_{F}) LIndF W) \leftrightarrow (F \subseteq B \land (({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B \land \forall x \in dom ({I ↾}_{F}) \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]))))$
16		dmresi	$⊢ dom ({I ↾}_{F}) = F$
17	16	raleqi	$⊢ \forall x \in dom ({I ↾}_{F}) \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]) \leftrightarrow \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}])$
18		fvresi	$⊢ x \in F \to ({I ↾}_{F}) (x) = x$
19	18	oveq2d	$⊢ x \in F \to k \underset{˙}{\cdot} ({I ↾}_{F}) (x) = k \underset{˙}{\cdot} x$
20	16	difeq1i	$⊢ dom ({I ↾}_{F}) ∖ \{x\} = F ∖ \{x\}$
21	20	imaeq2i	$⊢ ({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}] = ({I ↾}_{F}) [F ∖ \{x\}]$
22		difss	$⊢ F ∖ \{x\} \subseteq F$
23		resiima	$⊢ F ∖ \{x\} \subseteq F \to ({I ↾}_{F}) [F ∖ \{x\}] = F ∖ \{x\}$
24	22 23	ax-mp	$⊢ ({I ↾}_{F}) [F ∖ \{x\}] = F ∖ \{x\}$
25	21 24	eqtri	$⊢ ({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}] = F ∖ \{x\}$
26	25	fveq2i	$⊢ K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]) = K (F ∖ \{x\})$
27	26	a1i	$⊢ x \in F \to K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]) = K (F ∖ \{x\})$
28	19 27	eleq12d	$⊢ x \in F \to (k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]) \leftrightarrow k \underset{˙}{\cdot} x \in K (F ∖ \{x\}))$
29	28	notbid	$⊢ x \in F \to (\neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]) \leftrightarrow \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\}))$
30	29	ralbidv	$⊢ x \in F \to (\forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]) \leftrightarrow \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\}))$
31	30	ralbiia	$⊢ \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]) \leftrightarrow \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\})$
32	17 31	bitri	$⊢ \forall x \in dom ({I ↾}_{F}) \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]) \leftrightarrow \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\})$
33	32	anbi2i	$⊢ (({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B \land \forall x \in dom ({I ↾}_{F}) \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}])) \leftrightarrow (({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B \land \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\}))$
34		f1oi	$⊢ ({I ↾}_{F}) : F \underset{1-1 onto}{⟶} F$
35		f1of	$⊢ ({I ↾}_{F}) : F \underset{1-1 onto}{⟶} F \to ({I ↾}_{F}) : F ⟶ F$
36	34 35	ax-mp	$⊢ ({I ↾}_{F}) : F ⟶ F$
37	16	feq2i	$⊢ ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ F \leftrightarrow ({I ↾}_{F}) : F ⟶ F$
38	36 37	mpbir	$⊢ ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ F$
39		fss	$⊢ (({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ F \land F \subseteq B) \to ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B$
40	38 39	mpan	$⊢ F \subseteq B \to ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B$
41	40	biantrurd	$⊢ F \subseteq B \to (\forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\}) \leftrightarrow (({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B \land \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\})))$
42	33 41	bitr4id	$⊢ F \subseteq B \to ((({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B \land \forall x \in dom ({I ↾}_{F}) \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}])) \leftrightarrow \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\}))$
43	42	pm5.32i	$⊢ (F \subseteq B \land (({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B \land \forall x \in dom ({I ↾}_{F}) \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]))) \leftrightarrow (F \subseteq B \land \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\}))$
44	43	a1i	$⊢ W \in Y \to ((F \subseteq B \land (({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B \land \forall x \in dom ({I ↾}_{F}) \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} ({I ↾}_{F}) (x) \in K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]))) \leftrightarrow (F \subseteq B \land \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\})))$
45	7 15 44	3bitrd	$⊢ W \in Y \to (F \in LIndS (W) \leftrightarrow (F \subseteq B \land \forall x \in F \forall k \in (N ∖ \{\underset{˙}{0}\}) \neg k \underset{˙}{\cdot} x \in K (F ∖ \{x\})))$

Metamath Proof Explorer

Theorem islinds2

Proof