This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frlmsslsp

Description: A subset of a free module obtained by restricting the support set is spanned by the relevant unit vectors. (Contributed by Stefan O'Rear, 6-Feb-2015) (Revised by AV, 24-Jun-2019)

Ref Expression
Hypotheses frlmsslsp.y 
|- Y = ( R freeLMod I )
frlmsslsp.u 
|- U = ( R unitVec I )
frlmsslsp.k 
|- K = ( LSpan ` Y )
frlmsslsp.b 
|- B = ( Base ` Y )
frlmsslsp.z 
|- .0. = ( 0g ` R )
frlmsslsp.c 
|- C = { x e. B | ( x supp .0. ) C_ J }
Assertion frlmsslsp 
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( K ` ( U " J ) ) = C )

Proof

Step Hyp Ref Expression
1 frlmsslsp.y 
 |-  Y = ( R freeLMod I )
2 frlmsslsp.u 
 |-  U = ( R unitVec I )
3 frlmsslsp.k 
 |-  K = ( LSpan ` Y )
4 frlmsslsp.b 
 |-  B = ( Base ` Y )
5 frlmsslsp.z 
 |-  .0. = ( 0g ` R )
6 frlmsslsp.c 
 |-  C = { x e. B | ( x supp .0. ) C_ J }
7 1 frlmlmod 
 |-  ( ( R e. Ring /\ I e. V ) -> Y e. LMod )
8 7 3adant3 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> Y e. LMod )
9 eqid 
 |-  ( LSubSp ` Y ) = ( LSubSp ` Y )
10 1 9 4 5 6 frlmsslss2 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> C e. ( LSubSp ` Y ) )
11 2 1 4 uvcff 
 |-  ( ( R e. Ring /\ I e. V ) -> U : I --> B )
12 11 3adant3 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> U : I --> B )
13 12 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) -> U : I --> B )
14 simp3 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> J C_ I )
15 14 sselda 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) -> y e. I )
16 13 15 ffvelcdmd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) -> ( U ` y ) e. B )
17 simpl2 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) -> I e. V )
18 eqid 
 |-  ( Base ` R ) = ( Base ` R )
19 1 18 4 frlmbasf 
 |-  ( ( I e. V /\ ( U ` y ) e. B ) -> ( U ` y ) : I --> ( Base ` R ) )
20 17 16 19 syl2anc 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) -> ( U ` y ) : I --> ( Base ` R ) )
21 simpll1 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) /\ x e. ( I \ J ) ) -> R e. Ring )
22 simpll2 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) /\ x e. ( I \ J ) ) -> I e. V )
23 15 adantr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) /\ x e. ( I \ J ) ) -> y e. I )
24 eldifi 
 |-  ( x e. ( I \ J ) -> x e. I )
25 24 adantl 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) /\ x e. ( I \ J ) ) -> x e. I )
26 elneeldif 
 |-  ( ( y e. J /\ x e. ( I \ J ) ) -> y =/= x )
