Metamath Proof Explorer

Theorem lincreslvec3

Description: Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Hypotheses lincresunit.b 
|- B = ( Base ` M )
lincresunit.r 
|- R = ( Scalar ` M )
lincresunit.e 
|- E = ( Base ` R )
lincresunit.u 
|- U = ( Unit ` R )
lincresunit.0 
|- .0. = ( 0g ` R )
lincresunit.z 
|- Z = ( 0g ` M )
lincresunit.n 
|- N = ( invg ` R )
lincresunit.i 
|- I = ( invr ` R )
lincresunit.t 
|- .x. = ( .r ` R )
lincresunit.g 
|- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )
Assertion lincreslvec3 
|- ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) /\ ( F ( linC ` M ) S ) = Z ) -> ( G ( linC ` M ) ( S \ { X } ) ) = X )

Proof

Step Hyp Ref Expression
1 lincresunit.b 
 |-  B = ( Base ` M )
2 lincresunit.r 
 |-  R = ( Scalar ` M )
3 lincresunit.e 
 |-  E = ( Base ` R )
4 lincresunit.u 
 |-  U = ( Unit ` R )
5 lincresunit.0 
 |-  .0. = ( 0g ` R )
6 lincresunit.z 
 |-  Z = ( 0g ` M )
7 lincresunit.n 
 |-  N = ( invg ` R )
8 lincresunit.i 
 |-  I = ( invr ` R )
9 lincresunit.t 
 |-  .x. = ( .r ` R )
10 lincresunit.g 
 |-  G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )
11 lveclmod 
 |-  ( M e. LVec -> M e. LMod )
12 11 3anim2i 
 |-  ( ( S e. ~P B /\ M e. LVec /\ X e. S ) -> ( S e. ~P B /\ M e. LMod /\ X e. S ) )
13 12 3ad2ant1 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) /\ ( F ( linC ` M ) S ) = Z ) -> ( S e. ~P B /\ M e. LMod /\ X e. S ) )
14 simp21 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) /\ ( F ( linC ` M ) S ) = Z ) -> F e. ( E ^m S ) )
15 elmapi 
 |-  ( F e. ( E ^m S ) -> F : S --> E )
16 15 3ad2ant1 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) -> F : S --> E )
17 simp3 
 |-  ( ( S e. ~P B /\ M e. LVec /\ X e. S ) -> X e. S )
18 ffvelcdm 
 |-  ( ( F : S --> E /\ X e. S ) -> ( F ` X ) e. E )
19 16 17 18 syl2anr 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) ) -> ( F ` X ) e. E )
20 simpr2 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) ) -> ( F ` X ) =/= .0. )
21 2 lvecdrng 
 |-  ( M e. LVec -> R e. DivRing )
22 21 3ad2ant2 
 |-  ( ( S e. ~P B /\ M e. LVec /\ X e. S ) -> R e. DivRing )
23 22 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) ) -> R e. DivRing )
24 3 4 5 drngunit 
 |-  ( R e. DivRing -> ( ( F ` X ) e. U <-> ( ( F ` X ) e. E /\ ( F ` X ) =/= .0. ) ) )
25 23 24 syl 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) ) -> ( ( F ` X ) e. U <-> ( ( F ` X ) e. E /\ ( F ` X ) =/= .0. ) ) )
26 19 20 25 mpbir2and 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) ) -> ( F ` X ) e. U )
27 26 3adant3 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) /\ ( F ( linC ` M ) S ) = Z ) -> ( F ` X ) e. U )
28 simp3 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) -> F finSupp .0. )
29 28 3ad2ant2 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) /\ ( F ( linC ` M ) S ) = Z ) -> F finSupp .0. )
30 simp3 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) /\ ( F ( linC ` M ) S ) = Z ) -> ( F ( linC ` M ) S ) = Z )
31 1 2 3 4 5 6 7 8 9 10 lincresunit3 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) /\ ( F ( linC ` M ) S ) = Z ) -> ( G ( linC ` M ) ( S \ { X } ) ) = X )
32 13 14 27 29 30 31 syl131anc 
 |-  ( ( ( S e. ~P B /\ M e. LVec /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) =/= .0. /\ F finSupp .0. ) /\ ( F ( linC ` M ) S ) = Z ) -> ( G ( linC ` M ) ( S \ { X } ) ) = X )