This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐿 = ( 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 ‘ 𝑊 ) ) ) )