27 26 adantll 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) /\ x e. ( I \ J ) ) -> y =/= x )
28 2 21 22 23 25 27 5 uvcvv0 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) /\ x e. ( I \ J ) ) -> ( ( U ` y ) ` x ) = .0. )
29 20 28 suppss 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) -> ( ( U ` y ) supp .0. ) C_ J )
30 oveq1 
 |-  ( x = ( U ` y ) -> ( x supp .0. ) = ( ( U ` y ) supp .0. ) )
31 30 sseq1d 
 |-  ( x = ( U ` y ) -> ( ( x supp .0. ) C_ J <-> ( ( U ` y ) supp .0. ) C_ J ) )
32 31 6 elrab2 
 |-  ( ( U ` y ) e. C <-> ( ( U ` y ) e. B /\ ( ( U ` y ) supp .0. ) C_ J ) )
33 16 29 32 sylanbrc 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. J ) -> ( U ` y ) e. C )
34 33 ralrimiva 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> A. y e. J ( U ` y ) e. C )
35 12 ffund 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> Fun U )
36 12 fdmd 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> dom U = I )
37 14 36 sseqtrrd 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> J C_ dom U )
38 funimass4 
 |-  ( ( Fun U /\ J C_ dom U ) -> ( ( U " J ) C_ C <-> A. y e. J ( U ` y ) e. C ) )
39 35 37 38 syl2anc 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( ( U " J ) C_ C <-> A. y e. J ( U ` y ) e. C ) )
40 34 39 mpbird 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( U " J ) C_ C )
41 9 3 lspssp 
 |-  ( ( Y e. LMod /\ C e. ( LSubSp ` Y ) /\ ( U " J ) C_ C ) -> ( K ` ( U " J ) ) C_ C )
42 8 10 40 41 syl3anc 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( K ` ( U " J ) ) C_ C )
43 simpl1 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> R e. Ring )
44 simpl2 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> I e. V )
45 6 ssrab3 
 |-  C C_ B
46 45 a1i 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> C C_ B )
47 46 sselda 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> y e. B )
48 eqid 
 |-  ( .s ` Y ) = ( .s ` Y )
49 2 1 4 48 uvcresum 
 |-  ( ( R e. Ring /\ I e. V /\ y e. B ) -> y = ( Y gsum ( y oF ( .s ` Y ) U ) ) )
50 43 44 47 49 syl3anc 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> y = ( Y gsum ( y oF ( .s ` Y ) U ) ) )
51 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
52 lmodabl 
 |-  ( Y e. LMod -> Y e. Abel )
53 8 52 syl 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> Y e. Abel )
54 53 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> Y e. Abel )
55 imassrn 
 |-  ( U " J ) C_ ran U
56 12 frnd 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ran U C_ B )
57 55 56 sstrid 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( U " J ) C_ B )
58 4 9 3 lspcl 
 |-  ( ( Y e. LMod /\ ( U " J ) C_ B ) -> ( K ` ( U " J ) ) e. ( LSubSp ` Y ) )
59 8 57 58 syl2anc 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( K ` ( U " J ) ) e. ( LSubSp ` Y ) )
60 9 lsssubg 
 |-  ( ( Y e. LMod /\ ( K ` ( U " J ) ) e. ( LSubSp ` Y ) ) -> ( K ` ( U " J ) ) e. ( SubGrp ` Y ) )
61 8 59 60 syl2anc 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( K ` ( U " J ) ) e. ( SubGrp ` Y ) )
62 61 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( K ` ( U " J ) ) e. ( SubGrp ` Y ) )
63 1 18 4 frlmbasf 
 |-  ( ( I e. V /\ y e. B ) -> y : I --> ( Base ` R ) )
64 63 3ad2antl2 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) -> y : I --> ( Base ` R ) )
65 64 ffnd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) -> y Fn I )
66 12 ffnd 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> U Fn I )
67 66 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) -> U Fn I )
68 simpl2 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) -> I e. V )
69 inidm 
 |-  ( I i^i I ) = I
70 65 67 68 68 69 offn 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) -> ( y oF ( .s ` Y ) U ) Fn I )
71 47 70 syldan 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( y oF ( .s ` Y ) U ) Fn I )
72 47 65 syldan 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> y Fn I )
73 72 adantrr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) -> y Fn I )
74 66 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) -> U Fn I )
75 simpl2 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) -> I e. V )
76 simprr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) -> z e. I )
77 fnfvof 
 |-  ( ( ( y Fn I /\ U Fn I ) /\ ( I e. V /\ z e. I ) ) -> ( ( y oF ( .s ` Y ) U ) ` z ) = ( ( y ` z ) ( .s ` Y ) ( U ` z ) ) )
78 73 74 75 76 77 syl22anc 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) -> ( ( y oF ( .s ` Y ) U ) ` z ) = ( ( y ` z ) ( .s ` Y ) ( U ` z ) ) )
79 8 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> Y e. LMod )
80 59 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> ( K ` ( U " J ) ) e. ( LSubSp ` Y ) )
81 45 sseli 
 |-  ( y e. C -> y e. B )
