Metamath Proof Explorer

Theorem lindfind2

Description: In a linearly independent family in a module over a nonzero ring, no element is contained in the span of any non-containing set. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses lindfind2.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
lindfind2.l ⊢ 𝐿 = ( Scalar ‘ 𝑊 )
Assertion lindfind2 ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ¬ ( 𝐹 ‘ 𝐸 ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝐸 } ) ) ) )

Proof

Step Hyp Ref Expression
1 lindfind2.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
2 lindfind2.l ⊢ 𝐿 = ( Scalar ‘ 𝑊 )
3 simp1l ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → 𝑊 ∈ LMod )
4 simp2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → 𝐹 LIndF 𝑊 )
5 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6 5 lindff ⊢ ( ( 𝐹 LIndF 𝑊 ∧ 𝑊 ∈ LMod ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) )
7 4 3 6 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) )
8 simp3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → 𝐸 ∈ dom 𝐹 )
9 7 8 ffvelcdmd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐸 ) ∈ ( Base ‘ 𝑊 ) )
10 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
11 eqid ⊢ ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐿 )
12 5 2 10 11 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐹 ‘ 𝐸 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r ‘ 𝐿 ) ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝐸 ) ) = ( 𝐹 ‘ 𝐸 ) )
13 3 9 12 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ( ( 1r ‘ 𝐿 ) ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝐸 ) ) = ( 𝐹 ‘ 𝐸 ) )
14 nzrring ⊢ ( 𝐿 ∈ NzRing → 𝐿 ∈ Ring )
15 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
16 15 11 ringidcl ⊢ ( 𝐿 ∈ Ring → ( 1r ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) )
17 14 16 syl ⊢ ( 𝐿 ∈ NzRing → ( 1r ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) )
18 17 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) → ( 1r ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) )
19 18 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ( 1r ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) )
20 eqid ⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
21 11 20 nzrnz ⊢ ( 𝐿 ∈ NzRing → ( 1r ‘ 𝐿 ) ≠ ( 0g ‘ 𝐿 ) )
22 21 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) → ( 1r ‘ 𝐿 ) ≠ ( 0g ‘ 𝐿 ) )
23 22 3ad2ant1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ( 1r ‘ 𝐿 ) ≠ ( 0g ‘ 𝐿 ) )
24 10 1 2 20 15 lindfind ⊢ ( ( ( 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) ∧ ( ( 1r ‘ 𝐿 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 1r ‘ 𝐿 ) ≠ ( 0g ‘ 𝐿 ) ) ) → ¬ ( ( 1r ‘ 𝐿 ) ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝐸 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝐸 } ) ) ) )
25 4 8 19 23 24 syl22anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ¬ ( ( 1r ‘ 𝐿 ) ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝐸 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝐸 } ) ) ) )
26 13 25 eqneltrrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 LIndF 𝑊 ∧ 𝐸 ∈ dom 𝐹 ) → ¬ ( 𝐹 ‘ 𝐸 ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝐸 } ) ) ) )