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 ∈ LMod ∧ L ∈ NzRing → F LIndF W ↔ F : dom ⁡ F ⟶ 1-1 V ∧ ran ⁡ F ∈ LIndS ⁡ W

Proof

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