Theorem islindf

Description: Property of an independent family of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Hypotheses	islindf.b	$$⊢B={\mathrm{Base}}_W$$
	islindf.v	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	islindf.k	$$⊢K=\mathrm{LSpan}\left(W\right)$$
	islindf.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
	islindf.n	$$⊢N={\mathrm{Base}}_S$$
	islindf.z	$$⊢\underset{\dot{}}{0}=0_S$$
Assertion	islindf	$$⊢\left(W\in Y\wedge F\in X\right)\to \left(F\mathrm{LIndF}W\leftrightarrow \left(F:\mathrm{dom}F⟶B\wedge \forall x\in \mathrm{dom}F\forall k\in \left(N\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg k\underset{\dot{}}{·}F\left(x\right)\in K\left(F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islindf.b	$$⊢B={\mathrm{Base}}_W$$
2		islindf.v	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		islindf.k	$$⊢K=\mathrm{LSpan}\left(W\right)$$
4		islindf.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
5		islindf.n	$$⊢N={\mathrm{Base}}_S$$
6		islindf.z	$$⊢\underset{\dot{}}{0}=0_S$$
7		feq1	$$⊢f=F\to \left(f:\mathrm{dom}f⟶{\mathrm{Base}}_w\leftrightarrow F:\mathrm{dom}f⟶{\mathrm{Base}}_w\right)$$
8	7	adantr	$$⊢\left(f=F\wedge w=W\right)\to \left(f:\mathrm{dom}f⟶{\mathrm{Base}}_w\leftrightarrow F:\mathrm{dom}f⟶{\mathrm{Base}}_w\right)$$
9		dmeq	$$⊢f=F\to \mathrm{dom}f=\mathrm{dom}F$$
10	9	adantr	$$⊢\left(f=F\wedge w=W\right)\to \mathrm{dom}f=\mathrm{dom}F$$
11		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
12	11 1	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_w=B$$
13	12	adantl	$$⊢\left(f=F\wedge w=W\right)\to {\mathrm{Base}}_w=B$$
14	10 13	feq23d	$$⊢\left(f=F\wedge w=W\right)\to \left(F:\mathrm{dom}f⟶{\mathrm{Base}}_w\leftrightarrow F:\mathrm{dom}F⟶B\right)$$
15	8 14	bitrd	$$⊢\left(f=F\wedge w=W\right)\to \left(f:\mathrm{dom}f⟶{\mathrm{Base}}_w\leftrightarrow F:\mathrm{dom}F⟶B\right)$$
16		fvex	$$⊢\mathrm{Scalar}\left(w\right)\in \mathrm{V}$$
17		fveq2	$$⊢s=\mathrm{Scalar}\left(w\right)\to {\mathrm{Base}}_s={\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}$$
18		fveq2	$$⊢s=\mathrm{Scalar}\left(w\right)\to 0_s=0_{\mathrm{Scalar}\left(w\right)}$$
19	18	sneqd	$$⊢s=\mathrm{Scalar}\left(w\right)\to \left\{0_s\right\}=\left\{0_{\mathrm{Scalar}\left(w\right)}\right\}$$
20	17 19	difeq12d	$$⊢s=\mathrm{Scalar}\left(w\right)\to {\mathrm{Base}}_s\setminus \left\{0_s\right\}={\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\setminus \left\{0_{\mathrm{Scalar}\left(w\right)}\right\}$$
21	20	raleqdv	$$⊢s=\mathrm{Scalar}\left(w\right)\to \left(\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\leftrightarrow \forall k\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\setminus \left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\right)$$
22	21	ralbidv	$$⊢s=\mathrm{Scalar}\left(w\right)\to \left(\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\leftrightarrow \forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\setminus \left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\right)$$
23	16 22	sbcie	$$⊢\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\leftrightarrow \forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\setminus \left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)$$
24		fveq2	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=\mathrm{Scalar}\left(W\right)$$
25	24 4	eqtr4di	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=S$$
26	25	fveq2d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}={\mathrm{Base}}_S$$
27	26 5	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}=N$$
28	25	fveq2d	$$⊢w=W\to 0_{\mathrm{Scalar}\left(w\right)}=0_S$$
29	28 6	eqtr4di	$$⊢w=W\to 0_{\mathrm{Scalar}\left(w\right)}=\underset{\dot{}}{0}$$
30	29	sneqd	$$⊢w=W\to \left\{0_{\mathrm{Scalar}\left(w\right)}\right\}=\left\{\underset{\dot{}}{0}\right\}$$
31	27 30	difeq12d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\setminus \left\{0_{\mathrm{Scalar}\left(w\right)}\right\}=N\setminus \left\{\underset{\dot{}}{0}\right\}$$
32	31	adantl	$$⊢\left(f=F\wedge w=W\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\setminus \left\{0_{\mathrm{Scalar}\left(w\right)}\right\}=N\setminus \left\{\underset{\dot{}}{0}\right\}$$
33		fveq2	$$⊢w=W\to {\cdot }_w={\cdot }_W$$
34	33 2	eqtr4di	$$⊢w=W\to {\cdot }_w=\underset{\dot{}}{·}$$
35	34	adantl	$$⊢\left(f=F\wedge w=W\right)\to {\cdot }_w=\underset{\dot{}}{·}$$
36		eqidd	$$⊢\left(f=F\wedge w=W\right)\to k=k$$
37		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
38	37	adantr	$$⊢\left(f=F\wedge w=W\right)\to f\left(x\right)=F\left(x\right)$$
39	35 36 38	oveq123d	$$⊢\left(f=F\wedge w=W\right)\to k{\cdot }_{w}f\left(x\right)=k\underset{\dot{}}{·}F\left(x\right)$$
40		fveq2	$$⊢w=W\to \mathrm{LSpan}\left(w\right)=\mathrm{LSpan}\left(W\right)$$
41	40 3	eqtr4di	$$⊢w=W\to \mathrm{LSpan}\left(w\right)=K$$
42	41	adantl	$$⊢\left(f=F\wedge w=W\right)\to \mathrm{LSpan}\left(w\right)=K$$
43		imaeq1	$$⊢f=F\to f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]=F\left[\mathrm{dom}f\setminus \left\{x\right\}\right]$$
44	9	difeq1d	$$⊢f=F\to \mathrm{dom}f\setminus \left\{x\right\}=\mathrm{dom}F\setminus \left\{x\right\}$$
45	44	imaeq2d	$$⊢f=F\to F\left[\mathrm{dom}f\setminus \left\{x\right\}\right]=F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]$$
46	43 45	eqtrd	$$⊢f=F\to f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]=F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]$$
47	46	adantr	$$⊢\left(f=F\wedge w=W\right)\to f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]=F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]$$
48	42 47	fveq12d	$$⊢\left(f=F\wedge w=W\right)\to \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)=K\left(F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]\right)$$
49	39 48	eleq12d	$$⊢\left(f=F\wedge w=W\right)\to \left(k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\leftrightarrow k\underset{\dot{}}{·}F\left(x\right)\in K\left(F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]\right)\right)$$
50	49	notbid	$$⊢\left(f=F\wedge w=W\right)\to \left(\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\leftrightarrow \neg k\underset{\dot{}}{·}F\left(x\right)\in K\left(F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]\right)\right)$$
51	32 50	raleqbidv	$$⊢\left(f=F\wedge w=W\right)\to \left(\forall k\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\setminus \left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\leftrightarrow \forall k\in \left(N\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg k\underset{\dot{}}{·}F\left(x\right)\in K\left(F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]\right)\right)$$
52	10 51	raleqbidv	$$⊢\left(f=F\wedge w=W\right)\to \left(\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\setminus \left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\leftrightarrow \forall x\in \mathrm{dom}F\forall k\in \left(N\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg k\underset{\dot{}}{·}F\left(x\right)\in K\left(F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]\right)\right)$$
53	23 52	syl5bb	$$⊢\left(f=F\wedge w=W\right)\to \left(\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\leftrightarrow \forall x\in \mathrm{dom}F\forall k\in \left(N\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg k\underset{\dot{}}{·}F\left(x\right)\in K\left(F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]\right)\right)$$
54	15 53	anbi12d	$$⊢\left(f=F\wedge w=W\right)\to \left(\left(f:\mathrm{dom}f⟶{\mathrm{Base}}_w\wedge \underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\right)\leftrightarrow \left(F:\mathrm{dom}F⟶B\wedge \forall x\in \mathrm{dom}F\forall k\in \left(N\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg k\underset{\dot{}}{·}F\left(x\right)\in K\left(F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]\right)\right)\right)$$
55		df-lindf	$$⊢\mathrm{LIndF}=\left\{⟨f,w⟩|\left(f:\mathrm{dom}f⟶{\mathrm{Base}}_w\wedge \underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\right)\right\}$$
56	54 55	brabga	$$⊢\left(F\in X\wedge W\in Y\right)\to \left(F\mathrm{LIndF}W\leftrightarrow \left(F:\mathrm{dom}F⟶B\wedge \forall x\in \mathrm{dom}F\forall k\in \left(N\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg k\underset{\dot{}}{·}F\left(x\right)\in K\left(F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]\right)\right)\right)$$
57	56	ancoms	$$⊢\left(W\in Y\wedge F\in X\right)\to \left(F\mathrm{LIndF}W\leftrightarrow \left(F:\mathrm{dom}F⟶B\wedge \forall x\in \mathrm{dom}F\forall k\in \left(N\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg k\underset{\dot{}}{·}F\left(x\right)\in K\left(F\left[\mathrm{dom}F\setminus \left\{x\right\}\right]\right)\right)\right)$$