Metamath Proof Explorer

Theorem frlmsnic

Description: Given a free module with a singleton as the index set, that is, a free module of one-dimensional vectors, the function that maps each vector to its coordinate is a module isomorphism from that module to its ring of scalars seen as a module. (Contributed by Steven Nguyen, 18-Aug-2023)

Ref Expression
Hypotheses frlmsnic.w 
|- W = ( K freeLMod { I } )
frlmsnic.1 
|- F = ( x e. ( Base ` W ) |-> ( x ` I ) )
Assertion frlmsnic 
|- ( ( K e. Ring /\ I e. _V ) -> F e. ( W LMIso ( ringLMod ` K ) ) )

Proof

Step Hyp Ref Expression
1 frlmsnic.w 
 |-  W = ( K freeLMod { I } )
2 frlmsnic.1 
 |-  F = ( x e. ( Base ` W ) |-> ( x ` I ) )
3 eqid 
 |-  ( Base ` W ) = ( Base ` W )
4 eqid 
 |-  ( .s ` W ) = ( .s ` W )
5 eqid 
 |-  ( .s ` ( ringLMod ` K ) ) = ( .s ` ( ringLMod ` K ) )
6 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
7 eqid 
 |-  ( Scalar ` ( ringLMod ` K ) ) = ( Scalar ` ( ringLMod ` K ) )
8 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
9 snex 
 |-  { I } e. _V
10 1 frlmlmod 
 |-  ( ( K e. Ring /\ { I } e. _V ) -> W e. LMod )
11 9 10 mpan2 
 |-  ( K e. Ring -> W e. LMod )
12 11 adantr 
 |-  ( ( K e. Ring /\ I e. _V ) -> W e. LMod )
13 rlmlmod 
 |-  ( K e. Ring -> ( ringLMod ` K ) e. LMod )
14 13 adantr 
 |-  ( ( K e. Ring /\ I e. _V ) -> ( ringLMod ` K ) e. LMod )
15 rlmsca 
 |-  ( K e. Ring -> K = ( Scalar ` ( ringLMod ` K ) ) )
16 15 adantr 
 |-  ( ( K e. Ring /\ I e. _V ) -> K = ( Scalar ` ( ringLMod ` K ) ) )
17 1 frlmsca 
 |-  ( ( K e. Ring /\ { I } e. _V ) -> K = ( Scalar ` W ) )
18 9 17 mpan2 
 |-  ( K e. Ring -> K = ( Scalar ` W ) )
19 18 adantr 
 |-  ( ( K e. Ring /\ I e. _V ) -> K = ( Scalar ` W ) )
20 16 19 eqtr3d 
 |-  ( ( K e. Ring /\ I e. _V ) -> ( Scalar ` ( ringLMod ` K ) ) = ( Scalar ` W ) )
21 rlmbas 
 |-  ( Base ` K ) = ( Base ` ( ringLMod ` K ) )
22 eqid 
 |-  ( +g ` W ) = ( +g ` W )
23 rlmplusg 
 |-  ( +g ` K ) = ( +g ` ( ringLMod ` K ) )
24 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
25 12 24 syl 
 |-  ( ( K e. Ring /\ I e. _V ) -> W e. Grp )
26 lmodgrp 
 |-  ( ( ringLMod ` K ) e. LMod -> ( ringLMod ` K ) e. Grp )
27 13 26 syl 
 |-  ( K e. Ring -> ( ringLMod ` K ) e. Grp )
28 27 adantr 
 |-  ( ( K e. Ring /\ I e. _V ) -> ( ringLMod ` K ) e. Grp )
29 eqid 
 |-  ( Base ` K ) = ( Base ` K )
30 1 29 3 frlmbasf 
 |-  ( ( { I } e. _V /\ x e. ( Base ` W ) ) -> x : { I } --> ( Base ` K ) )
31 9 30 mpan 
 |-  ( x e. ( Base ` W ) -> x : { I } --> ( Base ` K ) )
32 31 adantl 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ x e. ( Base ` W ) ) -> x : { I } --> ( Base ` K ) )
33 snidg 
 |-  ( I e. _V -> I e. { I } )
34 33 adantl 
 |-  ( ( K e. Ring /\ I e. _V ) -> I e. { I } )
35 34 adantr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ x e. ( Base ` W ) ) -> I e. { I } )
36 32 35 ffvelcdmd 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ x e. ( Base ` W ) ) -> ( x ` I ) e. ( Base ` K ) )
37 36 2 fmptd 
 |-  ( ( K e. Ring /\ I e. _V ) -> F : ( Base ` W ) --> ( Base ` K ) )
38 simpll 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> K e. Ring )
39 9 a1i 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> { I } e. _V )
40 simprl 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> x e. ( Base ` W ) )
41 simprr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
42 34 adantr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> I e. { I } )
43 eqid 
 |-  ( +g ` K ) = ( +g ` K )
44 1 3 38 39 40 41 42 43 22 frlmvplusgvalc 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( x ( +g ` W ) y ) ` I ) = ( ( x ` I ) ( +g ` K ) ( y ` I ) ) )
45 12 adantr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> W e. LMod )
46 3 22 lmodvacl 
 |-  ( ( W e. LMod /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( x ( +g ` W ) y ) e. ( Base ` W ) )
47 45 40 41 46 syl3anc 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( +g ` W ) y ) e. ( Base ` W ) )
48 fveq1 
 |-  ( t = ( x ( +g ` W ) y ) -> ( t ` I ) = ( ( x ( +g ` W ) y ) ` I ) )
49 fveq1 
 |-  ( x = t -> ( x ` I ) = ( t ` I ) )
50 49 cbvmptv 
 |-  ( x e. ( Base ` W ) |-> ( x ` I ) ) = ( t e. ( Base ` W ) |-> ( t ` I ) )
51 2 50 eqtri 
 |-  F = ( t e. ( Base ` W ) |-> ( t ` I ) )
52 fvexd 
 |-  ( t e. ( Base ` W ) -> ( t ` I ) e. _V )
53 48 51 52 fvmpt3 
 |-  ( ( x ( +g ` W ) y ) e. ( Base ` W ) -> ( F ` ( x ( +g ` W ) y ) ) = ( ( x ( +g ` W ) y ) ` I ) )
54 47 53 syl 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( F ` ( x ( +g ` W ) y ) ) = ( ( x ( +g ` W ) y ) ` I ) )
55 2 a1i 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> F = ( x e. ( Base ` W ) |-> ( x ` I ) ) )
56 fvexd 
 |-  ( ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ x e. ( Base ` W ) ) -> ( x ` I ) e. _V )
57 55 56 fvmpt2d 
 |-  ( ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ x e. ( Base ` W ) ) -> ( F ` x ) = ( x ` I ) )
