Metamath Proof Explorer

Theorem lincresunit2

Description: Property 2 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 lincresunit2 
|- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> G finSupp .0. )

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 difexg 
 |-  ( S e. ~P B -> ( S \ { X } ) e. _V )
12 11 3ad2ant1 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( S \ { X } ) e. _V )
13 12 adantl 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> ( S \ { X } ) e. _V )
14 13 adantr 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ F finSupp .0. ) -> ( S \ { X } ) e. _V )
15 mptexg 
 |-  ( ( S \ { X } ) e. _V -> ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) ) e. _V )
16 10 15 eqeltrid 
 |-  ( ( S \ { X } ) e. _V -> G e. _V )
17 14 16 syl 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ F finSupp .0. ) -> G e. _V )
18 10 funmpt2 
 |-  Fun G
19 18 a1i 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ F finSupp .0. ) -> Fun G )
20 5 fvexi 
 |-  .0. e. _V
21 20 a1i 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ F finSupp .0. ) -> .0. e. _V )
22 simpr 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ F finSupp .0. ) -> F finSupp .0. )
23 22 fsuppimpd 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ F finSupp .0. ) -> ( F supp .0. ) e. Fin )
24 simplr 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ s e. ( S \ { X } ) ) -> ( S e. ~P B /\ M e. LMod /\ X e. S ) )
25 simpll 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ s e. ( S \ { X } ) ) -> ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) )
26 eldifi 
 |-  ( s e. ( S \ { X } ) -> s e. S )
27 26 adantl 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ s e. ( S \ { X } ) ) -> s e. S )
28 1 2 3 4 5 6 7 8 9 10 lincresunitlem2 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) /\ s e. S ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) e. E )
29 24 25 27 28 syl21anc 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ s e. ( S \ { X } ) ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) e. E )
30 29 ralrimiva 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> A. s e. ( S \ { X } ) ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) e. E )
31 10 fnmpt 
 |-  ( A. s e. ( S \ { X } ) ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) e. E -> G Fn ( S \ { X } ) )
32 30 31 syl 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> G Fn ( S \ { X } ) )
33 elmapfn 
 |-  ( F e. ( E ^m S ) -> F Fn S )
34 33 adantr 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) -> F Fn S )
35 34 adantr 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> F Fn S )
36 32 35 jca 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> ( G Fn ( S \ { X } ) /\ F Fn S ) )
37 difssd 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> ( S \ { X } ) C_ S )
38 simpr1 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> S e. ~P B )
39 20 a1i 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> .0. e. _V )
40 37 38 39 3jca 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> ( ( S \ { X } ) C_ S /\ S e. ~P B /\ .0. e. _V ) )
41 fveq2 
 |-  ( s = x -> ( F ` s ) = ( F ` x ) )
42 41 oveq2d 
 |-  ( s = x -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) = ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` x ) ) )
43 simplr 
 |-  ( ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) /\ ( F ` x ) = .0. ) -> x e. ( S \ { X } ) )
44 simpllr 
 |-  ( ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) /\ ( F ` x ) = .0. ) -> ( S e. ~P B /\ M e. LMod /\ X e. S ) )
45 simpll 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) -> ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) )
46 45 adantr 
 |-  ( ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) /\ ( F ` x ) = .0. ) -> ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) )
47 eldifi 
 |-  ( x e. ( S \ { X } ) -> x e. S )
48 47 adantl 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) -> x e. S )
49 48 adantr 
 |-  ( ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) /\ ( F ` x ) = .0. ) -> x e. S )
50 1 2 3 4 5 6 7 8 9 10 lincresunitlem2 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) /\ x e. S ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` x ) ) e. E )
51 44 46 49 50 syl21anc 
 |-  ( ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) /\ ( F ` x ) = .0. ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` x ) ) e. E )
52 10 42 43 51 fvmptd3 
 |-  ( ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) /\ ( F ` x ) = .0. ) -> ( G ` x ) = ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` x ) ) )
53 oveq2 
 |-  ( ( F ` x ) = .0. -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` x ) ) = ( ( I ` ( N ` ( F ` X ) ) ) .x. .0. ) )
54 2 lmodring 
 |-  ( M e. LMod -> R e. Ring )
55 54 3ad2ant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> R e. Ring )
56 55 adantl 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> R e. Ring )
57 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 )
58 57 ancoms 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> ( I ` ( N ` ( F ` X ) ) ) e. E )
59 3 9 5 ringrz 
 |-  ( ( R e. Ring /\ ( I ` ( N ` ( F ` X ) ) ) e. E ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. .0. ) = .0. )
60 56 58 59 syl2anc 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. .0. ) = .0. )
61 60 adantr 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. .0. ) = .0. )
62 53 61 sylan9eqr 
 |-  ( ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) /\ ( F ` x ) = .0. ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` x ) ) = .0. )
63 52 62 eqtrd 
 |-  ( ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) /\ ( F ` x ) = .0. ) -> ( G ` x ) = .0. )
64 63 ex 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ x e. ( S \ { X } ) ) -> ( ( F ` x ) = .0. -> ( G ` x ) = .0. ) )
65 64 ralrimiva 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> A. x e. ( S \ { X } ) ( ( F ` x ) = .0. -> ( G ` x ) = .0. ) )
66 suppfnss 
 |-  ( ( ( G Fn ( S \ { X } ) /\ F Fn S ) /\ ( ( S \ { X } ) C_ S /\ S e. ~P B /\ .0. e. _V ) ) -> ( A. x e. ( S \ { X } ) ( ( F ` x ) = .0. -> ( G ` x ) = .0. ) -> ( G supp .0. ) C_ ( F supp .0. ) ) )
67 66 imp 
 |-  ( ( ( ( G Fn ( S \ { X } ) /\ F Fn S ) /\ ( ( S \ { X } ) C_ S /\ S e. ~P B /\ .0. e. _V ) ) /\ A. x e. ( S \ { X } ) ( ( F ` x ) = .0. -> ( G ` x ) = .0. ) ) -> ( G supp .0. ) C_ ( F supp .0. ) )
68 36 40 65 67 syl21anc 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> ( G supp .0. ) C_ ( F supp .0. ) )
69 68 adantr 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ F finSupp .0. ) -> ( G supp .0. ) C_ ( F supp .0. ) )
70 suppssfifsupp 
 |-  ( ( ( G e. _V /\ Fun G /\ .0. e. _V ) /\ ( ( F supp .0. ) e. Fin /\ ( G supp .0. ) C_ ( F supp .0. ) ) ) -> G finSupp .0. )
71 17 19 21 23 69 70 syl32anc 
 |-  ( ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) /\ F finSupp .0. ) -> G finSupp .0. )
72 71 ex 
 |-  ( ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) /\ ( S e. ~P B /\ M e. LMod /\ X e. S ) ) -> ( F finSupp .0. -> G finSupp .0. ) )
73 72 ex 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) -> ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( F finSupp .0. -> G finSupp .0. ) ) )
74 73 com23 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) -> ( F finSupp .0. -> ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> G finSupp .0. ) ) )
75 74 3impia 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) -> ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> G finSupp .0. ) )
76 75 impcom 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> G finSupp .0. )