lindff1

Description: A linearly independent family over a nonzero ring has no repeated elements. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Hypotheses	lindff1.b	$⊢ B = {Base}_{W}$
	lindff1.l	$⊢ L = Scalar (W)$
Assertion	lindff1	$⊢ (W \in LMod \land L \in NzRing \land F LIndF W) \to F : dom F \underset{1-1}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		lindff1.b	$⊢ B = {Base}_{W}$
2		lindff1.l	$⊢ L = Scalar (W)$
3		simp3	$⊢ (W \in LMod \land L \in NzRing \land F LIndF W) \to F LIndF W$
4		simp1	$⊢ (W \in LMod \land L \in NzRing \land F LIndF W) \to W \in LMod$
5	1	lindff	$⊢ (F LIndF W \land W \in LMod) \to F : dom F ⟶ B$
6	3 4 5	syl2anc	$⊢ (W \in LMod \land L \in NzRing \land F LIndF W) \to F : dom F ⟶ B$
7		simpl1	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to W \in LMod$
8		imassrn	$⊢ F [dom F ∖ \{y\}] \subseteq ran F$
9	6	frnd	$⊢ (W \in LMod \land L \in NzRing \land F LIndF W) \to ran F \subseteq B$
10	8 9	sstrid	$⊢ (W \in LMod \land L \in NzRing \land F LIndF W) \to F [dom F ∖ \{y\}] \subseteq B$
11	10	adantr	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to F [dom F ∖ \{y\}] \subseteq B$
12		eqid	$⊢ LSpan (W) = LSpan (W)$
13	1 12	lspssid	$⊢ (W \in LMod \land F [dom F ∖ \{y\}] \subseteq B) \to F [dom F ∖ \{y\}] \subseteq LSpan (W) (F [dom F ∖ \{y\}])$
14	7 11 13	syl2anc	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to F [dom F ∖ \{y\}] \subseteq LSpan (W) (F [dom F ∖ \{y\}])$
15	6	ffund	$⊢ (W \in LMod \land L \in NzRing \land F LIndF W) \to Fun F$
16	15	adantr	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to Fun F$
17		simprll	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to x \in dom F$
18	16 17	jca	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to (Fun F \land x \in dom F)$
19		eldifsn	$⊢ x \in (dom F ∖ \{y\}) \leftrightarrow (x \in dom F \land x \neq y)$
20	19	biimpri	$⊢ (x \in dom F \land x \neq y) \to x \in (dom F ∖ \{y\})$
21	20	adantlr	$⊢ ((x \in dom F \land y \in dom F) \land x \neq y) \to x \in (dom F ∖ \{y\})$
22	21	adantl	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to x \in (dom F ∖ \{y\})$
23		funfvima	$⊢ (Fun F \land x \in dom F) \to (x \in (dom F ∖ \{y\}) \to F (x) \in F [dom F ∖ \{y\}])$
24	18 22 23	sylc	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to F (x) \in F [dom F ∖ \{y\}]$
25	14 24	sseldd	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to F (x) \in LSpan (W) (F [dom F ∖ \{y\}])$
26		simpl2	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to L \in NzRing$
27		simpl3	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to F LIndF W$
28		simprlr	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to y \in dom F$
29	12 2	lindfind2	$⊢ ((W \in LMod \land L \in NzRing) \land F LIndF W \land y \in dom F) \to \neg F (y) \in LSpan (W) (F [dom F ∖ \{y\}])$
30	7 26 27 28 29	syl211anc	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to \neg F (y) \in LSpan (W) (F [dom F ∖ \{y\}])$
31		nelne2	$⊢ (F (x) \in LSpan (W) (F [dom F ∖ \{y\}]) \land \neg F (y) \in LSpan (W) (F [dom F ∖ \{y\}])) \to F (x) \neq F (y)$
32	25 30 31	syl2anc	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land ((x \in dom F \land y \in dom F) \land x \neq y)) \to F (x) \neq F (y)$
33	32	expr	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land (x \in dom F \land y \in dom F)) \to (x \neq y \to F (x) \neq F (y))$
34	33	necon4d	$⊢ ((W \in LMod \land L \in NzRing \land F LIndF W) \land (x \in dom F \land y \in dom F)) \to (F (x) = F (y) \to x = y)$
35	34	ralrimivva	$⊢ (W \in LMod \land L \in NzRing \land F LIndF W) \to \forall x \in dom F \forall y \in dom F (F (x) = F (y) \to x = y)$
36		dff13	$⊢ F : dom F \underset{1-1}{⟶} B \leftrightarrow (F : dom F ⟶ B \land \forall x \in dom F \forall y \in dom F (F (x) = F (y) \to x = y))$
37	6 35 36	sylanbrc	$⊢ (W \in LMod \land L \in NzRing \land F LIndF W) \to F : dom F \underset{1-1}{⟶} B$

Metamath Proof Explorer

Theorem lindff1

Proof