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		f1oi	$⊢ ({I ↾}_{F}) : F \underset{1-1 onto}{⟶} F$
17		f1of	$⊢ ({I ↾}_{F}) : F \underset{1-1 onto}{⟶} F \to ({I ↾}_{F}) : F ⟶ F$
18	16 17	ax-mp	$⊢ ({I ↾}_{F}) : F ⟶ F$
19		dmresi	$⊢ dom ({I ↾}_{F}) = F$
20	19	feq2i	$⊢ ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ F \leftrightarrow ({I ↾}_{F}) : F ⟶ F$
21	18 20	mpbir	$⊢ ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ F$
22		fss	$⊢ (({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ F \land F \subseteq B) \to ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B$
23	21 22	mpan	$⊢ F \subseteq B \to ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ B$
24	23	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\})))$
25	19	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\}])$
26		fvresi	$⊢ x \in F \to ({I ↾}_{F}) (x) = x$
27	26	oveq2d	$⊢ x \in F \to k \underset{˙}{\cdot} ({I ↾}_{F}) (x) = k \underset{˙}{\cdot} x$
28	19	difeq1i	$⊢ dom ({I ↾}_{F}) ∖ \{x\} = F ∖ \{x\}$
29	28	imaeq2i	$⊢ ({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}] = ({I ↾}_{F}) [F ∖ \{x\}]$
30		difss	$⊢ F ∖ \{x\} \subseteq F$
31		resiima	$⊢ F ∖ \{x\} \subseteq F \to ({I ↾}_{F}) [F ∖ \{x\}] = F ∖ \{x\}$
32	30 31	ax-mp	$⊢ ({I ↾}_{F}) [F ∖ \{x\}] = F ∖ \{x\}$
33	29 32	eqtri	$⊢ ({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}] = F ∖ \{x\}$
34	33	fveq2i	$⊢ K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]) = K (F ∖ \{x\})$
35	34	a1i	$⊢ x \in F \to K (({I ↾}_{F}) [dom ({I ↾}_{F}) ∖ \{x\}]) = K (F ∖ \{x\})$
36	27 35	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\}))$
37	36	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\}))$
38	37	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\}))$
39	38	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\})$
40	25 39	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\})$
41	40	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\}))$
42	24 41	syl6rbbr	$⊢ 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