frlmup1

Description: Any assignment of unit vectors to target vectors can be extended (uniquely) to a homomorphism from a free module to an arbitrary other module on the same base ring. (Contributed by Stefan O'Rear, 7-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Hypotheses	frlmup.f	$⊢ F = R freeLMod I$
	frlmup.b	$⊢ B = {Base}_{F}$
	frlmup.c	$⊢ C = {Base}_{T}$
	frlmup.v	$⊢ \underset{˙}{\cdot} = \cdot_{T}$
	frlmup.e	$⊢ E = (x \in B ⟼ \sum_{T} (x {\underset{˙}{\cdot}}_{f} A))$
	frlmup.t	$⊢ φ \to T \in LMod$
	frlmup.i	$⊢ φ \to I \in X$
	frlmup.r	$⊢ φ \to R = Scalar (T)$
	frlmup.a	$⊢ φ \to A : I ⟶ C$
Assertion	frlmup1	$⊢ φ \to E \in (F LMHom T)$

Proof

Step	Hyp	Ref	Expression
1		frlmup.f	$⊢ F = R freeLMod I$
2		frlmup.b	$⊢ B = {Base}_{F}$
3		frlmup.c	$⊢ C = {Base}_{T}$
4		frlmup.v	$⊢ \underset{˙}{\cdot} = \cdot_{T}$
5		frlmup.e	$⊢ E = (x \in B ⟼ \sum_{T} (x {\underset{˙}{\cdot}}_{f} A))$
6		frlmup.t	$⊢ φ \to T \in LMod$
7		frlmup.i	$⊢ φ \to I \in X$
8		frlmup.r	$⊢ φ \to R = Scalar (T)$
9		frlmup.a	$⊢ φ \to A : I ⟶ C$
10		eqid	$⊢ \cdot_{F} = \cdot_{F}$
11		eqid	$⊢ Scalar (F) = Scalar (F)$
12		eqid	$⊢ Scalar (T) = Scalar (T)$
13		eqid	$⊢ {Base}_{Scalar (F)} = {Base}_{Scalar (F)}$
14	12	lmodring	$⊢ T \in LMod \to Scalar (T) \in Ring$
15	6 14	syl	$⊢ φ \to Scalar (T) \in Ring$
16	8 15	eqeltrd	$⊢ φ \to R \in Ring$
17	1	frlmlmod	$⊢ (R \in Ring \land I \in X) \to F \in LMod$
18	16 7 17	syl2anc	$⊢ φ \to F \in LMod$
19	1	frlmsca	$⊢ (R \in Ring \land I \in X) \to R = Scalar (F)$
20	16 7 19	syl2anc	$⊢ φ \to R = Scalar (F)$
21	8 20	eqtr3d	$⊢ φ \to Scalar (T) = Scalar (F)$
22		eqid	$⊢ +_{F} = +_{F}$
23		eqid	$⊢ +_{T} = +_{T}$
24		lmodgrp	$⊢ F \in LMod \to F \in Grp$
25	18 24	syl	$⊢ φ \to F \in Grp$
26		lmodgrp	$⊢ T \in LMod \to T \in Grp$
27	6 26	syl	$⊢ φ \to T \in Grp$
28		eleq1w	$⊢ z = x \to (z \in B \leftrightarrow x \in B)$
29	28	anbi2d	$⊢ z = x \to ((φ \land z \in B) \leftrightarrow (φ \land x \in B))$
30		oveq1	$⊢ z = x \to z {\underset{˙}{\cdot}}_{f} A = x {\underset{˙}{\cdot}}_{f} A$
31	30	oveq2d	$⊢ z = x \to \sum_{T} (z {\underset{˙}{\cdot}}_{f} A) = \sum_{T} (x {\underset{˙}{\cdot}}_{f} A)$
32	31	eleq1d	$⊢ z = x \to (\sum_{T} (z {\underset{˙}{\cdot}}_{f} A) \in C \leftrightarrow \sum_{T} (x {\underset{˙}{\cdot}}_{f} A) \in C)$
33	29 32	imbi12d	$⊢ z = x \to (((φ \land z \in B) \to \sum_{T} (z {\underset{˙}{\cdot}}_{f} A) \in C) \leftrightarrow ((φ \land x \in B) \to \sum_{T} (x {\underset{˙}{\cdot}}_{f} A) \in C))$
34		eqid	$⊢ 0_{T} = 0_{T}$
35		lmodcmn	$⊢ T \in LMod \to T \in CMnd$
36	6 35	syl	$⊢ φ \to T \in CMnd$
37	36	adantr	$⊢ (φ \land z \in B) \to T \in CMnd$
38	7	adantr	$⊢ (φ \land z \in B) \to I \in X$
39	6	ad2antrr	$⊢ ((φ \land z \in B) \land (x \in {Base}_{R} \land y \in C)) \to T \in LMod$
40		simprl	$⊢ ((φ \land z \in B) \land (x \in {Base}_{R} \land y \in C)) \to x \in {Base}_{R}$
41	8	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (T)}$
42	41	ad2antrr	$⊢ ((φ \land z \in B) \land (x \in {Base}_{R} \land y \in C)) \to {Base}_{R} = {Base}_{Scalar (T)}$
43	40 42	eleqtrd	$⊢ ((φ \land z \in B) \land (x \in {Base}_{R} \land y \in C)) \to x \in {Base}_{Scalar (T)}$
44		simprr	$⊢ ((φ \land z \in B) \land (x \in {Base}_{R} \land y \in C)) \to y \in C$
45		eqid	$⊢ {Base}_{Scalar (T)} = {Base}_{Scalar (T)}$
46	3 12 4 45	lmodvscl	$⊢ (T \in LMod \land x \in {Base}_{Scalar (T)} \land y \in C) \to x \underset{˙}{\cdot} y \in C$
47	39 43 44 46	syl3anc	$⊢ ((φ \land z \in B) \land (x \in {Base}_{R} \land y \in C)) \to x \underset{˙}{\cdot} y \in C$
48		eqid	$⊢ {Base}_{R} = {Base}_{R}$
49	1 48 2	frlmbasf	$⊢ (I \in X \land z \in B) \to z : I ⟶ {Base}_{R}$
50	7 49	sylan	$⊢ (φ \land z \in B) \to z : I ⟶ {Base}_{R}$
51	9	adantr	$⊢ (φ \land z \in B) \to A : I ⟶ C$
52		inidm	$⊢ I \cap I = I$
53	47 50 51 38 38 52	off	$⊢ (φ \land z \in B) \to (z {\underset{˙}{\cdot}}_{f} A) : I ⟶ C$
54		ovexd	$⊢ (φ \land z \in B) \to z {\underset{˙}{\cdot}}_{f} A \in V$
55	53	ffund	$⊢ (φ \land z \in B) \to Fun (z {\underset{˙}{\cdot}}_{f} A)$
56		fvexd	$⊢ (φ \land z \in B) \to 0_{T} \in V$
57		eqid	$⊢ 0_{R} = 0_{R}$
58	1 57 2	frlmbasfsupp	$⊢ (I \in X \land z \in B) \to {finSupp}_{0_{R}} (z)$
59	7 58	sylan	$⊢ (φ \land z \in B) \to {finSupp}_{0_{R}} (z)$
60	8	fveq2d	$⊢ φ \to 0_{R} = 0_{Scalar (T)}$
61	60	eqcomd	$⊢ φ \to 0_{Scalar (T)} = 0_{R}$
62	61	breq2d	$⊢ φ \to ({finSupp}_{0_{Scalar (T)}} (z) \leftrightarrow {finSupp}_{0_{R}} (z))$
63	62	adantr	$⊢ (φ \land z \in B) \to ({finSupp}_{0_{Scalar (T)}} (z) \leftrightarrow {finSupp}_{0_{R}} (z))$
64	59 63	mpbird	$⊢ (φ \land z \in B) \to {finSupp}_{0_{Scalar (T)}} (z)$
65	64	fsuppimpd	$⊢ (φ \land z \in B) \to z supp 0_{Scalar (T)} \in Fin$
66		ssidd	$⊢ (φ \land z \in B) \to z supp 0_{Scalar (T)} \subseteq z supp 0_{Scalar (T)}$
67	6	ad2antrr	$⊢ ((φ \land z \in B) \land w \in C) \to T \in LMod$
68		eqid	$⊢ 0_{Scalar (T)} = 0_{Scalar (T)}$
69	3 12 4 68 34	lmod0vs	$⊢ (T \in LMod \land w \in C) \to 0_{Scalar (T)} \underset{˙}{\cdot} w = 0_{T}$
70	67 69	sylancom	$⊢ ((φ \land z \in B) \land w \in C) \to 0_{Scalar (T)} \underset{˙}{\cdot} w = 0_{T}$
71		fvexd	$⊢ (φ \land z \in B) \to 0_{Scalar (T)} \in V$
72	66 70 50 51 38 71	suppssof1	$⊢ (φ \land z \in B) \to (z {\underset{˙}{\cdot}}_{f} A) supp 0_{T} \subseteq z supp 0_{Scalar (T)}$
73		suppssfifsupp	$⊢ ((z {\underset{˙}{\cdot}}_{f} A \in V \land Fun (z {\underset{˙}{\cdot}}_{f} A) \land 0_{T} \in V) \land (z supp 0_{Scalar (T)} \in Fin \land (z {\underset{˙}{\cdot}}_{f} A) supp 0_{T} \subseteq z supp 0_{Scalar (T)})) \to {finSupp}_{0_{T}} ((z {\underset{˙}{\cdot}}_{f} A))$
74	54 55 56 65 72 73	syl32anc	$⊢ (φ \land z \in B) \to {finSupp}_{0_{T}} ((z {\underset{˙}{\cdot}}_{f} A))$
75	3 34 37 38 53 74	gsumcl	$⊢ (φ \land z \in B) \to \sum_{T} (z {\underset{˙}{\cdot}}_{f} A) \in C$
76	33 75	chvarvv	$⊢ (φ \land x \in B) \to \sum_{T} (x {\underset{˙}{\cdot}}_{f} A) \in C$
77	76 5	fmptd	$⊢ φ \to E : B ⟶ C$
78	36	adantr	$⊢ (φ \land (y \in B \land z \in B)) \to T \in CMnd$
79	7	adantr	$⊢ (φ \land (y \in B \land z \in B)) \to I \in X$
80		eleq1w	$⊢ z = y \to (z \in B \leftrightarrow y \in B)$
81	80	anbi2d	$⊢ z = y \to ((φ \land z \in B) \leftrightarrow (φ \land y \in B))$
82		oveq1	$⊢ z = y \to z {\underset{˙}{\cdot}}_{f} A = y {\underset{˙}{\cdot}}_{f} A$
83	82	feq1d	$⊢ z = y \to ((z {\underset{˙}{\cdot}}_{f} A) : I ⟶ C \leftrightarrow (y {\underset{˙}{\cdot}}_{f} A) : I ⟶ C)$
84	81 83	imbi12d	$⊢ z = y \to (((φ \land z \in B) \to (z {\underset{˙}{\cdot}}_{f} A) : I ⟶ C) \leftrightarrow ((φ \land y \in B) \to (y {\underset{˙}{\cdot}}_{f} A) : I ⟶ C))$
85	84 53	chvarvv	$⊢ (φ \land y \in B) \to (y {\underset{˙}{\cdot}}_{f} A) : I ⟶ C$
86	85	adantrr	$⊢ (φ \land (y \in B \land z \in B)) \to (y {\underset{˙}{\cdot}}_{f} A) : I ⟶ C$
87	53	adantrl	$⊢ (φ \land (y \in B \land z \in B)) \to (z {\underset{˙}{\cdot}}_{f} A) : I ⟶ C$
88	82	breq1d	$⊢ z = y \to ({finSupp}_{0_{T}} ((z {\underset{˙}{\cdot}}_{f} A)) \leftrightarrow {finSupp}_{0_{T}} ((y {\underset{˙}{\cdot}}_{f} A)))$
89	81 88	imbi12d	$⊢ z = y \to (((φ \land z \in B) \to {finSupp}_{0_{T}} ((z {\underset{˙}{\cdot}}_{f} A))) \leftrightarrow ((φ \land y \in B) \to {finSupp}_{0_{T}} ((y {\underset{˙}{\cdot}}_{f} A))))$
90	89 74	chvarvv	$⊢ (φ \land y \in B) \to {finSupp}_{0_{T}} ((y {\underset{˙}{\cdot}}_{f} A))$
91	90	adantrr	$⊢ (φ \land (y \in B \land z \in B)) \to {finSupp}_{0_{T}} ((y {\underset{˙}{\cdot}}_{f} A))$
92	74	adantrl	$⊢ (φ \land (y \in B \land z \in B)) \to {finSupp}_{0_{T}} ((z {\underset{˙}{\cdot}}_{f} A))$
93	3 34 23 78 79 86 87 91 92	gsumadd	$⊢ (φ \land (y \in B \land z \in B)) \to \sum_{T} ((y {\underset{˙}{\cdot}}_{f} A) {+_{T}}_{f} (z {\underset{˙}{\cdot}}_{f} A)) = (\sum_{T}, (y {\underset{˙}{\cdot}}_{f} A)) +_{T} (\sum_{T}, (z {\underset{˙}{\cdot}}_{f} A))$
94	2 22	lmodvacl	$⊢ (F \in LMod \land y \in B \land z \in B) \to y +_{F} z \in B$
95	94	3expb	$⊢ (F \in LMod \land (y \in B \land z \in B)) \to y +_{F} z \in B$
96	18 95	sylan	$⊢ (φ \land (y \in B \land z \in B)) \to y +_{F} z \in B$
97		oveq1	$⊢ x = y +_{F} z \to x {\underset{˙}{\cdot}}_{f} A = (y +_{F} z) {\underset{˙}{\cdot}}_{f} A$
98	97	oveq2d	$⊢ x = y +_{F} z \to \sum_{T} (x {\underset{˙}{\cdot}}_{f} A) = \sum_{T} ((y +_{F} z) {\underset{˙}{\cdot}}_{f} A)$
99		ovex	$⊢ \sum_{T} ((y +_{F} z) {\underset{˙}{\cdot}}_{f} A) \in V$
100	98 5 99	fvmpt	$⊢ y +_{F} z \in B \to E (y +_{F} z) = \sum_{T} ((y +_{F} z) {\underset{˙}{\cdot}}_{f} A)$
101	96 100	syl	$⊢ (φ \land (y \in B \land z \in B)) \to E (y +_{F} z) = \sum_{T} ((y +_{F} z) {\underset{˙}{\cdot}}_{f} A)$
102	16	adantr	$⊢ (φ \land (y \in B \land z \in B)) \to R \in Ring$
103		simprl	$⊢ (φ \land (y \in B \land z \in B)) \to y \in B$
104		simprr	$⊢ (φ \land (y \in B \land z \in B)) \to z \in B$
105		eqid	$⊢ +_{R} = +_{R}$
106	1 2 102 79 103 104 105 22	frlmplusgval	$⊢ (φ \land (y \in B \land z \in B)) \to y +_{F} z = y {+_{R}}_{f} z$
107	106	oveq1d	$⊢ (φ \land (y \in B \land z \in B)) \to (y +_{F} z) {\underset{˙}{\cdot}}_{f} A = (y {+_{R}}_{f} z) {\underset{˙}{\cdot}}_{f} A$
108	1 48 2	frlmbasf	$⊢ (I \in X \land y \in B) \to y : I ⟶ {Base}_{R}$
109	7 108	sylan	$⊢ (φ \land y \in B) \to y : I ⟶ {Base}_{R}$
110	109	adantrr	$⊢ (φ \land (y \in B \land z \in B)) \to y : I ⟶ {Base}_{R}$
111	110	ffnd	$⊢ (φ \land (y \in B \land z \in B)) \to y Fn I$
112	50	adantrl	$⊢ (φ \land (y \in B \land z \in B)) \to z : I ⟶ {Base}_{R}$
113	112	ffnd	$⊢ (φ \land (y \in B \land z \in B)) \to z Fn I$
114	111 113 79 79 52	offn	$⊢ (φ \land (y \in B \land z \in B)) \to (y {+_{R}}_{f} z) Fn I$
115	9	ffnd	$⊢ φ \to A Fn I$
116	115	adantr	$⊢ (φ \land (y \in B \land z \in B)) \to A Fn I$
117	114 116 79 79 52	offn	$⊢ (φ \land (y \in B \land z \in B)) \to ((y {+_{R}}_{f} z) {\underset{˙}{\cdot}}_{f} A) Fn I$
118	85	ffnd	$⊢ (φ \land y \in B) \to (y {\underset{˙}{\cdot}}_{f} A) Fn I$
119	118	adantrr	$⊢ (φ \land (y \in B \land z \in B)) \to (y {\underset{˙}{\cdot}}_{f} A) Fn I$
120	53	ffnd	$⊢ (φ \land z \in B) \to (z {\underset{˙}{\cdot}}_{f} A) Fn I$
121	120	adantrl	$⊢ (φ \land (y \in B \land z \in B)) \to (z {\underset{˙}{\cdot}}_{f} A) Fn I$
122	119 121 79 79 52	offn	$⊢ (φ \land (y \in B \land z \in B)) \to ((y {\underset{˙}{\cdot}}_{f} A) {+_{T}}_{f} (z {\underset{˙}{\cdot}}_{f} A)) Fn I$
123	8	fveq2d	$⊢ φ \to +_{R} = +_{Scalar (T)}$
124	123	ad2antrr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to +_{R} = +_{Scalar (T)}$
125	124	oveqd	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to y (x) +_{R} z (x) = y (x) +_{Scalar (T)} z (x)$
126	125	oveq1d	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (y (x) +_{R} z (x)) \underset{˙}{\cdot} A (x) = (y (x) +_{Scalar (T)} z (x)) \underset{˙}{\cdot} A (x)$
127	6	ad2antrr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to T \in LMod$
128	110	ffvelcdmda	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to y (x) \in {Base}_{R}$
129	41	ad2antrr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to {Base}_{R} = {Base}_{Scalar (T)}$
130	128 129	eleqtrd	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to y (x) \in {Base}_{Scalar (T)}$
131	112	ffvelcdmda	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to z (x) \in {Base}_{R}$
132	131 129	eleqtrd	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to z (x) \in {Base}_{Scalar (T)}$
133	9	adantr	$⊢ (φ \land (y \in B \land z \in B)) \to A : I ⟶ C$
134	133	ffvelcdmda	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to A (x) \in C$
135		eqid	$⊢ +_{Scalar (T)} = +_{Scalar (T)}$
136	3 23 12 4 45 135	lmodvsdir	$⊢ (T \in LMod \land (y (x) \in {Base}_{Scalar (T)} \land z (x) \in {Base}_{Scalar (T)} \land A (x) \in C)) \to (y (x) +_{Scalar (T)} z (x)) \underset{˙}{\cdot} A (x) = (y (x) \underset{˙}{\cdot} A (x)) +_{T} (z (x) \underset{˙}{\cdot} A (x))$
137	127 130 132 134 136	syl13anc	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (y (x) +_{Scalar (T)} z (x)) \underset{˙}{\cdot} A (x) = (y (x) \underset{˙}{\cdot} A (x)) +_{T} (z (x) \underset{˙}{\cdot} A (x))$
138	126 137	eqtrd	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (y (x) +_{R} z (x)) \underset{˙}{\cdot} A (x) = (y (x) \underset{˙}{\cdot} A (x)) +_{T} (z (x) \underset{˙}{\cdot} A (x))$
139	111	adantr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to y Fn I$
140	113	adantr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to z Fn I$
141	7	ad2antrr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to I \in X$
142		simpr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to x \in I$
143		fnfvof	$⊢ ((y Fn I \land z Fn I) \land (I \in X \land x \in I)) \to (y {+_{R}}_{f} z) (x) = y (x) +_{R} z (x)$
144	139 140 141 142 143	syl22anc	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (y {+_{R}}_{f} z) (x) = y (x) +_{R} z (x)$
145	144	oveq1d	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (y {+_{R}}_{f} z) (x) \underset{˙}{\cdot} A (x) = (y (x) +_{R} z (x)) \underset{˙}{\cdot} A (x)$
146	115	ad2antrr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to A Fn I$
147		fnfvof	$⊢ ((y Fn I \land A Fn I) \land (I \in X \land x \in I)) \to (y {\underset{˙}{\cdot}}_{f} A) (x) = y (x) \underset{˙}{\cdot} A (x)$
148	139 146 141 142 147	syl22anc	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (y {\underset{˙}{\cdot}}_{f} A) (x) = y (x) \underset{˙}{\cdot} A (x)$
149		fnfvof	$⊢ ((z Fn I \land A Fn I) \land (I \in X \land x \in I)) \to (z {\underset{˙}{\cdot}}_{f} A) (x) = z (x) \underset{˙}{\cdot} A (x)$
150	140 146 141 142 149	syl22anc	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (z {\underset{˙}{\cdot}}_{f} A) (x) = z (x) \underset{˙}{\cdot} A (x)$
151	148 150	oveq12d	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (y {\underset{˙}{\cdot}}_{f} A) (x) +_{T} (z {\underset{˙}{\cdot}}_{f} A) (x) = (y (x) \underset{˙}{\cdot} A (x)) +_{T} (z (x) \underset{˙}{\cdot} A (x))$
152	138 145 151	3eqtr4d	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (y {+_{R}}_{f} z) (x) \underset{˙}{\cdot} A (x) = (y {\underset{˙}{\cdot}}_{f} A) (x) +_{T} (z {\underset{˙}{\cdot}}_{f} A) (x)$
153	114	adantr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (y {+_{R}}_{f} z) Fn I$
154		fnfvof	$⊢ (((y {+_{R}}_{f} z) Fn I \land A Fn I) \land (I \in X \land x \in I)) \to ((y {+_{R}}_{f} z) {\underset{˙}{\cdot}}_{f} A) (x) = (y {+_{R}}_{f} z) (x) \underset{˙}{\cdot} A (x)$
155	153 146 141 142 154	syl22anc	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to ((y {+_{R}}_{f} z) {\underset{˙}{\cdot}}_{f} A) (x) = (y {+_{R}}_{f} z) (x) \underset{˙}{\cdot} A (x)$
156	119	adantr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (y {\underset{˙}{\cdot}}_{f} A) Fn I$
157	121	adantr	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to (z {\underset{˙}{\cdot}}_{f} A) Fn I$
158		fnfvof	$⊢ (((y {\underset{˙}{\cdot}}_{f} A) Fn I \land (z {\underset{˙}{\cdot}}_{f} A) Fn I) \land (I \in X \land x \in I)) \to ((y {\underset{˙}{\cdot}}_{f} A) {+_{T}}_{f} (z {\underset{˙}{\cdot}}_{f} A)) (x) = (y {\underset{˙}{\cdot}}_{f} A) (x) +_{T} (z {\underset{˙}{\cdot}}_{f} A) (x)$
159	156 157 141 142 158	syl22anc	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to ((y {\underset{˙}{\cdot}}_{f} A) {+_{T}}_{f} (z {\underset{˙}{\cdot}}_{f} A)) (x) = (y {\underset{˙}{\cdot}}_{f} A) (x) +_{T} (z {\underset{˙}{\cdot}}_{f} A) (x)$
160	152 155 159	3eqtr4d	$⊢ ((φ \land (y \in B \land z \in B)) \land x \in I) \to ((y {+_{R}}_{f} z) {\underset{˙}{\cdot}}_{f} A) (x) = ((y {\underset{˙}{\cdot}}_{f} A) {+_{T}}_{f} (z {\underset{˙}{\cdot}}_{f} A)) (x)$
161	117 122 160	eqfnfvd	$⊢ (φ \land (y \in B \land z \in B)) \to (y {+_{R}}_{f} z) {\underset{˙}{\cdot}}_{f} A = (y {\underset{˙}{\cdot}}_{f} A) {+_{T}}_{f} (z {\underset{˙}{\cdot}}_{f} A)$
162	107 161	eqtrd	$⊢ (φ \land (y \in B \land z \in B)) \to (y +_{F} z) {\underset{˙}{\cdot}}_{f} A = (y {\underset{˙}{\cdot}}_{f} A) {+_{T}}_{f} (z {\underset{˙}{\cdot}}_{f} A)$
163	162	oveq2d	$⊢ (φ \land (y \in B \land z \in B)) \to \sum_{T} ((y +_{F} z) {\underset{˙}{\cdot}}_{f} A) = \sum_{T} ((y {\underset{˙}{\cdot}}_{f} A) {+_{T}}_{f} (z {\underset{˙}{\cdot}}_{f} A))$
164	101 163	eqtrd	$⊢ (φ \land (y \in B \land z \in B)) \to E (y +_{F} z) = \sum_{T} ((y {\underset{˙}{\cdot}}_{f} A) {+_{T}}_{f} (z {\underset{˙}{\cdot}}_{f} A))$
165		oveq1	$⊢ x = y \to x {\underset{˙}{\cdot}}_{f} A = y {\underset{˙}{\cdot}}_{f} A$
166	165	oveq2d	$⊢ x = y \to \sum_{T} (x {\underset{˙}{\cdot}}_{f} A) = \sum_{T} (y {\underset{˙}{\cdot}}_{f} A)$
167		ovex	$⊢ \sum_{T} (y {\underset{˙}{\cdot}}_{f} A) \in V$
168	166 5 167	fvmpt	$⊢ y \in B \to E (y) = \sum_{T} (y {\underset{˙}{\cdot}}_{f} A)$
169	168	ad2antrl	$⊢ (φ \land (y \in B \land z \in B)) \to E (y) = \sum_{T} (y {\underset{˙}{\cdot}}_{f} A)$
170		oveq1	$⊢ x = z \to x {\underset{˙}{\cdot}}_{f} A = z {\underset{˙}{\cdot}}_{f} A$
171	170	oveq2d	$⊢ x = z \to \sum_{T} (x {\underset{˙}{\cdot}}_{f} A) = \sum_{T} (z {\underset{˙}{\cdot}}_{f} A)$
172		ovex	$⊢ \sum_{T} (z {\underset{˙}{\cdot}}_{f} A) \in V$
173	171 5 172	fvmpt	$⊢ z \in B \to E (z) = \sum_{T} (z {\underset{˙}{\cdot}}_{f} A)$
174	173	ad2antll	$⊢ (φ \land (y \in B \land z \in B)) \to E (z) = \sum_{T} (z {\underset{˙}{\cdot}}_{f} A)$
175	169 174	oveq12d	$⊢ (φ \land (y \in B \land z \in B)) \to E (y) +_{T} E (z) = (\sum_{T}, (y {\underset{˙}{\cdot}}_{f} A)) +_{T} (\sum_{T}, (z {\underset{˙}{\cdot}}_{f} A))$
176	93 164 175	3eqtr4d	$⊢ (φ \land (y \in B \land z \in B)) \to E (y +_{F} z) = E (y) +_{T} E (z)$
177	2 3 22 23 25 27 77 176	isghmd	$⊢ φ \to E \in (F GrpHom T)$
178	6	adantr	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to T \in LMod$
179	7	adantr	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to I \in X$
180	21	fveq2d	$⊢ φ \to {Base}_{Scalar (T)} = {Base}_{Scalar (F)}$
181	180	eleq2d	$⊢ φ \to (y \in {Base}_{Scalar (T)} \leftrightarrow y \in {Base}_{Scalar (F)})$
182	181	biimpar	$⊢ (φ \land y \in {Base}_{Scalar (F)}) \to y \in {Base}_{Scalar (T)}$
183	182	adantrr	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to y \in {Base}_{Scalar (T)}$
184	53	adantrl	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to (z {\underset{˙}{\cdot}}_{f} A) : I ⟶ C$
185	184	ffvelcdmda	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to (z {\underset{˙}{\cdot}}_{f} A) (x) \in C$
186	53	feqmptd	$⊢ (φ \land z \in B) \to z {\underset{˙}{\cdot}}_{f} A = (x \in I ⟼ (z {\underset{˙}{\cdot}}_{f} A) (x))$
187	186 74	eqbrtrrd	$⊢ (φ \land z \in B) \to {finSupp}_{0_{T}} ((x \in I ⟼ (z {\underset{˙}{\cdot}}_{f} A) (x)))$
188	187	adantrl	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to {finSupp}_{0_{T}} ((x \in I ⟼ (z {\underset{˙}{\cdot}}_{f} A) (x)))$
189	3 12 45 34 23 4 178 179 183 185 188	gsumvsmul	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to \underset{x \in I}{\sum_{T}} (y \underset{˙}{\cdot} (z {\underset{˙}{\cdot}}_{f} A) (x)) = y \underset{˙}{\cdot} (\underset{x \in I}{\sum_{T}}, (z {\underset{˙}{\cdot}}_{f} A) (x))$
190	18	adantr	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to F \in LMod$
191		simprl	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to y \in {Base}_{Scalar (F)}$
192		simprr	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to z \in B$
193	2 11 10 13	lmodvscl	$⊢ (F \in LMod \land y \in {Base}_{Scalar (F)} \land z \in B) \to y \cdot_{F} z \in B$
194	190 191 192 193	syl3anc	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to y \cdot_{F} z \in B$
195	1 48 2	frlmbasf	$⊢ (I \in X \land y \cdot_{F} z \in B) \to (y \cdot_{F} z) : I ⟶ {Base}_{R}$
196	179 194 195	syl2anc	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to (y \cdot_{F} z) : I ⟶ {Base}_{R}$
197	196	ffnd	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to (y \cdot_{F} z) Fn I$
198	115	adantr	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to A Fn I$
199	197 198 179 179 52	offn	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) Fn I$
200		dffn2	$⊢ ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) Fn I \leftrightarrow ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) : I ⟶ V$
201	199 200	sylib	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) : I ⟶ V$
202	201	feqmptd	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to (y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A = (x \in I ⟼ ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) (x))$
203	8	fveq2d	$⊢ φ \to \cdot_{R} = \cdot_{Scalar (T)}$
204	203	ad2antrr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to \cdot_{R} = \cdot_{Scalar (T)}$
205	204	oveqd	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to y \cdot_{R} z (x) = y \cdot_{Scalar (T)} z (x)$
206	205	oveq1d	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to (y \cdot_{R} z (x)) \underset{˙}{\cdot} A (x) = (y \cdot_{Scalar (T)} z (x)) \underset{˙}{\cdot} A (x)$
207	6	ad2antrr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to T \in LMod$
208		simplrl	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to y \in {Base}_{Scalar (F)}$
209	180	ad2antrr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to {Base}_{Scalar (T)} = {Base}_{Scalar (F)}$
210	208 209	eleqtrrd	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to y \in {Base}_{Scalar (T)}$
211	50	ffvelcdmda	$⊢ ((φ \land z \in B) \land x \in I) \to z (x) \in {Base}_{R}$
212	41	ad2antrr	$⊢ ((φ \land z \in B) \land x \in I) \to {Base}_{R} = {Base}_{Scalar (T)}$
213	211 212	eleqtrd	$⊢ ((φ \land z \in B) \land x \in I) \to z (x) \in {Base}_{Scalar (T)}$
214	213	adantlrl	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to z (x) \in {Base}_{Scalar (T)}$
215	9	ffvelcdmda	$⊢ (φ \land x \in I) \to A (x) \in C$
216	215	adantlr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to A (x) \in C$
217		eqid	$⊢ \cdot_{Scalar (T)} = \cdot_{Scalar (T)}$
218	3 12 4 45 217	lmodvsass	$⊢ (T \in LMod \land (y \in {Base}_{Scalar (T)} \land z (x) \in {Base}_{Scalar (T)} \land A (x) \in C)) \to (y \cdot_{Scalar (T)} z (x)) \underset{˙}{\cdot} A (x) = y \underset{˙}{\cdot} (z (x) \underset{˙}{\cdot} A (x))$
219	207 210 214 216 218	syl13anc	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to (y \cdot_{Scalar (T)} z (x)) \underset{˙}{\cdot} A (x) = y \underset{˙}{\cdot} (z (x) \underset{˙}{\cdot} A (x))$
220	206 219	eqtrd	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to (y \cdot_{R} z (x)) \underset{˙}{\cdot} A (x) = y \underset{˙}{\cdot} (z (x) \underset{˙}{\cdot} A (x))$
221	197	adantr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to (y \cdot_{F} z) Fn I$
222	115	ad2antrr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to A Fn I$
223	7	ad2antrr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to I \in X$
224		simpr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to x \in I$
225		fnfvof	$⊢ (((y \cdot_{F} z) Fn I \land A Fn I) \land (I \in X \land x \in I)) \to ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) (x) = (y \cdot_{F} z) (x) \underset{˙}{\cdot} A (x)$
226	221 222 223 224 225	syl22anc	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) (x) = (y \cdot_{F} z) (x) \underset{˙}{\cdot} A (x)$
227	20	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (F)}$
228	227	ad2antrr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to {Base}_{R} = {Base}_{Scalar (F)}$
229	208 228	eleqtrrd	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to y \in {Base}_{R}$
230		simplrr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to z \in B$
231		eqid	$⊢ \cdot_{R} = \cdot_{R}$
232	1 2 48 223 229 230 224 10 231	frlmvscaval	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to (y \cdot_{F} z) (x) = y \cdot_{R} z (x)$
233	232	oveq1d	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to (y \cdot_{F} z) (x) \underset{˙}{\cdot} A (x) = (y \cdot_{R} z (x)) \underset{˙}{\cdot} A (x)$
234	226 233	eqtrd	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) (x) = (y \cdot_{R} z (x)) \underset{˙}{\cdot} A (x)$
235	50	ffnd	$⊢ (φ \land z \in B) \to z Fn I$
236	235	adantrl	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to z Fn I$
237	236	adantr	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to z Fn I$
238	237 222 223 224 149	syl22anc	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to (z {\underset{˙}{\cdot}}_{f} A) (x) = z (x) \underset{˙}{\cdot} A (x)$
239	238	oveq2d	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to y \underset{˙}{\cdot} (z {\underset{˙}{\cdot}}_{f} A) (x) = y \underset{˙}{\cdot} (z (x) \underset{˙}{\cdot} A (x))$
240	220 234 239	3eqtr4d	$⊢ ((φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \land x \in I) \to ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) (x) = y \underset{˙}{\cdot} (z {\underset{˙}{\cdot}}_{f} A) (x)$
241	240	mpteq2dva	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to (x \in I ⟼ ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) (x)) = (x \in I ⟼ y \underset{˙}{\cdot} (z {\underset{˙}{\cdot}}_{f} A) (x))$
242	202 241	eqtrd	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to (y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A = (x \in I ⟼ y \underset{˙}{\cdot} (z {\underset{˙}{\cdot}}_{f} A) (x))$
243	242	oveq2d	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to \sum_{T} ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) = \underset{x \in I}{\sum_{T}} (y \underset{˙}{\cdot} (z {\underset{˙}{\cdot}}_{f} A) (x))$
244	184	feqmptd	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to z {\underset{˙}{\cdot}}_{f} A = (x \in I ⟼ (z {\underset{˙}{\cdot}}_{f} A) (x))$
245	244	oveq2d	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to \sum_{T} (z {\underset{˙}{\cdot}}_{f} A) = \underset{x \in I}{\sum_{T}} (z {\underset{˙}{\cdot}}_{f} A) (x)$
246	245	oveq2d	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to y \underset{˙}{\cdot} (\sum_{T}, (z {\underset{˙}{\cdot}}_{f} A)) = y \underset{˙}{\cdot} (\underset{x \in I}{\sum_{T}}, (z {\underset{˙}{\cdot}}_{f} A) (x))$
247	189 243 246	3eqtr4d	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to \sum_{T} ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) = y \underset{˙}{\cdot} (\sum_{T}, (z {\underset{˙}{\cdot}}_{f} A))$
248		oveq1	$⊢ x = y \cdot_{F} z \to x {\underset{˙}{\cdot}}_{f} A = (y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A$
249	248	oveq2d	$⊢ x = y \cdot_{F} z \to \sum_{T} (x {\underset{˙}{\cdot}}_{f} A) = \sum_{T} ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A)$
250		ovex	$⊢ \sum_{T} ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A) \in V$
251	249 5 250	fvmpt	$⊢ y \cdot_{F} z \in B \to E (y \cdot_{F} z) = \sum_{T} ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A)$
252	194 251	syl	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to E (y \cdot_{F} z) = \sum_{T} ((y \cdot_{F} z) {\underset{˙}{\cdot}}_{f} A)$
253	173	oveq2d	$⊢ z \in B \to y \underset{˙}{\cdot} E (z) = y \underset{˙}{\cdot} (\sum_{T}, (z {\underset{˙}{\cdot}}_{f} A))$
254	253	ad2antll	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to y \underset{˙}{\cdot} E (z) = y \underset{˙}{\cdot} (\sum_{T}, (z {\underset{˙}{\cdot}}_{f} A))$
255	247 252 254	3eqtr4d	$⊢ (φ \land (y \in {Base}_{Scalar (F)} \land z \in B)) \to E (y \cdot_{F} z) = y \underset{˙}{\cdot} E (z)$
256	2 10 4 11 12 13 18 6 21 177 255	islmhmd	$⊢ φ \to E \in (F LMHom T)$

Metamath Proof Explorer

Theorem frlmup1

Proof