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 ffvelrnd ( ( ( 𝑊 ∈ 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 𝐹 ∖ { 𝐸 } ) ) ) )