Metamath Proof Explorer

Theorem lincresunit3

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 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 )

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 simp2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> M e. LMod )
12 11 3ad2ant1 
 |-  ( ( ( 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 ) -> M e. LMod )
13 simp1 
 |-  ( ( ( 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 ) -> ( S e. ~P B /\ M e. LMod /\ X e. S ) )
14 3simpa 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) -> ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) )
15 14 3ad2ant2 
 |-  ( ( ( 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 ) -> ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) )
16 13 15 jca 
 |-  ( ( ( 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 ) -> ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) )
17 eldifi 
 |-  ( s e. ( S \ { X } ) -> s e. S )
18 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 )
19 16 17 18 syl2an 
 |-  ( ( ( ( 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 ) /\ s e. ( S \ { X } ) ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) e. E )
20 2 fveq2i 
 |-  ( Base ` R ) = ( Base ` ( Scalar ` M ) )
21 3 20 eqtri 
 |-  E = ( Base ` ( Scalar ` M ) )
22 19 21 eleqtrdi 
 |-  ( ( ( ( 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 ) /\ s e. ( S \ { X } ) ) -> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) e. ( Base ` ( Scalar ` M ) ) )
23 22 10 fmptd 
 |-  ( ( ( 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 : ( S \ { X } ) --> ( Base ` ( Scalar ` M ) ) )
24 fvex 
 |-  ( Base ` ( Scalar ` M ) ) e. _V
25 difexg 
 |-  ( S e. ~P B -> ( S \ { X } ) e. _V )
26 25 3ad2ant1 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( S \ { X } ) e. _V )
27 26 3ad2ant1 
 |-  ( ( ( 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 ) -> ( S \ { X } ) e. _V )
28 elmapg 
 |-  ( ( ( Base ` ( Scalar ` M ) ) e. _V /\ ( S \ { X } ) e. _V ) -> ( G e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { X } ) ) <-> G : ( S \ { X } ) --> ( Base ` ( Scalar ` M ) ) ) )
29 24 27 28 sylancr 
 |-  ( ( ( 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 e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { X } ) ) <-> G : ( S \ { X } ) --> ( Base ` ( Scalar ` M ) ) ) )
30 23 29 mpbird 
 |-  ( ( ( 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 e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { X } ) ) )
31 difexg 
 |-  ( S e. ~P ( Base ` M ) -> ( S \ { X } ) e. _V )
32 31 adantl 
 |-  ( ( X e. S /\ S e. ~P ( Base ` M ) ) -> ( S \ { X } ) e. _V )
33 ssdifss 
 |-  ( S C_ ( Base ` M ) -> ( S \ { X } ) C_ ( Base ` M ) )
34 33 a1i 
 |-  ( X e. S -> ( S C_ ( Base ` M ) -> ( S \ { X } ) C_ ( Base ` M ) ) )
35 elpwi 
 |-  ( S e. ~P ( Base ` M ) -> S C_ ( Base ` M ) )
36 34 35 impel 
 |-  ( ( X e. S /\ S e. ~P ( Base ` M ) ) -> ( S \ { X } ) C_ ( Base ` M ) )
37 32 36 elpwd 
 |-  ( ( X e. S /\ S e. ~P ( Base ` M ) ) -> ( S \ { X } ) e. ~P ( Base ` M ) )
38 37 expcom 
 |-  ( S e. ~P ( Base ` M ) -> ( X e. S -> ( S \ { X } ) e. ~P ( Base ` M ) ) )
39 1 pweqi 
 |-  ~P B = ~P ( Base ` M )
40 38 39 eleq2s 
 |-  ( S e. ~P B -> ( X e. S -> ( S \ { X } ) e. ~P ( Base ` M ) ) )
41 40 imp 
 |-  ( ( S e. ~P B /\ X e. S ) -> ( S \ { X } ) e. ~P ( Base ` M ) )
42 41 3adant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( S \ { X } ) e. ~P ( Base ` M ) )
43 42 3ad2ant1 
 |-  ( ( ( 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 ) -> ( S \ { X } ) e. ~P ( Base ` M ) )
44 lincval 
 |-  ( ( M e. LMod /\ G e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { X } ) ) /\ ( S \ { X } ) e. ~P ( Base ` M ) ) -> ( G ( linC ` M ) ( S \ { X } ) ) = ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) )
45 12 30 43 44 syl3anc 
 |-  ( ( ( 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 } ) ) = ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) )
46 simp1 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> S e. ~P B )
47 simp3 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> X e. S )
48 11 46 47 3jca 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( M e. LMod /\ S e. ~P B /\ X e. S ) )
49 48 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( M e. LMod /\ S e. ~P B /\ X e. S ) )
50 3simpb 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) -> ( F e. ( E ^m S ) /\ F finSupp .0. ) )
51 50 adantl 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( F e. ( E ^m S ) /\ F finSupp .0. ) )
52 eqidd 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( F |` ( S \ { X } ) ) = ( F |` ( S \ { X } ) ) )
53 eqid 
 |-  ( .s ` M ) = ( .s ` M )
54 eqid 
 |-  ( +g ` M ) = ( +g ` M )