82 81 64 sylan2 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> y : I --> ( Base ` R ) )
83 82 adantrr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> y : I --> ( Base ` R ) )
84 14 sselda 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ z e. J ) -> z e. I )
85 84 adantrl 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> z e. I )
86 83 85 ffvelcdmd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> ( y ` z ) e. ( Base ` R ) )
87 1 frlmsca 
 |-  ( ( R e. Ring /\ I e. V ) -> R = ( Scalar ` Y ) )
88 87 3adant3 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> R = ( Scalar ` Y ) )
89 88 fveq2d 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( Base ` R ) = ( Base ` ( Scalar ` Y ) ) )
90 89 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` Y ) ) )
91 86 90 eleqtrd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> ( y ` z ) e. ( Base ` ( Scalar ` Y ) ) )
92 4 3 lspssid 
 |-  ( ( Y e. LMod /\ ( U " J ) C_ B ) -> ( U " J ) C_ ( K ` ( U " J ) ) )
93 8 57 92 syl2anc 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( U " J ) C_ ( K ` ( U " J ) ) )
94 93 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> ( U " J ) C_ ( K ` ( U " J ) ) )
95 funfvima2 
 |-  ( ( Fun U /\ J C_ dom U ) -> ( z e. J -> ( U ` z ) e. ( U " J ) ) )
96 35 37 95 syl2anc 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( z e. J -> ( U ` z ) e. ( U " J ) ) )
97 96 imp 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ z e. J ) -> ( U ` z ) e. ( U " J ) )
98 97 adantrl 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> ( U ` z ) e. ( U " J ) )
99 94 98 sseldd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> ( U ` z ) e. ( K ` ( U " J ) ) )
100 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
101 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
102 100 48 101 9 lssvscl 
 |-  ( ( ( Y e. LMod /\ ( K ` ( U " J ) ) e. ( LSubSp ` Y ) ) /\ ( ( y ` z ) e. ( Base ` ( Scalar ` Y ) ) /\ ( U ` z ) e. ( K ` ( U " J ) ) ) ) -> ( ( y ` z ) ( .s ` Y ) ( U ` z ) ) e. ( K ` ( U " J ) ) )
103 79 80 91 99 102 syl22anc 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. J ) ) -> ( ( y ` z ) ( .s ` Y ) ( U ` z ) ) e. ( K ` ( U " J ) ) )
104 103 anassrs 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) /\ z e. J ) -> ( ( y ` z ) ( .s ` Y ) ( U ` z ) ) e. ( K ` ( U " J ) ) )
105 104 adantlrr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ z e. J ) -> ( ( y ` z ) ( .s ` Y ) ( U ` z ) ) e. ( K ` ( U " J ) ) )
106 id 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) )
107 106 adantrr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) -> ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) )
108 107 adantr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) )
109 simplrr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> z e. I )
110 simpr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> -. z e. J )
111 109 110 eldifd 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> z e. ( I \ J ) )
112 oveq1 
 |-  ( x = y -> ( x supp .0. ) = ( y supp .0. ) )
113 112 sseq1d 
 |-  ( x = y -> ( ( x supp .0. ) C_ J <-> ( y supp .0. ) C_ J ) )
114 113 6 elrab2 
 |-  ( y e. C <-> ( y e. B /\ ( y supp .0. ) C_ J ) )
115 114 simprbi 
 |-  ( y e. C -> ( y supp .0. ) C_ J )
116 115 adantl 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( y supp .0. ) C_ J )
117 5 fvexi 
 |-  .0. e. _V
118 117 a1i 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> .0. e. _V )
119 82 116 44 118 suppssr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) /\ z e. ( I \ J ) ) -> ( y ` z ) = .0. )
120 108 111 119 syl2anc 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> ( y ` z ) = .0. )
121 88 fveq2d 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` Y ) ) )
122 5 121 eqtrid 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> .0. = ( 0g ` ( Scalar ` Y ) ) )
123 122 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> .0. = ( 0g ` ( Scalar ` Y ) ) )
124 120 123 eqtrd 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> ( y ` z ) = ( 0g ` ( Scalar ` Y ) ) )
125 124 oveq1d 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> ( ( y ` z ) ( .s ` Y ) ( U ` z ) ) = ( ( 0g ` ( Scalar ` Y ) ) ( .s ` Y ) ( U ` z ) ) )
126 8 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> Y e. LMod )
127 12 ffvelcdmda 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ z e. I ) -> ( U ` z ) e. B )
128 127 adantrl 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) -> ( U ` z ) e. B )
129 128 adantr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> ( U ` z ) e. B )
130 eqid 
 |-  ( 0g ` ( Scalar ` Y ) ) = ( 0g ` ( Scalar ` Y ) )
131 4 100 48 130 51 lmod0vs 
 |-  ( ( Y e. LMod /\ ( U ` z ) e. B ) -> ( ( 0g ` ( Scalar ` Y ) ) ( .s ` Y ) ( U ` z ) ) = ( 0g ` Y ) )
132 126 129 131 syl2anc 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> ( ( 0g ` ( Scalar ` Y ) ) ( .s ` Y ) ( U ` z ) ) = ( 0g ` Y ) )
133 125 132 eqtrd 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> ( ( y ` z ) ( .s ` Y ) ( U ` z ) ) = ( 0g ` Y ) )
134 59 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> ( K ` ( U " J ) ) e. ( LSubSp ` Y ) )
135 51 9 lss0cl 
 |-  ( ( Y e. LMod /\ ( K ` ( U " J ) ) e. ( LSubSp ` Y ) ) -> ( 0g ` Y ) e. ( K ` ( U " J ) ) )
136 126 134 135 syl2anc 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> ( 0g ` Y ) e. ( K ` ( U " J ) ) )
137 133 136 eqeltrd 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) /\ -. z e. J ) -> ( ( y ` z ) ( .s ` Y ) ( U ` z ) ) e. ( K ` ( U " J ) ) )
138 105 137 pm2.61dan 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) -> ( ( y ` z ) ( .s ` Y ) ( U ` z ) ) e. ( K ` ( U " J ) ) )
139 78 138 eqeltrd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ ( y e. C /\ z e. I ) ) -> ( ( y oF ( .s ` Y ) U ) ` z ) e. ( K ` ( U " J ) ) )
140 139 expr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( z e. I -> ( ( y oF ( .s ` Y ) U ) ` z ) e. ( K ` ( U " J ) ) ) )
141 140 ralrimiv 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> A. z e. I ( ( y oF ( .s ` Y ) U ) ` z ) e. ( K ` ( U " J ) ) )
142 ffnfv 
 |-  ( ( y oF ( .s ` Y ) U ) : I --> ( K ` ( U " J ) ) <-> ( ( y oF ( .s ` Y ) U ) Fn I /\ A. z e. I ( ( y oF ( .s ` Y ) U ) ` z ) e. ( K ` ( U " J ) ) ) )
143 71 141 142 sylanbrc 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( y oF ( .s ` Y ) U ) : I --> ( K ` ( U " J ) ) )
144 1 5 4 frlmbasfsupp 
 |-  ( ( I e. V /\ y e. B ) -> y finSupp .0. )
145 144 fsuppimpd 
 |-  ( ( I e. V /\ y e. B ) -> ( y supp .0. ) e. Fin )
146 44 47 145 syl2anc 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( y supp .0. ) e. Fin )
147 dffn2 
 |-  ( ( y oF ( .s ` Y ) U ) Fn I <-> ( y oF ( .s ` Y ) U ) : I --> _V )
148 70 147 sylib 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) -> ( y oF ( .s ` Y ) U ) : I --> _V )
149 65 adantr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> y Fn I )
150 66 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> U Fn I )
151 simpll2 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> I e. V )
152 eldifi 
 |-  ( x e. ( I \ ( y supp .0. ) ) -> x e. I )
153 152 adantl 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> x e. I )
154 fnfvof 
 |-  ( ( ( y Fn I /\ U Fn I ) /\ ( I e. V /\ x e. I ) ) -> ( ( y oF ( .s ` Y ) U ) ` x ) = ( ( y ` x ) ( .s ` Y ) ( U ` x ) ) )
155 149 150 151 153 154 syl22anc 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> ( ( y oF ( .s ` Y ) U ) ` x ) = ( ( y ` x ) ( .s ` Y ) ( U ` x ) ) )
156 ssidd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) -> ( y supp .0. ) C_ ( y supp .0. ) )
157 117 a1i 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) -> .0. e. _V )
158 64 156 68 157 suppssr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> ( y ` x ) = .0. )
159 122 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> .0. = ( 0g ` ( Scalar ` Y ) ) )
160 158 159 eqtrd 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> ( y ` x ) = ( 0g ` ( Scalar ` Y ) ) )
161 160 oveq1d 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> ( ( y ` x ) ( .s ` Y ) ( U ` x ) ) = ( ( 0g ` ( Scalar ` Y ) ) ( .s ` Y ) ( U ` x ) ) )
162 8 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> Y e. LMod )
163 12 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) -> U : I --> B )
164 ffvelcdm 
 |-  ( ( U : I --> B /\ x e. I ) -> ( U ` x ) e. B )
165 163 152 164 syl2an 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> ( U ` x ) e. B )
166 4 100 48 130 51 lmod0vs 
 |-  ( ( Y e. LMod /\ ( U ` x ) e. B ) -> ( ( 0g ` ( Scalar ` Y ) ) ( .s ` Y ) ( U ` x ) ) = ( 0g ` Y ) )
167 162 165 166 syl2anc 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> ( ( 0g ` ( Scalar ` Y ) ) ( .s ` Y ) ( U ` x ) ) = ( 0g ` Y ) )
168 155 161 167 3eqtrd 
 |-  ( ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) /\ x e. ( I \ ( y supp .0. ) ) ) -> ( ( y oF ( .s ` Y ) U ) ` x ) = ( 0g ` Y ) )
169 148 168 suppss 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. B ) -> ( ( y oF ( .s ` Y ) U ) supp ( 0g ` Y ) ) C_ ( y supp .0. ) )
170 47 169 syldan 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( ( y oF ( .s ` Y ) U ) supp ( 0g ` Y ) ) C_ ( y supp .0. ) )
171 146 170 ssfid 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( ( y oF ( .s ` Y ) U ) supp ( 0g ` Y ) ) e. Fin )
172 simp2 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> I e. V )
173 1 18 4 frlmbasmap 
 |-  ( ( I e. V /\ y e. B ) -> y e. ( ( Base ` R ) ^m I ) )
