Metamath Proof Explorer

Theorem islindf3

Description: In a nonzero ring, independent families can be equivalently characterized as renamings of independent sets. (Contributed by Stefan O'Rear, 26-Feb-2015)

		Ref	Expression
	Hypothesis	islindf3.l	$⊢ L = Scalar (W)$
	Assertion	islindf3	$⊢ (W \in LMod \land L \in NzRing) \to (F LIndF W \leftrightarrow (F : dom F \underset{1-1}{⟶} V \land ran F \in LIndS (W)))$

Proof

Step	Hyp	Ref	Expression
1		islindf3.l	$⊢ L = Scalar (W)$
2		eqid	$⊢ {Base}_{W} = {Base}_{W}$
3	2 1	lindff1	$⊢ (W \in LMod \land L \in NzRing \land F LIndF W) \to F : dom F \underset{1-1}{⟶} {Base}_{W}$
4	3	3expa	$⊢ ((W \in LMod \land L \in NzRing) \land F LIndF W) \to F : dom F \underset{1-1}{⟶} {Base}_{W}$
5		ssv	$⊢ {Base}_{W} \subseteq V$
6		f1ss	$⊢ (F : dom F \underset{1-1}{⟶} {Base}_{W} \land {Base}_{W} \subseteq V) \to F : dom F \underset{1-1}{⟶} V$
7	4 5 6	sylancl	$⊢ ((W \in LMod \land L \in NzRing) \land F LIndF W) \to F : dom F \underset{1-1}{⟶} V$
8		lindfrn	$⊢ (W \in LMod \land F LIndF W) \to ran F \in LIndS (W)$
9	8	adantlr	$⊢ ((W \in LMod \land L \in NzRing) \land F LIndF W) \to ran F \in LIndS (W)$
10	7 9	jca	$⊢ ((W \in LMod \land L \in NzRing) \land F LIndF W) \to (F : dom F \underset{1-1}{⟶} V \land ran F \in LIndS (W))$
11		simpll	$⊢ ((W \in LMod \land L \in NzRing) \land (F : dom F \underset{1-1}{⟶} V \land ran F \in LIndS (W))) \to W \in LMod$
12		simprr	$⊢ ((W \in LMod \land L \in NzRing) \land (F : dom F \underset{1-1}{⟶} V \land ran F \in LIndS (W))) \to ran F \in LIndS (W)$
13		f1f1orn	$⊢ F : dom F \underset{1-1}{⟶} V \to F : dom F \underset{1-1 onto}{⟶} ran F$
14		f1of1	$⊢ F : dom F \underset{1-1 onto}{⟶} ran F \to F : dom F \underset{1-1}{⟶} ran F$
15	13 14	syl	$⊢ F : dom F \underset{1-1}{⟶} V \to F : dom F \underset{1-1}{⟶} ran F$
16	15	ad2antrl	$⊢ ((W \in LMod \land L \in NzRing) \land (F : dom F \underset{1-1}{⟶} V \land ran F \in LIndS (W))) \to F : dom F \underset{1-1}{⟶} ran F$
17		f1linds	$⊢ (W \in LMod \land ran F \in LIndS (W) \land F : dom F \underset{1-1}{⟶} ran F) \to F LIndF W$
18	11 12 16 17	syl3anc	$⊢ ((W \in LMod \land L \in NzRing) \land (F : dom F \underset{1-1}{⟶} V \land ran F \in LIndS (W))) \to F LIndF W$
19	10 18	impbida	$⊢ (W \in LMod \land L \in NzRing) \to (F LIndF W \leftrightarrow (F : dom F \underset{1-1}{⟶} V \land ran F \in LIndS (W)))$