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 ⊢ 𝑊 = ( 𝐾 freeLMod { 𝐼 } )
frlmsnic.1 ⊢ 𝐹 = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ‘ 𝐼 ) )
Assertion frlmsnic ( ( 𝐾 ∈ Ring ∧ 𝐼 ∈ V ) → 𝐹 ∈ ( 𝑊 LMIso ( ringLMod ‘ 𝐾 ) ) )

Proof

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