58 40 57 mpdan 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( F ` x ) = ( x ` I ) )
59 fveq1 
 |-  ( x = y -> ( x ` I ) = ( y ` I ) )
60 fvexd 
 |-  ( x e. ( Base ` W ) -> ( x ` I ) e. _V )
61 59 2 60 fvmpt3 
 |-  ( y e. ( Base ` W ) -> ( F ` y ) = ( y ` I ) )
62 41 61 syl 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( F ` y ) = ( y ` I ) )
63 58 62 oveq12d 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( F ` x ) ( +g ` K ) ( F ` y ) ) = ( ( x ` I ) ( +g ` K ) ( y ` I ) ) )
64 44 54 63 3eqtr4d 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( F ` ( x ( +g ` W ) y ) ) = ( ( F ` x ) ( +g ` K ) ( F ` y ) ) )
65 3 21 22 23 25 28 37 64 isghmd 
 |-  ( ( K e. Ring /\ I e. _V ) -> F e. ( W GrpHom ( ringLMod ` K ) ) )
66 9 a1i 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> { I } e. _V )
67 19 eqcomd 
 |-  ( ( K e. Ring /\ I e. _V ) -> ( Scalar ` W ) = K )
68 67 fveq2d 
 |-  ( ( K e. Ring /\ I e. _V ) -> ( Base ` ( Scalar ` W ) ) = ( Base ` K ) )
69 68 eleq2d 
 |-  ( ( K e. Ring /\ I e. _V ) -> ( x e. ( Base ` ( Scalar ` W ) ) <-> x e. ( Base ` K ) ) )
70 69 biimpa 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ x e. ( Base ` ( Scalar ` W ) ) ) -> x e. ( Base ` K ) )
71 70 adantrr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> x e. ( Base ` K ) )
72 simprr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
73 34 adantr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> I e. { I } )
74 eqid 
 |-  ( .r ` K ) = ( .r ` K )