55 1 2 3 53 54 5 lincdifsn 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ X e. S ) /\ ( F e. ( E ^m S ) /\ F finSupp .0. ) /\ ( F |` ( S \ { X } ) ) = ( F |` ( S \ { X } ) ) ) -> ( F ( linC ` M ) S ) = ( ( ( F |` ( S \ { X } ) ) ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) )
56 49 51 52 55 syl3anc 
 |-  ( ( ( 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 ) = ( ( ( F |` ( S \ { X } ) ) ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) )
57 56 eqeq1d 
 |-  ( ( ( 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 <-> ( ( ( F |` ( S \ { X } ) ) ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = Z ) )
58 fveq2 
 |-  ( s = z -> ( G ` s ) = ( G ` z ) )
59 id 
 |-  ( s = z -> s = z )
60 58 59 oveq12d 
 |-  ( s = z -> ( ( G ` s ) ( .s ` M ) s ) = ( ( G ` z ) ( .s ` M ) z ) )
61 60 cbvmptv 
 |-  ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) = ( z e. ( S \ { X } ) |-> ( ( G ` z ) ( .s ` M ) z ) )
62 61 a1i 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) = ( z e. ( S \ { X } ) |-> ( ( G ` z ) ( .s ` M ) z ) ) )
63 62 oveq2d 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) = ( M gsum ( z e. ( S \ { X } ) |-> ( ( G ` z ) ( .s ` M ) z ) ) ) )
64 63 oveq2d 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( z e. ( S \ { X } ) |-> ( ( G ` z ) ( .s ` M ) z ) ) ) ) )
65 1 2 3 4 5 6 7 8 9 10 lincresunit3lem2 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( z e. ( S \ { X } ) |-> ( ( G ` z ) ( .s ` M ) z ) ) ) ) = ( ( F |` ( S \ { X } ) ) ( linC ` M ) ( S \ { X } ) ) )
66 64 65 eqtr2d 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( F |` ( S \ { X } ) ) ( linC ` M ) ( S \ { X } ) ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) )
67 66 oveq1d 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( ( F |` ( S \ { X } ) ) ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = ( ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) )
68 67 eqeq1d 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( ( ( F |` ( S \ { X } ) ) ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = Z <-> ( ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = Z ) )
69 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
70 69 3ad2ant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> M e. Grp )
71 70 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> M e. Grp )
72 11 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> M e. LMod )
73 elmapi 
 |-  ( F e. ( E ^m S ) -> F : S --> E )
74 73 3ad2ant1 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) -> F : S --> E )
75 ffvelrn 
 |-  ( ( F : S --> E /\ X e. S ) -> ( F ` X ) e. E )
76 74 47 75 syl2anr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( F ` X ) e. E )
77 elpwi 
 |-  ( S e. ~P B -> S C_ B )
78 77 sselda 
 |-  ( ( S e. ~P B /\ X e. S ) -> X e. B )
79 78 3adant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> X e. B )
80 79 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> X e. B )
81 1 2 53 3 lmodvscl 
 |-  ( ( M e. LMod /\ ( F ` X ) e. E /\ X e. B ) -> ( ( F ` X ) ( .s ` M ) X ) e. B )
82 72 76 80 81 syl3anc 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( F ` X ) ( .s ` M ) X ) e. B )
83 2 lmodfgrp 
 |-  ( M e. LMod -> R e. Grp )
84 83 3ad2ant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> R e. Grp )
85 3 7 grpinvcl 
 |-  ( ( R e. Grp /\ ( F ` X ) e. E ) -> ( N ` ( F ` X ) ) e. E )
86 84 76 85 syl2an2r 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( N ` ( F ` X ) ) e. E )
87 lmodcmn 
 |-  ( M e. LMod -> M e. CMnd )
88 87 3ad2ant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> M e. CMnd )
89 88 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> M e. CMnd )
90 26 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( S \ { X } ) e. _V )
91 simpll2 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ s e. ( S \ { X } ) ) -> M e. LMod )
92 1 2 3 4 5 6 7 8 9 10 lincresunit1 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) -> G e. ( E ^m ( S \ { X } ) ) )
93 92 3adantr3 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> G e. ( E ^m ( S \ { X } ) ) )
94 elmapi 
 |-  ( G e. ( E ^m ( S \ { X } ) ) -> G : ( S \ { X } ) --> E )
95 93 94 syl 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> G : ( S \ { X } ) --> E )
96 95 ffvelrnda 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ s e. ( S \ { X } ) ) -> ( G ` s ) e. E )
97 ssel2 
 |-  ( ( S C_ B /\ s e. S ) -> s e. B )
98 97 expcom 
 |-  ( s e. S -> ( S C_ B -> s e. B ) )
99 17 77 98 syl2imc 
 |-  ( S e. ~P B -> ( s e. ( S \ { X } ) -> s e. B ) )
100 99 3ad2ant1 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( s e. ( S \ { X } ) -> s e. B ) )
101 100 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( s e. ( S \ { X } ) -> s e. B ) )
102 101 imp 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ s e. ( S \ { X } ) ) -> s e. B )
103 1 2 53 3 lmodvscl 
 |-  ( ( M e. LMod /\ ( G ` s ) e. E /\ s e. B ) -> ( ( G ` s ) ( .s ` M ) s ) e. B )