174 172 81 173 syl2an 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> y e. ( ( Base ` R ) ^m I ) )
175 elmapfn 
 |-  ( y e. ( ( Base ` R ) ^m I ) -> y Fn I )
176 174 175 syl 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> y Fn I )
177 12 adantr 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> U : I --> B )
178 177 ffnd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> U Fn I )
179 176 178 44 44 offun 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> Fun ( y oF ( .s ` Y ) U ) )
180 ovexd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( y oF ( .s ` Y ) U ) e. _V )
181 fvexd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( 0g ` Y ) e. _V )
182 funisfsupp 
 |-  ( ( Fun ( y oF ( .s ` Y ) U ) /\ ( y oF ( .s ` Y ) U ) e. _V /\ ( 0g ` Y ) e. _V ) -> ( ( y oF ( .s ` Y ) U ) finSupp ( 0g ` Y ) <-> ( ( y oF ( .s ` Y ) U ) supp ( 0g ` Y ) ) e. Fin ) )
183 179 180 181 182 syl3anc 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( ( y oF ( .s ` Y ) U ) finSupp ( 0g ` Y ) <-> ( ( y oF ( .s ` Y ) U ) supp ( 0g ` Y ) ) e. Fin ) )
184 171 183 mpbird 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( y oF ( .s ` Y ) U ) finSupp ( 0g ` Y ) )
185 51 54 44 62 143 184 gsumsubgcl 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> ( Y gsum ( y oF ( .s ` Y ) U ) ) e. ( K ` ( U " J ) ) )
186 50 185 eqeltrd 
 |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ y e. C ) -> y e. ( K ` ( U " J ) ) )
187 42 186 eqelssd 
 |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( K ` ( U " J ) ) = C )