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 \in {Base}_{W} ⟼ x (I))$
Assertion	frlmsnic	$⊢ (K \in Ring \land I \in V) \to F \in (W LMIso ringLMod (K))$

Proof

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

Metamath Proof Explorer

Theorem frlmsnic

Proof