Metamath Proof Explorer

Theorem lincresunit3lem2

Description: Lemma 2 for lincresunit3 . (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 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 } ) ) )

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 simpl2 
 |-  ( ( ( 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 )
12 2 fveq2i 
 |-  ( Base ` R ) = ( Base ` ( Scalar ` M ) )
13 3 12 eqtri 
 |-  E = ( Base ` ( Scalar ` M ) )
14 13 oveq1i 
 |-  ( E ^m S ) = ( ( Base ` ( Scalar ` M ) ) ^m S )
15 14 eleq2i 
 |-  ( F e. ( E ^m S ) <-> F e. ( ( Base ` ( Scalar ` M ) ) ^m S ) )
16 15 biimpi 
 |-  ( F e. ( E ^m S ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m S ) )
17 16 3ad2ant1 
 |-  ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m S ) )
18 17 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. ( ( Base ` ( Scalar ` M ) ) ^m S ) )
19 difssd 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( S \ { X } ) C_ S )
20 elmapssres 
 |-  ( ( F e. ( ( Base ` ( Scalar ` M ) ) ^m S ) /\ ( S \ { X } ) C_ S ) -> ( F |` ( S \ { X } ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { X } ) ) )
21 18 19 20 syl2anc 
 |-  ( ( ( 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 } ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { X } ) ) )
22 elpwi 
 |-  ( S e. ~P ( Base ` M ) -> S C_ ( Base ` M ) )
23 22 ssdifssd 
 |-  ( S e. ~P ( Base ` M ) -> ( S \ { X } ) C_ ( Base ` M ) )
24 difexg 
 |-  ( S e. ~P ( Base ` M ) -> ( S \ { X } ) e. _V )
25 elpwg 
 |-  ( ( S \ { X } ) e. _V -> ( ( S \ { X } ) e. ~P ( Base ` M ) <-> ( S \ { X } ) C_ ( Base ` M ) ) )
26 24 25 syl 
 |-  ( S e. ~P ( Base ` M ) -> ( ( S \ { X } ) e. ~P ( Base ` M ) <-> ( S \ { X } ) C_ ( Base ` M ) ) )
27 23 26 mpbird 
 |-  ( S e. ~P ( Base ` M ) -> ( S \ { X } ) e. ~P ( Base ` M ) )
28 1 pweqi 
 |-  ~P B = ~P ( Base ` M )
29 27 28 eleq2s 
 |-  ( S e. ~P B -> ( S \ { X } ) e. ~P ( Base ` M ) )
30 29 3ad2ant1 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( S \ { X } ) e. ~P ( Base ` M ) )
31 30 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. ~P ( Base ` M ) )
32 lincval 
 |-  ( ( M e. LMod /\ ( F |` ( S \ { X } ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { X } ) ) /\ ( S \ { X } ) e. ~P ( Base ` M ) ) -> ( ( F |` ( S \ { X } ) ) ( linC ` M ) ( S \ { X } ) ) = ( M gsum ( z e. ( S \ { X } ) |-> ( ( ( F |` ( S \ { X } ) ) ` z ) ( .s ` M ) z ) ) ) )
33 11 21 31 32 syl3anc 
 |-  ( ( ( 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 } ) ) = ( M gsum ( z e. ( S \ { X } ) |-> ( ( ( F |` ( S \ { X } ) ) ` z ) ( .s ` M ) z ) ) ) )
34 simpll 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> ( S e. ~P B /\ M e. LMod /\ X e. S ) )
35 simplr1 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> F e. ( E ^m S ) )
36 simplr2 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> ( F ` X ) e. U )
37 simpr 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> z e. ( S \ { X } ) )
38 1 2 3 4 5 6 7 8 9 10 lincresunit3lem1 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ z e. ( S \ { X } ) ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( G ` z ) ( .s ` M ) z ) ) = ( ( F ` z ) ( .s ` M ) z ) )
39 34 35 36 37 38 syl13anc 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( G ` z ) ( .s ` M ) z ) ) = ( ( F ` z ) ( .s ` M ) z ) )
40 fvres 
 |-  ( z e. ( S \ { X } ) -> ( ( F |` ( S \ { X } ) ) ` z ) = ( F ` z ) )
41 40 adantl 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> ( ( F |` ( S \ { X } ) ) ` z ) = ( F ` z ) )
42 41 eqcomd 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> ( F ` z ) = ( ( F |` ( S \ { X } ) ) ` z ) )
43 42 oveq1d 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> ( ( F ` z ) ( .s ` M ) z ) = ( ( ( F |` ( S \ { X } ) ) ` z ) ( .s ` M ) z ) )
44 39 43 eqtrd 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( G ` z ) ( .s ` M ) z ) ) = ( ( ( F |` ( S \ { X } ) ) ` z ) ( .s ` M ) z ) )
45 44 mpteq2dva 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( z e. ( S \ { X } ) |-> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( G ` z ) ( .s ` M ) z ) ) ) = ( z e. ( S \ { X } ) |-> ( ( ( F |` ( S \ { X } ) ) ` z ) ( .s ` M ) z ) ) )
46 45 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 ( z e. ( S \ { X } ) |-> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( G ` z ) ( .s ` M ) z ) ) ) ) = ( M gsum ( z e. ( S \ { X } ) |-> ( ( ( F |` ( S \ { X } ) ) ` z ) ( .s ` M ) z ) ) ) )
47 eqid 
 |-  ( +g ` M ) = ( +g ` M )
