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

Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
lindff1.l ⊢ 𝐿 = ( Scalar ‘ 𝑊 )
Assertion lindff1 ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) → 𝐹 : dom 𝐹 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 lindff1.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 lindff1.l ⊢ 𝐿 = ( Scalar ‘ 𝑊 )
3 simp3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) → 𝐹 LIndF 𝑊 )
4 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) → 𝑊 ∈ LMod )
5 1 lindff ⊢ ( ( 𝐹 LIndF 𝑊 ∧ 𝑊 ∈ LMod ) → 𝐹 : dom 𝐹 ⟶ 𝐵 )
6 3 4 5 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) → 𝐹 : dom 𝐹 ⟶ 𝐵 )
7 simpl1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑊 ∈ LMod )
8 imassrn ⊢ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ⊆ ran 𝐹
9 6 frnd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) → ran 𝐹 ⊆ 𝐵 )
10 8 9 sstrid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) → ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ⊆ 𝐵 )
11 10 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ⊆ 𝐵 )
12 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
13 1 12 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ⊆ 𝐵 ) → ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
14 7 11 13 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
15 6 ffund ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) → Fun 𝐹 )
16 15 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → Fun 𝐹 )
17 simprll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ dom 𝐹 )
18 16 17 jca ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) )
19 eldifsn ⊢ ( 𝑥 ∈ ( dom 𝐹 ∖ { 𝑦 } ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ≠ 𝑦 ) )
20 19 biimpri ⊢ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ( dom 𝐹 ∖ { 𝑦 } ) )
21 20 adantlr ⊢ ( ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ( dom 𝐹 ∖ { 𝑦 } ) )
22 21 adantl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ( dom 𝐹 ∖ { 𝑦 } ) )
23 funfvima ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 ∈ ( dom 𝐹 ∖ { 𝑦 } ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
24 18 22 23 sylc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) )
25 14 24 sseldd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
26 simpl2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐿 ∈ NzRing )
27 simpl3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐹 LIndF 𝑊 )
28 simprlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ dom 𝐹 )
29 12 2 lindfind2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝑦 ∈ dom 𝐹 ) → ¬ ( 𝐹 ‘ 𝑦 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
30 7 26 27 28 29 syl211anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → ¬ ( 𝐹 ‘ 𝑦 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
31 nelne2 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) ∧ ¬ ( 𝐹 ‘ 𝑦 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) )
32 25 30 31 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) )
33 32 expr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( 𝑥 ≠ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) )
34 33 necon4d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
35 34 ralrimivva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) → ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
36 dff13 ⊢ ( 𝐹 : dom 𝐹 –1-1→ 𝐵 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
37 6 35 36 sylanbrc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ∧ 𝐹 LIndF 𝑊 ) → 𝐹 : dom 𝐹 –1-1→ 𝐵 )