Metamath Proof Explorer

Theorem lincresunitlem2

Description: Lemma for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-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 lincresunitlem2 
|- ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) /\ Y e. S ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` Y ) ) e. E )

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 2 lmodring 
 |-  ( M e. LMod -> R e. Ring )
12 11 3ad2ant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> R e. Ring )
13 12 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) -> R e. Ring )
14 13 adantr 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) /\ Y e. S ) -> R e. Ring )
15 1 2 3 4 5 6 7 8 9 10 lincresunitlem1 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) -> ( I ` ( N ` ( F ` X ) ) ) e. E )
16 15 adantr 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) /\ Y e. S ) -> ( I ` ( N ` ( F ` X ) ) ) e. E )
17 elmapi 
 |-  ( F e. ( E ^m S ) -> F : S --> E )
18 ffvelcdm 
 |-  ( ( F : S --> E /\ Y e. S ) -> ( F ` Y ) e. E )
19 18 ex 
 |-  ( F : S --> E -> ( Y e. S -> ( F ` Y ) e. E ) )
20 17 19 syl 
 |-  ( F e. ( E ^m S ) -> ( Y e. S -> ( F ` Y ) e. E ) )
21 20 ad2antrl 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) -> ( Y e. S -> ( F ` Y ) e. E ) )
22 21 imp 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) /\ Y e. S ) -> ( F ` Y ) e. E )
23 3 9 ringcl 
 |-  ( ( R e. Ring /\ ( I ` ( N ` ( F ` X ) ) ) e. E /\ ( F ` Y ) e. E ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` Y ) ) e. E )
24 14 16 22 23 syl3anc 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) /\ Y e. S ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` Y ) ) e. E )