lindfrn

Description: The range of an independent family is an independent set. (Contributed by Stefan O'Rear, 24-Feb-2015)

		Ref	Expression
	Assertion	lindfrn	$⊢ (W \in LMod \land F LIndF W) \to ran F \in LIndS (W)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{W} = {Base}_{W}$
2	1	lindff	$⊢ (F LIndF W \land W \in LMod) \to F : dom F ⟶ {Base}_{W}$
3	2	ancoms	$⊢ (W \in LMod \land F LIndF W) \to F : dom F ⟶ {Base}_{W}$
4	3	frnd	$⊢ (W \in LMod \land F LIndF W) \to ran F \subseteq {Base}_{W}$
5		simpll	$⊢ ((W \in LMod \land F LIndF W) \land y \in dom F) \to W \in LMod$
6		imassrn	$⊢ F [dom F ∖ \{y\}] \subseteq ran F$
7	6 4	sstrid	$⊢ (W \in LMod \land F LIndF W) \to F [dom F ∖ \{y\}] \subseteq {Base}_{W}$
8	7	adantr	$⊢ ((W \in LMod \land F LIndF W) \land y \in dom F) \to F [dom F ∖ \{y\}] \subseteq {Base}_{W}$
9	3	ffund	$⊢ (W \in LMod \land F LIndF W) \to Fun F$
10		eldifsn	$⊢ x \in (ran F ∖ \{F (y)\}) \leftrightarrow (x \in ran F \land x \neq F (y))$
11		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
12		fvelrnb	$⊢ F Fn dom F \to (x \in ran F \leftrightarrow \exists k \in dom F F (k) = x)$
13	11 12	sylbi	$⊢ Fun F \to (x \in ran F \leftrightarrow \exists k \in dom F F (k) = x)$
14	13	adantr	$⊢ (Fun F \land y \in dom F) \to (x \in ran F \leftrightarrow \exists k \in dom F F (k) = x)$
15		difss	$⊢ dom F ∖ \{y\} \subseteq dom F$
16	15	jctr	$⊢ Fun F \to (Fun F \land dom F ∖ \{y\} \subseteq dom F)$
17	16	ad2antrr	$⊢ ((Fun F \land y \in dom F) \land (k \in dom F \land F (k) \neq F (y))) \to (Fun F \land dom F ∖ \{y\} \subseteq dom F)$
18		simpl	$⊢ (k \in dom F \land F (k) \neq F (y)) \to k \in dom F$
19		fveq2	$⊢ k = y \to F (k) = F (y)$
20	19	necon3i	$⊢ F (k) \neq F (y) \to k \neq y$
21	20	adantl	$⊢ (k \in dom F \land F (k) \neq F (y)) \to k \neq y$
22		eldifsn	$⊢ k \in (dom F ∖ \{y\}) \leftrightarrow (k \in dom F \land k \neq y)$
23	18 21 22	sylanbrc	$⊢ (k \in dom F \land F (k) \neq F (y)) \to k \in (dom F ∖ \{y\})$
24	23	adantl	$⊢ ((Fun F \land y \in dom F) \land (k \in dom F \land F (k) \neq F (y))) \to k \in (dom F ∖ \{y\})$
25		funfvima2	$⊢ (Fun F \land dom F ∖ \{y\} \subseteq dom F) \to (k \in (dom F ∖ \{y\}) \to F (k) \in F [dom F ∖ \{y\}])$
26	17 24 25	sylc	$⊢ ((Fun F \land y \in dom F) \land (k \in dom F \land F (k) \neq F (y))) \to F (k) \in F [dom F ∖ \{y\}]$
27	26	expr	$⊢ ((Fun F \land y \in dom F) \land k \in dom F) \to (F (k) \neq F (y) \to F (k) \in F [dom F ∖ \{y\}])$
28		neeq1	$⊢ F (k) = x \to (F (k) \neq F (y) \leftrightarrow x \neq F (y))$
29		eleq1	$⊢ F (k) = x \to (F (k) \in F [dom F ∖ \{y\}] \leftrightarrow x \in F [dom F ∖ \{y\}])$
30	28 29	imbi12d	$⊢ F (k) = x \to ((F (k) \neq F (y) \to F (k) \in F [dom F ∖ \{y\}]) \leftrightarrow (x \neq F (y) \to x \in F [dom F ∖ \{y\}]))$
31	27 30	syl5ibcom	$⊢ ((Fun F \land y \in dom F) \land k \in dom F) \to (F (k) = x \to (x \neq F (y) \to x \in F [dom F ∖ \{y\}]))$
32	31	rexlimdva	$⊢ (Fun F \land y \in dom F) \to (\exists k \in dom F F (k) = x \to (x \neq F (y) \to x \in F [dom F ∖ \{y\}]))$
33	14 32	sylbid	$⊢ (Fun F \land y \in dom F) \to (x \in ran F \to (x \neq F (y) \to x \in F [dom F ∖ \{y\}]))$
34	33	impd	$⊢ (Fun F \land y \in dom F) \to ((x \in ran F \land x \neq F (y)) \to x \in F [dom F ∖ \{y\}])$
35	10 34	syl5bi	$⊢ (Fun F \land y \in dom F) \to (x \in (ran F ∖ \{F (y)\}) \to x \in F [dom F ∖ \{y\}])$
36	35	ssrdv	$⊢ (Fun F \land y \in dom F) \to ran F ∖ \{F (y)\} \subseteq F [dom F ∖ \{y\}]$
37	9 36	sylan	$⊢ ((W \in LMod \land F LIndF W) \land y \in dom F) \to ran F ∖ \{F (y)\} \subseteq F [dom F ∖ \{y\}]$
38		eqid	$⊢ LSpan (W) = LSpan (W)$
39	1 38	lspss	$⊢ (W \in LMod \land F [dom F ∖ \{y\}] \subseteq {Base}_{W} \land ran F ∖ \{F (y)\} \subseteq F [dom F ∖ \{y\}]) \to LSpan (W) (ran F ∖ \{F (y)\}) \subseteq LSpan (W) (F [dom F ∖ \{y\}])$
40	5 8 37 39	syl3anc	$⊢ ((W \in LMod \land F LIndF W) \land y \in dom F) \to LSpan (W) (ran F ∖ \{F (y)\}) \subseteq LSpan (W) (F [dom F ∖ \{y\}])$
41	40	adantrr	$⊢ ((W \in LMod \land F LIndF W) \land (y \in dom F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to LSpan (W) (ran F ∖ \{F (y)\}) \subseteq LSpan (W) (F [dom F ∖ \{y\}])$
42		simplr	$⊢ ((W \in LMod \land F LIndF W) \land (y \in dom F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to F LIndF W$
43		simprl	$⊢ ((W \in LMod \land F LIndF W) \land (y \in dom F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to y \in dom F$
44		eldifi	$⊢ k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \to k \in {Base}_{Scalar (W)}$
45	44	ad2antll	$⊢ ((W \in LMod \land F LIndF W) \land (y \in dom F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to k \in {Base}_{Scalar (W)}$
46		eldifsni	$⊢ k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \to k \neq 0_{Scalar (W)}$
47	46	ad2antll	$⊢ ((W \in LMod \land F LIndF W) \land (y \in dom F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to k \neq 0_{Scalar (W)}$
48		eqid	$⊢ \cdot_{W} = \cdot_{W}$
49		eqid	$⊢ Scalar (W) = Scalar (W)$
50		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
51		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
52	48 38 49 50 51	lindfind	$⊢ ((F LIndF W \land y \in dom F) \land (k \in {Base}_{Scalar (W)} \land k \neq 0_{Scalar (W)})) \to \neg k \cdot_{W} F (y) \in LSpan (W) (F [dom F ∖ \{y\}])$
53	42 43 45 47 52	syl22anc	$⊢ ((W \in LMod \land F LIndF W) \land (y \in dom F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \neg k \cdot_{W} F (y) \in LSpan (W) (F [dom F ∖ \{y\}])$
54	41 53	ssneldd	$⊢ ((W \in LMod \land F LIndF W) \land (y \in dom F \land k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \neg k \cdot_{W} F (y) \in LSpan (W) (ran F ∖ \{F (y)\})$
55	54	ralrimivva	$⊢ (W \in LMod \land F LIndF W) \to \forall y \in dom F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} F (y) \in LSpan (W) (ran F ∖ \{F (y)\})$
56	9	funfnd	$⊢ (W \in LMod \land F LIndF W) \to F Fn dom F$
57		oveq2	$⊢ x = F (y) \to k \cdot_{W} x = k \cdot_{W} F (y)$
58		sneq	$⊢ x = F (y) \to \{x\} = \{F (y)\}$
59	58	difeq2d	$⊢ x = F (y) \to ran F ∖ \{x\} = ran F ∖ \{F (y)\}$
60	59	fveq2d	$⊢ x = F (y) \to LSpan (W) (ran F ∖ \{x\}) = LSpan (W) (ran F ∖ \{F (y)\})$
61	57 60	eleq12d	$⊢ x = F (y) \to (k \cdot_{W} x \in LSpan (W) (ran F ∖ \{x\}) \leftrightarrow k \cdot_{W} F (y) \in LSpan (W) (ran F ∖ \{F (y)\}))$
62	61	notbid	$⊢ x = F (y) \to (\neg k \cdot_{W} x \in LSpan (W) (ran F ∖ \{x\}) \leftrightarrow \neg k \cdot_{W} F (y) \in LSpan (W) (ran F ∖ \{F (y)\}))$
63	62	ralbidv	$⊢ x = F (y) \to (\forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) (ran F ∖ \{x\}) \leftrightarrow \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} F (y) \in LSpan (W) (ran F ∖ \{F (y)\}))$
64	63	ralrn	$⊢ F Fn dom F \to (\forall x \in ran F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) (ran F ∖ \{x\}) \leftrightarrow \forall y \in dom F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} F (y) \in LSpan (W) (ran F ∖ \{F (y)\}))$
65	56 64	syl	$⊢ (W \in LMod \land F LIndF W) \to (\forall x \in ran F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) (ran F ∖ \{x\}) \leftrightarrow \forall y \in dom F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} F (y) \in LSpan (W) (ran F ∖ \{F (y)\}))$
66	55 65	mpbird	$⊢ (W \in LMod \land F LIndF W) \to \forall x \in ran F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) (ran F ∖ \{x\})$
67	1 48 38 49 51 50	islinds2	$⊢ W \in LMod \to (ran F \in LIndS (W) \leftrightarrow (ran F \subseteq {Base}_{W} \land \forall x \in ran F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) (ran F ∖ \{x\})))$
68	67	adantr	$⊢ (W \in LMod \land F LIndF W) \to (ran F \in LIndS (W) \leftrightarrow (ran F \subseteq {Base}_{W} \land \forall x \in ran F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) (ran F ∖ \{x\})))$
69	4 66 68	mpbir2and	$⊢ (W \in LMod \land F LIndF W) \to ran F \in LIndS (W)$

Metamath Proof Explorer

Theorem lindfrn

Proof