75 1 3 29 66 71 72 73 4 74 frlmvscaval 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> ( ( x ( .s ` W ) y ) ` I ) = ( x ( .r ` K ) ( y ` I ) ) )
76 rlmvsca 
 |-  ( .r ` K ) = ( .s ` ( ringLMod ` K ) )
77 76 oveqi 
 |-  ( x ( .r ` K ) ( y ` I ) ) = ( x ( .s ` ( ringLMod ` K ) ) ( y ` I ) )
78 75 77 eqtrdi 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> ( ( x ( .s ` W ) y ) ` I ) = ( x ( .s ` ( ringLMod ` K ) ) ( y ` I ) ) )
79 fveq1 
 |-  ( x = u -> ( x ` I ) = ( u ` I ) )
80 79 cbvmptv 
 |-  ( x e. ( Base ` W ) |-> ( x ` I ) ) = ( u e. ( Base ` W ) |-> ( u ` I ) )
81 2 80 eqtri 
 |-  F = ( u e. ( Base ` W ) |-> ( u ` I ) )
82 fveq1 
 |-  ( u = ( x ( .s ` W ) y ) -> ( u ` I ) = ( ( x ( .s ` W ) y ) ` I ) )
83 9 a1i 
 |-  ( I e. _V -> { I } e. _V )
84 83 10 sylan2 
 |-  ( ( K e. Ring /\ I e. _V ) -> W e. LMod )
85 84 adantr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> W e. LMod )
86 simprl 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> x e. ( Base ` ( Scalar ` W ) ) )
87 3 6 4 8 85 86 72 lmodvscld 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> ( x ( .s ` W ) y ) e. ( Base ` W ) )
88 fvexd 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> ( ( x ( .s ` W ) y ) ` I ) e. _V )
89 81 82 87 88 fvmptd3 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> ( F ` ( x ( .s ` W ) y ) ) = ( ( x ( .s ` W ) y ) ` I ) )
90 fvex 
 |-  ( x ` I ) e. _V
91 59 2 90 fvmpt3i 
 |-  ( y e. ( Base ` W ) -> ( F ` y ) = ( y ` I ) )
92 72 91 syl 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> ( F ` y ) = ( y ` I ) )
93 92 oveq2d 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> ( x ( .s ` ( ringLMod ` K ) ) ( F ` y ) ) = ( x ( .s ` ( ringLMod ` K ) ) ( y ` I ) ) )
94 78 89 93 3eqtr4d 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) ) -> ( F ` ( x ( .s ` W ) y ) ) = ( x ( .s ` ( ringLMod ` K ) ) ( F ` y ) ) )
95 3 4 5 6 7 8 12 14 20 65 94 islmhmd 
 |-  ( ( K e. Ring /\ I e. _V ) -> F e. ( W LMHom ( ringLMod ` K ) ) )
96 simplr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ y e. ( Base ` K ) ) -> I e. _V )
97 simpr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ y e. ( Base ` K ) ) -> y e. ( Base ` K ) )
98 96 97 fsnd 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ y e. ( Base ` K ) ) -> { <. I , y >. } : { I } --> ( Base ` K ) )
99 simpll 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ y e. ( Base ` K ) ) -> K e. Ring )
100 snfi 
 |-  { I } e. Fin
101 1 29 3 frlmfielbas 
 |-  ( ( K e. Ring /\ { I } e. Fin ) -> ( { <. I , y >. } e. ( Base ` W ) <-> { <. I , y >. } : { I } --> ( Base ` K ) ) )
102 99 100 101 sylancl 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ y e. ( Base ` K ) ) -> ( { <. I , y >. } e. ( Base ` W ) <-> { <. I , y >. } : { I } --> ( Base ` K ) ) )
103 98 102 mpbird 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ y e. ( Base ` K ) ) -> { <. I , y >. } e. ( Base ` W ) )
104 fveq1 
 |-  ( x = { <. I , y >. } -> ( x ` I ) = ( { <. I , y >. } ` I ) )
