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	⊢ 𝐿 = ( Scalar ‘ 𝑊 )
Assertion	islindf3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 –1-1→ V ∧ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islindf3.l	⊢ 𝐿 = ( Scalar ‘ 𝑊 )
2		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
3	2 1	lindff1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) → 𝐹 : dom 𝐹 –1-1→ ( Base ‘ 𝑊 ) )
4	3	3expa	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ) → 𝐹 : dom 𝐹 –1-1→ ( Base ‘ 𝑊 ) )
5		ssv	⊢ ( Base ‘ 𝑊 ) ⊆ V
6		f1ss	⊢ ( ( 𝐹 : dom 𝐹 –1-1→ ( Base ‘ 𝑊 ) ∧ ( Base ‘ 𝑊 ) ⊆ V ) → 𝐹 : dom 𝐹 –1-1→ V )
7	4 5 6	sylancl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ) → 𝐹 : dom 𝐹 –1-1→ V )
8		lindfrn	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) )
9	8	adantlr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ) → ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) )
10	7 9	jca	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ) → ( 𝐹 : dom 𝐹 –1-1→ V ∧ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) )
11		simpll	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ ( 𝐹 : dom 𝐹 –1-1→ V ∧ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ) → 𝑊 ∈ LMod )
12		simprr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ ( 𝐹 : dom 𝐹 –1-1→ V ∧ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ) → ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) )
13		f1f1orn	⊢ ( 𝐹 : dom 𝐹 –1-1→ V → 𝐹 : dom 𝐹 –1-1-onto→ ran 𝐹 )
14		f1of1	⊢ ( 𝐹 : dom 𝐹 –1-1-onto→ ran 𝐹 → 𝐹 : dom 𝐹 –1-1→ ran 𝐹 )
15	13 14	syl	⊢ ( 𝐹 : dom 𝐹 –1-1→ V → 𝐹 : dom 𝐹 –1-1→ ran 𝐹 )
16	15	ad2antrl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ ( 𝐹 : dom 𝐹 –1-1→ V ∧ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ) → 𝐹 : dom 𝐹 –1-1→ ran 𝐹 )
17		f1linds	⊢ ( ( 𝑊 ∈ LMod ∧ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : dom 𝐹 –1-1→ ran 𝐹 ) → 𝐹 LIndF 𝑊 )
18	11 12 16 17	syl3anc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ ( 𝐹 : dom 𝐹 –1-1→ V ∧ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ) → 𝐹 LIndF 𝑊 )
19	10 18	impbida	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 –1-1→ V ∧ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ) )