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 
|- K = ( LSpan ` W )
lindfind2.l 
|- L = ( Scalar ` W )
Assertion lindfind2 
|- ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> -. ( F ` E ) e. ( K ` ( F " ( dom F \ { E } ) ) ) )

Proof

Step Hyp Ref Expression
1 lindfind2.k 
 |-  K = ( LSpan ` W )
2 lindfind2.l 
 |-  L = ( Scalar ` W )
3 simp1l 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> W e. LMod )
4 simp2 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> F LIndF W )
5 eqid 
 |-  ( Base ` W ) = ( Base ` W )
6 5 lindff 
 |-  ( ( F LIndF W /\ W e. LMod ) -> F : dom F --> ( Base ` W ) )
7 4 3 6 syl2anc 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> F : dom F --> ( Base ` W ) )
8 simp3 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> E e. dom F )
9 7 8 ffvelrnd 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> ( F ` E ) e. ( Base ` W ) )
10 eqid 
 |-  ( .s ` W ) = ( .s ` W )
11 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
12 5 2 10 11 lmodvs1 
 |-  ( ( W e. LMod /\ ( F ` E ) e. ( Base ` W ) ) -> ( ( 1r ` L ) ( .s ` W ) ( F ` E ) ) = ( F ` E ) )
13 3 9 12 syl2anc 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> ( ( 1r ` L ) ( .s ` W ) ( F ` E ) ) = ( F ` E ) )
14 nzrring 
 |-  ( L e. NzRing -> L e. Ring )
15 eqid 
 |-  ( Base ` L ) = ( Base ` L )
16 15 11 ringidcl 
 |-  ( L e. Ring -> ( 1r ` L ) e. ( Base ` L ) )
17 14 16 syl 
 |-  ( L e. NzRing -> ( 1r ` L ) e. ( Base ` L ) )
18 17 adantl 
 |-  ( ( W e. LMod /\ L e. NzRing ) -> ( 1r ` L ) e. ( Base ` L ) )
19 18 3ad2ant1 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> ( 1r ` L ) e. ( Base ` L ) )
20 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
21 11 20 nzrnz 
 |-  ( L e. NzRing -> ( 1r ` L ) =/= ( 0g ` L ) )
22 21 adantl 
 |-  ( ( W e. LMod /\ L e. NzRing ) -> ( 1r ` L ) =/= ( 0g ` L ) )
23 22 3ad2ant1 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> ( 1r ` L ) =/= ( 0g ` L ) )
24 10 1 2 20 15 lindfind 
 |-  ( ( ( F LIndF W /\ E e. dom F ) /\ ( ( 1r ` L ) e. ( Base ` L ) /\ ( 1r ` L ) =/= ( 0g ` L ) ) ) -> -. ( ( 1r ` L ) ( .s ` W ) ( F ` E ) ) e. ( K ` ( F " ( dom F \ { E } ) ) ) )
25 4 8 19 23 24 syl22anc 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> -. ( ( 1r ` L ) ( .s ` W ) ( F ` E ) ) e. ( K ` ( F " ( dom F \ { E } ) ) ) )
26 13 25 eqneltrrd 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F LIndF W /\ E e. dom F ) -> -. ( F ` E ) e. ( K ` ( F " ( dom F \ { E } ) ) ) )