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 Base W x I
Assertion frlmsnic K Ring I V F W LMIso ringLMod K

Proof

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