105 104 adantl 
 |-  ( ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) /\ x = { <. I , y >. } ) -> ( x ` I ) = ( { <. I , y >. } ` I ) )
106 simpllr 
 |-  ( ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) /\ x = { <. I , y >. } ) -> I e. _V )
107 vex 
 |-  y e. _V
108 fvsng 
 |-  ( ( I e. _V /\ y e. _V ) -> ( { <. I , y >. } ` I ) = y )
109 106 107 108 sylancl 
 |-  ( ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) /\ x = { <. I , y >. } ) -> ( { <. I , y >. } ` I ) = y )
110 105 109 eqtr2d 
 |-  ( ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) /\ x = { <. I , y >. } ) -> y = ( x ` I ) )
111 110 ex 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) -> ( x = { <. I , y >. } -> y = ( x ` I ) ) )
112 simplr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) -> I e. _V )
113 32 adantrr 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) -> x : { I } --> ( Base ` K ) )
114 113 ffnd 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) -> x Fn { I } )
115 fnsnbg 
 |-  ( I e. _V -> ( x Fn { I } <-> x = { <. I , ( x ` I ) >. } ) )
116 115 biimpd 
 |-  ( I e. _V -> ( x Fn { I } -> x = { <. I , ( x ` I ) >. } ) )
117 112 114 116 sylc 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) -> x = { <. I , ( x ` I ) >. } )
118 opeq2 
 |-  ( y = ( x ` I ) -> <. I , y >. = <. I , ( x ` I ) >. )
119 118 sneqd 
 |-  ( y = ( x ` I ) -> { <. I , y >. } = { <. I , ( x ` I ) >. } )
120 119 eqeq2d 
 |-  ( y = ( x ` I ) -> ( x = { <. I , y >. } <-> x = { <. I , ( x ` I ) >. } ) )
121 117 120 syl5ibrcom 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) -> ( y = ( x ` I ) -> x = { <. I , y >. } ) )
122 111 121 impbid 
 |-  ( ( ( K e. Ring /\ I e. _V ) /\ ( x e. ( Base ` W ) /\ y e. ( Base ` K ) ) ) -> ( x = { <. I , y >. } <-> y = ( x ` I ) ) )
123 2 36 103 122 f1o2d 
 |-  ( ( K e. Ring /\ I e. _V ) -> F : ( Base ` W ) -1-1-onto-> ( Base ` K ) )
124 21 a1i 
 |-  ( ( K e. Ring /\ I e. _V ) -> ( Base ` K ) = ( Base ` ( ringLMod ` K ) ) )
125 124 f1oeq3d 
 |-  ( ( K e. Ring /\ I e. _V ) -> ( F : ( Base ` W ) -1-1-onto-> ( Base ` K ) <-> F : ( Base ` W ) -1-1-onto-> ( Base ` ( ringLMod ` K ) ) ) )
126 123 125 mpbid 
 |-  ( ( K e. Ring /\ I e. _V ) -> F : ( Base ` W ) -1-1-onto-> ( Base ` ( ringLMod ` K ) ) )
127 eqid 
 |-  ( Base ` ( ringLMod ` K ) ) = ( Base ` ( ringLMod ` K ) )
128 3 127 islmim 
 |-  ( F e. ( W LMIso ( ringLMod ` K ) ) <-> ( F e. ( W LMHom ( ringLMod ` K ) ) /\ F : ( Base ` W ) -1-1-onto-> ( Base ` ( ringLMod ` K ) ) ) )
129 95 126 128 sylanbrc 
 |-  ( ( K e. Ring /\ I e. _V ) -> F e. ( W LMIso ( ringLMod ` K ) ) )