Metamath Proof Explorer

Theorem lindsind2

Description: In a linearly independent set 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 lindsind2 
|- ( ( ( W e. LMod /\ L e. NzRing ) /\ F e. ( LIndS ` W ) /\ E e. F ) -> -. E e. ( K ` ( F \ { E } ) ) )

Proof

Step Hyp Ref Expression
1 lindfind2.k 
 |-  K = ( LSpan ` W )
2 lindfind2.l 
 |-  L = ( Scalar ` W )
3 simp1 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F e. ( LIndS ` W ) /\ E e. F ) -> ( W e. LMod /\ L e. NzRing ) )
4 linds2 
 |-  ( F e. ( LIndS ` W ) -> ( _I |` F ) LIndF W )
5 4 3ad2ant2 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F e. ( LIndS ` W ) /\ E e. F ) -> ( _I |` F ) LIndF W )
6 dmresi 
 |-  dom ( _I |` F ) = F
7 6 eleq2i 
 |-  ( E e. dom ( _I |` F ) <-> E e. F )
8 7 biimpri 
 |-  ( E e. F -> E e. dom ( _I |` F ) )
9 8 3ad2ant3 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F e. ( LIndS ` W ) /\ E e. F ) -> E e. dom ( _I |` F ) )
10 1 2 lindfind2 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ ( _I |` F ) LIndF W /\ E e. dom ( _I |` F ) ) -> -. ( ( _I |` F ) ` E ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { E } ) ) ) )
11 3 5 9 10 syl3anc 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F e. ( LIndS ` W ) /\ E e. F ) -> -. ( ( _I |` F ) ` E ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { E } ) ) ) )
12 fvresi 
 |-  ( E e. F -> ( ( _I |` F ) ` E ) = E )
13 6 difeq1i 
 |-  ( dom ( _I |` F ) \ { E } ) = ( F \ { E } )
14 13 imaeq2i 
 |-  ( ( _I |` F ) " ( dom ( _I |` F ) \ { E } ) ) = ( ( _I |` F ) " ( F \ { E } ) )
15 difss 
 |-  ( F \ { E } ) C_ F
16 resiima 
 |-  ( ( F \ { E } ) C_ F -> ( ( _I |` F ) " ( F \ { E } ) ) = ( F \ { E } ) )
17 15 16 ax-mp 
 |-  ( ( _I |` F ) " ( F \ { E } ) ) = ( F \ { E } )
18 14 17 eqtri 
 |-  ( ( _I |` F ) " ( dom ( _I |` F ) \ { E } ) ) = ( F \ { E } )
19 18 fveq2i 
 |-  ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { E } ) ) ) = ( K ` ( F \ { E } ) )
20 19 a1i 
 |-  ( E e. F -> ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { E } ) ) ) = ( K ` ( F \ { E } ) ) )
21 12 20 eleq12d 
 |-  ( E e. F -> ( ( ( _I |` F ) ` E ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { E } ) ) ) <-> E e. ( K ` ( F \ { E } ) ) ) )
22 21 3ad2ant3 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F e. ( LIndS ` W ) /\ E e. F ) -> ( ( ( _I |` F ) ` E ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { E } ) ) ) <-> E e. ( K ` ( F \ { E } ) ) ) )
23 11 22 mtbid 
 |-  ( ( ( W e. LMod /\ L e. NzRing ) /\ F e. ( LIndS ` W ) /\ E e. F ) -> -. E e. ( K ` ( F \ { E } ) ) )