104 91 96 102 103 syl3anc 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ s e. ( S \ { X } ) ) -> ( ( G ` s ) ( .s ` M ) s ) e. B )
105 104 fmpttd 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) : ( S \ { X } ) --> B )
106 25 adantr 
 |-  ( ( S e. ~P B /\ X e. S ) -> ( S \ { X } ) e. _V )
107 ssdifss 
 |-  ( S C_ B -> ( S \ { X } ) C_ B )
108 77 107 syl 
 |-  ( S e. ~P B -> ( S \ { X } ) C_ B )
109 108 adantr 
 |-  ( ( S e. ~P B /\ X e. S ) -> ( S \ { X } ) C_ B )
110 109 1 sseqtrdi 
 |-  ( ( S e. ~P B /\ X e. S ) -> ( S \ { X } ) C_ ( Base ` M ) )
111 106 110 elpwd 
 |-  ( ( S e. ~P B /\ X e. S ) -> ( S \ { X } ) e. ~P ( Base ` M ) )
112 111 3adant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( S \ { X } ) e. ~P ( Base ` M ) )
113 11 112 jca 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( M e. LMod /\ ( S \ { X } ) e. ~P ( Base ` M ) ) )
114 113 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( M e. LMod /\ ( S \ { X } ) e. ~P ( Base ` M ) ) )
115 1 2 3 4 5 6 7 8 9 10 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. )
116 115 5 breqtrdi 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> G finSupp ( 0g ` R ) )
117 2 3 scmfsupp 
 |-  ( ( ( M e. LMod /\ ( S \ { X } ) e. ~P ( Base ` M ) ) /\ G e. ( E ^m ( S \ { X } ) ) /\ G finSupp ( 0g ` R ) ) -> ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) finSupp ( 0g ` M ) )
118 114 93 116 117 syl3anc 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) finSupp ( 0g ` M ) )
119 118 6 breqtrrdi 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) finSupp Z )
120 1 6 89 90 105 119 gsumcl 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) e. B )
121 1 2 53 3 lmodvscl 
 |-  ( ( M e. LMod /\ ( N ` ( F ` X ) ) e. E /\ ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) e. B ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) e. B )
122 72 86 120 121 syl3anc 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) e. B )
123 eqid 
 |-  ( invg ` M ) = ( invg ` M )
124 1 54 6 123 grpinvid2 
 |-  ( ( M e. Grp /\ ( ( F ` X ) ( .s ` M ) X ) e. B /\ ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) e. B ) -> ( ( ( invg ` M ) ` ( ( F ` X ) ( .s ` M ) X ) ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) <-> ( ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = Z ) )
125 71 82 122 124 syl3anc 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( ( invg ` M ) ` ( ( F ` X ) ( .s ` M ) X ) ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) <-> ( ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = Z ) )
126 1 2 53 123 3 7 72 80 76 lmodvsneg 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( invg ` M ) ` ( ( F ` X ) ( .s ` M ) X ) ) = ( ( N ` ( F ` X ) ) ( .s ` M ) X ) )
127 126 eqeq1d 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( ( invg ` M ) ` ( ( F ` X ) ( .s ` M ) X ) ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) <-> ( ( N ` ( F ` X ) ) ( .s ` M ) X ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) ) )
128 simpr2 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( F ` X ) e. U )
129 1 2 3 4 7 53 lincresunit3lem3 
 |-  ( ( ( M e. LMod /\ X e. B /\ ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) e. B ) /\ ( F ` X ) e. U ) -> ( ( ( N ` ( F ` X ) ) ( .s ` M ) X ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) <-> X = ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) )
130 eqcom 
 |-  ( X = ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) <-> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) = X )
131 129 130 bitrdi 
 |-  ( ( ( M e. LMod /\ X e. B /\ ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) e. B ) /\ ( F ` X ) e. U ) -> ( ( ( N ` ( F ` X ) ) ( .s ` M ) X ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) <-> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) = X ) )
132 72 80 120 128 131 syl31anc 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( ( N ` ( F ` X ) ) ( .s ` M ) X ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) <-> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) = X ) )
133 132 biimpd 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( ( N ` ( F ` X ) ) ( .s ` M ) X ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) -> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) = X ) )
134 127 133 sylbid 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( ( invg ` M ) ` ( ( F ` X ) ( .s ` M ) X ) ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) -> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) = X ) )
135 125 134 sylbird 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = Z -> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) = X ) )
136 68 135 sylbid 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( ( ( ( F |` ( S \ { X } ) ) ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = Z -> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) = X ) )
137 57 136 sylbid 
 |-  ( ( ( 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 -> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) = X ) )
138 137 3impia 
 |-  ( ( ( 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 ) -> ( M gsum ( s e. ( S \ { X } ) |-> ( ( G ` s ) ( .s ` M ) s ) ) ) = X )
139 45 138 eqtrd 
 |-  ( ( ( 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 )