48 eqid 
 |-  ( .s ` M ) = ( .s ` M )
49 difexg 
 |-  ( S e. ~P B -> ( S \ { X } ) e. _V )
50 49 3ad2ant1 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( S \ { X } ) e. _V )
51 50 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 )
52 2 lmodfgrp 
 |-  ( M e. LMod -> R e. Grp )
53 52 3ad2ant2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> R e. Grp )
54 53 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ F e. ( E ^m S ) ) -> R e. Grp )
55 elmapi 
 |-  ( F e. ( E ^m S ) -> F : S --> E )
56 ffvelcdm 
 |-  ( ( F : S --> E /\ X e. S ) -> ( F ` X ) e. E )
57 56 expcom 
 |-  ( X e. S -> ( F : S --> E -> ( F ` X ) e. E ) )
58 57 3ad2ant3 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( F : S --> E -> ( F ` X ) e. E ) )
59 55 58 syl5com 
 |-  ( F e. ( E ^m S ) -> ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( F ` X ) e. E ) )
60 59 impcom 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ F e. ( E ^m S ) ) -> ( F ` X ) e. E )
61 3 7 grpinvcl 
 |-  ( ( R e. Grp /\ ( F ` X ) e. E ) -> ( N ` ( F ` X ) ) e. E )
62 54 60 61 syl2anc 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ F e. ( E ^m S ) ) -> ( N ` ( F ` X ) ) e. E )
63 62 3ad2antr1 
 |-  ( ( ( 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 )
64 11 adantr 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> M e. LMod )
65 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 } ) ) )
66 65 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 } ) ) )
67 elmapi 
 |-  ( G e. ( E ^m ( S \ { X } ) ) -> G : ( S \ { X } ) --> E )
68 ffvelcdm 
 |-  ( ( G : ( S \ { X } ) --> E /\ z e. ( S \ { X } ) ) -> ( G ` z ) e. E )
69 68 ex 
 |-  ( G : ( S \ { X } ) --> E -> ( z e. ( S \ { X } ) -> ( G ` z ) e. E ) )
70 66 67 69 3syl 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( z e. ( S \ { X } ) -> ( G ` z ) e. E ) )
71 70 imp 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> ( G ` z ) e. E )
72 elpwi 
 |-  ( S e. ~P B -> S C_ B )
73 eldifi 
 |-  ( z e. ( S \ { X } ) -> z e. S )
74 ssel2 
 |-  ( ( S C_ B /\ z e. S ) -> z e. B )
75 74 expcom 
 |-  ( z e. S -> ( S C_ B -> z e. B ) )
76 73 75 syl 
 |-  ( z e. ( S \ { X } ) -> ( S C_ B -> z e. B ) )
77 72 76 syl5com 
 |-  ( S e. ~P B -> ( z e. ( S \ { X } ) -> z e. B ) )
78 77 3ad2ant1 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( z e. ( S \ { X } ) -> z e. B ) )
79 78 adantr 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( z e. ( S \ { X } ) -> z e. B ) )
80 79 imp 
 |-  ( ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) /\ z e. ( S \ { X } ) ) -> z e. B )
81 1 2 48 3 lmodvscl 
 |-  ( ( M e. LMod /\ ( G ` z ) e. E /\ z e. B ) -> ( ( G ` z ) ( .s ` M ) z ) e. B )
82 64 71 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. ) ) /\ z e. ( S \ { X } ) ) -> ( ( G ` z ) ( .s ` M ) z ) e. B )
83 simp2 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> M e. LMod )
84 83 30 jca 
 |-  ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> ( M e. LMod /\ ( S \ { X } ) e. ~P ( Base ` M ) ) )
85 84 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 ) ) )
86 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. )
87 86 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 ) )
88 2 3 scmfsupp 
 |-  ( ( ( M e. LMod /\ ( S \ { X } ) e. ~P ( Base ` M ) ) /\ G e. ( E ^m ( S \ { X } ) ) /\ G finSupp ( 0g ` R ) ) -> ( z e. ( S \ { X } ) |-> ( ( G ` z ) ( .s ` M ) z ) ) finSupp ( 0g ` M ) )
89 88 6 breqtrrdi 
 |-  ( ( ( M e. LMod /\ ( S \ { X } ) e. ~P ( Base ` M ) ) /\ G e. ( E ^m ( S \ { X } ) ) /\ G finSupp ( 0g ` R ) ) -> ( z e. ( S \ { X } ) |-> ( ( G ` z ) ( .s ` M ) z ) ) finSupp Z )
90 85 66 87 89 syl3anc 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( z e. ( S \ { X } ) |-> ( ( G ` z ) ( .s ` M ) z ) ) finSupp Z )
91 1 2 3 6 47 48 11 51 63 82 90 gsumvsmul 
 |-  ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U /\ F finSupp .0. ) ) -> ( M gsum ( z e. ( S \ { X } ) |-> ( ( N ` ( F ` X ) ) ( .s ` M ) ( ( G ` z ) ( .s ` M ) z ) ) ) ) = ( ( N ` ( F ` X ) ) ( .s ` M ) ( M gsum ( z e. ( S \ { X } ) |-> ( ( G ` z ) ( .s ` M ) z ) ) ) ) )
92 33 46 91 3eqtr2rd 
 |-  ( ( ( 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 } ) ) )