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→ 𝐵 )