Theorem frlmup1 19956

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.)

Hypotheses

Ref	Expression
frlmup.f	⊢ 𝐹 = (𝑅 freeLMod 𝐼)
frlmup.b	⊢ 𝐵 = (Base‘𝐹)
frlmup.c	⊢ 𝐶 = (Base‘𝑇)
frlmup.v	⊢ · = ( ·𝑠 ‘𝑇)
frlmup.e	⊢ 𝐸 = (𝑥 ∈ 𝐵 ↦ (𝑇 Σg (𝑥 ∘𝑓 · 𝐴)))
frlmup.t	⊢ (𝜑 → 𝑇 ∈ LMod)
frlmup.i	⊢ (𝜑 → 𝐼 ∈ 𝑋)
frlmup.r	⊢ (𝜑 → 𝑅 = (Scalar‘𝑇))
frlmup.a	⊢ (𝜑 → 𝐴:𝐼⟶𝐶)

Assertion

Ref	Expression
frlmup1	⊢ (𝜑 → 𝐸 ∈ (𝐹 LMHom 𝑇))

Distinct variable groups:   𝑥,𝑅   𝑥,𝐼   𝑥,𝐹   𝑥,𝐵   𝑥,𝐶   𝑥, ·   𝑥,𝐴   𝑥,𝑋   𝜑,𝑥   𝑥,𝑇

Allowed substitution hint:   𝐸(𝑥)

Proof of Theorem frlmup1

Dummy variables 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frlmup.b	. 2 ⊢ 𝐵 = (Base‘𝐹)
2		eqid 2610	. 2 ⊢ ( ·𝑠 ‘𝐹) = ( ·𝑠 ‘𝐹)
3		frlmup.v	. 2 ⊢ · = ( ·𝑠 ‘𝑇)
4		eqid 2610	. 2 ⊢ (Scalar‘𝐹) = (Scalar‘𝐹)
5		eqid 2610	. 2 ⊢ (Scalar‘𝑇) = (Scalar‘𝑇)
6		eqid 2610	. 2 ⊢ (Base‘(Scalar‘𝐹)) = (Base‘(Scalar‘𝐹))
7		frlmup.r	. . . 4 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑇))
8		frlmup.t	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ LMod)
9	5	lmodring 18694	. . . . 5 ⊢ (𝑇 ∈ LMod → (Scalar‘𝑇) ∈ Ring)
10	8, 9	syl 17	. . . 4 ⊢ (𝜑 → (Scalar‘𝑇) ∈ Ring)
11	7, 10	eqeltrd 2688	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
12		frlmup.i	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑋)
13		frlmup.f	. . . 4 ⊢ 𝐹 = (𝑅 freeLMod 𝐼)
14	13	frlmlmod 19912	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) → 𝐹 ∈ LMod)
15	11, 12, 14	syl2anc 691	. 2 ⊢ (𝜑 → 𝐹 ∈ LMod)
16	13	frlmsca 19916	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) → 𝑅 = (Scalar‘𝐹))
17	11, 12, 16	syl2anc 691	. . 3 ⊢ (𝜑 → 𝑅 = (Scalar‘𝐹))
18	7, 17	eqtr3d 2646	. 2 ⊢ (𝜑 → (Scalar‘𝑇) = (Scalar‘𝐹))
19		frlmup.c	. . 3 ⊢ 𝐶 = (Base‘𝑇)
20		eqid 2610	. . 3 ⊢ (+g‘𝐹) = (+g‘𝐹)
21		eqid 2610	. . 3 ⊢ (+g‘𝑇) = (+g‘𝑇)
22		lmodgrp 18693	. . . 4 ⊢ (𝐹 ∈ LMod → 𝐹 ∈ Grp)
23	15, 22	syl 17	. . 3 ⊢ (𝜑 → 𝐹 ∈ Grp)
24		lmodgrp 18693	. . . 4 ⊢ (𝑇 ∈ LMod → 𝑇 ∈ Grp)
25	8, 24	syl 17	. . 3 ⊢ (𝜑 → 𝑇 ∈ Grp)
26		eleq1 2676	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
27	26	anbi2d 736	. . . . . 6 ⊢ (𝑧 = 𝑥 → ((𝜑 ∧ 𝑧 ∈ 𝐵) ↔ (𝜑 ∧ 𝑥 ∈ 𝐵)))
28		oveq1 6556	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ∘𝑓 · 𝐴) = (𝑥 ∘𝑓 · 𝐴))
29	28	oveq2d 6565	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑇 Σg (𝑧 ∘𝑓 · 𝐴)) = (𝑇 Σg (𝑥 ∘𝑓 · 𝐴)))
30	29	eleq1d 2672	. . . . . 6 ⊢ (𝑧 = 𝑥 → ((𝑇 Σg (𝑧 ∘𝑓 · 𝐴)) ∈ 𝐶 ↔ (𝑇 Σg (𝑥 ∘𝑓 · 𝐴)) ∈ 𝐶))
31	27, 30	imbi12d 333	. . . . 5 ⊢ (𝑧 = 𝑥 → (((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑇 Σg (𝑧 ∘𝑓 · 𝐴)) ∈ 𝐶) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑇 Σg (𝑥 ∘𝑓 · 𝐴)) ∈ 𝐶)))
32		eqid 2610	. . . . . 6 ⊢ (0g‘𝑇) = (0g‘𝑇)
33		lmodcmn 18734	. . . . . . . 8 ⊢ (𝑇 ∈ LMod → 𝑇 ∈ CMnd)
34	8, 33	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ CMnd)
35	34	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑇 ∈ CMnd)
36	12	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐼 ∈ 𝑋)
37	8	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → 𝑇 ∈ LMod)
38		simprl 790	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (Base‘𝑅))
39	7	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
40	39	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
41	38, 40	eleqtrd 2690	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (Base‘(Scalar‘𝑇)))
42		simprr 792	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶)
43		eqid 2610	. . . . . . . . 9 ⊢ (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇))
44	19, 5, 3, 43	lmodvscl 18703	. . . . . . . 8 ⊢ ((𝑇 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑦 ∈ 𝐶) → (𝑥 · 𝑦) ∈ 𝐶)
45	37, 41, 42, 44	syl3anc 1318	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → (𝑥 · 𝑦) ∈ 𝐶)
46		eqid 2610	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅)
47	13, 46, 1	frlmbasf 19923	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐵) → 𝑧:𝐼⟶(Base‘𝑅))
48	12, 47	sylan 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧:𝐼⟶(Base‘𝑅))
49		frlmup.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴:𝐼⟶𝐶)
50	49	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐴:𝐼⟶𝐶)
51		inidm 3784	. . . . . . 7 ⊢ (𝐼 ∩ 𝐼) = 𝐼
52	45, 48, 50, 36, 36, 51	off 6810	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘𝑓 · 𝐴):𝐼⟶𝐶)
53		ovex 6577	. . . . . . . 8 ⊢ (𝑧 ∘𝑓 · 𝐴) ∈ V
54	53	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘𝑓 · 𝐴) ∈ V)
55		ffun 5961	. . . . . . . 8 ⊢ ((𝑧 ∘𝑓 · 𝐴):𝐼⟶𝐶 → Fun (𝑧 ∘𝑓 · 𝐴))
56	52, 55	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → Fun (𝑧 ∘𝑓 · 𝐴))
57		fvex 6113	. . . . . . . 8 ⊢ (0g‘𝑇) ∈ V
58	57	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (0g‘𝑇) ∈ V)
59		eqid 2610	. . . . . . . . . . 11 ⊢ (0g‘𝑅) = (0g‘𝑅)
60	13, 59, 1	frlmbasfsupp 19921	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐵) → 𝑧 finSupp (0g‘𝑅))
61	12, 60	sylan 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 finSupp (0g‘𝑅))
62	7	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝜑 → (0g‘𝑅) = (0g‘(Scalar‘𝑇)))
63	62	eqcomd 2616	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘(Scalar‘𝑇)) = (0g‘𝑅))
64	63	breq2d 4595	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 finSupp (0g‘(Scalar‘𝑇)) ↔ 𝑧 finSupp (0g‘𝑅)))
65	64	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 finSupp (0g‘(Scalar‘𝑇)) ↔ 𝑧 finSupp (0g‘𝑅)))
66	61, 65	mpbird 246	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 finSupp (0g‘(Scalar‘𝑇)))
67	66	fsuppimpd 8165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 supp (0g‘(Scalar‘𝑇))) ∈ Fin)
68		ssid 3587	. . . . . . . . 9 ⊢ (𝑧 supp (0g‘(Scalar‘𝑇))) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇)))
69	68	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 supp (0g‘(Scalar‘𝑇))) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))
70	8	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑤 ∈ 𝐶) → 𝑇 ∈ LMod)
71		eqid 2610	. . . . . . . . . 10 ⊢ (0g‘(Scalar‘𝑇)) = (0g‘(Scalar‘𝑇))
72	19, 5, 3, 71, 32	lmod0vs 18719	. . . . . . . . 9 ⊢ ((𝑇 ∈ LMod ∧ 𝑤 ∈ 𝐶) → ((0g‘(Scalar‘𝑇)) · 𝑤) = (0g‘𝑇))
73	70, 72	sylancom 698	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑤 ∈ 𝐶) → ((0g‘(Scalar‘𝑇)) · 𝑤) = (0g‘𝑇))
74		fvex 6113	. . . . . . . . 9 ⊢ (0g‘(Scalar‘𝑇)) ∈ V
75	74	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (0g‘(Scalar‘𝑇)) ∈ V)
76	69, 73, 48, 50, 36, 75	suppssof1 7215	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((𝑧 ∘𝑓 · 𝐴) supp (0g‘𝑇)) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))
77		suppssfifsupp 8173	. . . . . . 7 ⊢ ((((𝑧 ∘𝑓 · 𝐴) ∈ V ∧ Fun (𝑧 ∘𝑓 · 𝐴) ∧ (0g‘𝑇) ∈ V) ∧ ((𝑧 supp (0g‘(Scalar‘𝑇))) ∈ Fin ∧ ((𝑧 ∘𝑓 · 𝐴) supp (0g‘𝑇)) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))) → (𝑧 ∘𝑓 · 𝐴) finSupp (0g‘𝑇))
78	54, 56, 58, 67, 76, 77	syl32anc 1326	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘𝑓 · 𝐴) finSupp (0g‘𝑇))
79	19, 32, 35, 36, 52, 78	gsumcl 18139	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑇 Σg (𝑧 ∘𝑓 · 𝐴)) ∈ 𝐶)
80	31, 79	chvarv 2251	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑇 Σg (𝑥 ∘𝑓 · 𝐴)) ∈ 𝐶)
81		frlmup.e	. . . 4 ⊢ 𝐸 = (𝑥 ∈ 𝐵 ↦ (𝑇 Σg (𝑥 ∘𝑓 · 𝐴)))
82	80, 81	fmptd 6292	. . 3 ⊢ (𝜑 → 𝐸:𝐵⟶𝐶)
83	34	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑇 ∈ CMnd)
84	12	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐼 ∈ 𝑋)
85		eleq1 2676	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
86	85	anbi2d 736	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝜑 ∧ 𝑧 ∈ 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐵)))
87		oveq1 6556	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ∘𝑓 · 𝐴) = (𝑦 ∘𝑓 · 𝐴))
88	87	feq1d 5943	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝑧 ∘𝑓 · 𝐴):𝐼⟶𝐶 ↔ (𝑦 ∘𝑓 · 𝐴):𝐼⟶𝐶))
89	86, 88	imbi12d 333	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘𝑓 · 𝐴):𝐼⟶𝐶) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∘𝑓 · 𝐴):𝐼⟶𝐶)))
90	89, 52	chvarv 2251	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∘𝑓 · 𝐴):𝐼⟶𝐶)
91	90	adantrr 749	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 ∘𝑓 · 𝐴):𝐼⟶𝐶)
92	52	adantrl 748	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑧 ∘𝑓 · 𝐴):𝐼⟶𝐶)
93	87	breq1d 4593	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝑧 ∘𝑓 · 𝐴) finSupp (0g‘𝑇) ↔ (𝑦 ∘𝑓 · 𝐴) finSupp (0g‘𝑇)))
94	86, 93	imbi12d 333	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘𝑓 · 𝐴) finSupp (0g‘𝑇)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∘𝑓 · 𝐴) finSupp (0g‘𝑇))))
95	94, 78	chvarv 2251	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∘𝑓 · 𝐴) finSupp (0g‘𝑇))
96	95	adantrr 749	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 ∘𝑓 · 𝐴) finSupp (0g‘𝑇))
97	78	adantrl 748	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑧 ∘𝑓 · 𝐴) finSupp (0g‘𝑇))
98	19, 32, 21, 83, 84, 91, 92, 96, 97	gsumadd 18146	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg ((𝑦 ∘𝑓 · 𝐴) ∘𝑓 (+g‘𝑇)(𝑧 ∘𝑓 · 𝐴))) = ((𝑇 Σg (𝑦 ∘𝑓 · 𝐴))(+g‘𝑇)(𝑇 Σg (𝑧 ∘𝑓 · 𝐴))))
99	1, 20	lmodvacl 18700	. . . . . . . 8 ⊢ ((𝐹 ∈ LMod ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝐹)𝑧) ∈ 𝐵)
100	99	3expb 1258	. . . . . . 7 ⊢ ((𝐹 ∈ LMod ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝐹)𝑧) ∈ 𝐵)
101	15, 100	sylan 487	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝐹)𝑧) ∈ 𝐵)
102		oveq1 6556	. . . . . . . 8 ⊢ (𝑥 = (𝑦(+g‘𝐹)𝑧) → (𝑥 ∘𝑓 · 𝐴) = ((𝑦(+g‘𝐹)𝑧) ∘𝑓 · 𝐴))
103	102	oveq2d 6565	. . . . . . 7 ⊢ (𝑥 = (𝑦(+g‘𝐹)𝑧) → (𝑇 Σg (𝑥 ∘𝑓 · 𝐴)) = (𝑇 Σg ((𝑦(+g‘𝐹)𝑧) ∘𝑓 · 𝐴)))
104		ovex 6577	. . . . . . 7 ⊢ (𝑇 Σg ((𝑦(+g‘𝐹)𝑧) ∘𝑓 · 𝐴)) ∈ V
105	103, 81, 104	fvmpt 6191	. . . . . 6 ⊢ ((𝑦(+g‘𝐹)𝑧) ∈ 𝐵 → (𝐸‘(𝑦(+g‘𝐹)𝑧)) = (𝑇 Σg ((𝑦(+g‘𝐹)𝑧) ∘𝑓 · 𝐴)))
106	101, 105	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝐸‘(𝑦(+g‘𝐹)𝑧)) = (𝑇 Σg ((𝑦(+g‘𝐹)𝑧) ∘𝑓 · 𝐴)))
107	11	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑅 ∈ Ring)
108		simprl 790	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
109		simprr 792	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧 ∈ 𝐵)
110		eqid 2610	. . . . . . . . 9 ⊢ (+g‘𝑅) = (+g‘𝑅)
111	13, 1, 107, 84, 108, 109, 110, 20	frlmplusgval 19926	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝐹)𝑧) = (𝑦 ∘𝑓 (+g‘𝑅)𝑧))
112	111	oveq1d 6564	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦(+g‘𝐹)𝑧) ∘𝑓 · 𝐴) = ((𝑦 ∘𝑓 (+g‘𝑅)𝑧) ∘𝑓 · 𝐴))
113	13, 46, 1	frlmbasf 19923	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑋 ∧ 𝑦 ∈ 𝐵) → 𝑦:𝐼⟶(Base‘𝑅))
114	12, 113	sylan 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦:𝐼⟶(Base‘𝑅))
115	114	adantrr 749	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑦:𝐼⟶(Base‘𝑅))
116		ffn 5958	. . . . . . . . . . 11 ⊢ (𝑦:𝐼⟶(Base‘𝑅) → 𝑦 Fn 𝐼)
117	115, 116	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑦 Fn 𝐼)
118	48	adantrl 748	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧:𝐼⟶(Base‘𝑅))
119		ffn 5958	. . . . . . . . . . 11 ⊢ (𝑧:𝐼⟶(Base‘𝑅) → 𝑧 Fn 𝐼)
120	118, 119	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧 Fn 𝐼)
121	117, 120, 84, 84, 51	offn 6806	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 ∘𝑓 (+g‘𝑅)𝑧) Fn 𝐼)
122		ffn 5958	. . . . . . . . . . 11 ⊢ (𝐴:𝐼⟶𝐶 → 𝐴 Fn 𝐼)
123	49, 122	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 Fn 𝐼)
124	123	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐴 Fn 𝐼)
125	121, 124, 84, 84, 51	offn 6806	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦 ∘𝑓 (+g‘𝑅)𝑧) ∘𝑓 · 𝐴) Fn 𝐼)
126		ffn 5958	. . . . . . . . . . 11 ⊢ ((𝑦 ∘𝑓 · 𝐴):𝐼⟶𝐶 → (𝑦 ∘𝑓 · 𝐴) Fn 𝐼)
127	90, 126	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∘𝑓 · 𝐴) Fn 𝐼)
128	127	adantrr 749	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 ∘𝑓 · 𝐴) Fn 𝐼)
129		ffn 5958	. . . . . . . . . . 11 ⊢ ((𝑧 ∘𝑓 · 𝐴):𝐼⟶𝐶 → (𝑧 ∘𝑓 · 𝐴) Fn 𝐼)
130	52, 129	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘𝑓 · 𝐴) Fn 𝐼)
131	130	adantrl 748	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑧 ∘𝑓 · 𝐴) Fn 𝐼)
132	128, 131, 84, 84, 51	offn 6806	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦 ∘𝑓 · 𝐴) ∘𝑓 (+g‘𝑇)(𝑧 ∘𝑓 · 𝐴)) Fn 𝐼)
133	7	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+g‘𝑅) = (+g‘(Scalar‘𝑇)))
134	133	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (+g‘𝑅) = (+g‘(Scalar‘𝑇)))
135	134	oveqd 6566	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥)) = ((𝑦‘𝑥)(+g‘(Scalar‘𝑇))(𝑧‘𝑥)))
136	135	oveq1d 6564	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)) = (((𝑦‘𝑥)(+g‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥)))
137	8	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ LMod)
138	115	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) ∈ (Base‘𝑅))
139	39	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
140	138, 139	eleqtrd 2690	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) ∈ (Base‘(Scalar‘𝑇)))
141	118	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑧‘𝑥) ∈ (Base‘𝑅))
142	141, 139	eleqtrd 2690	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑧‘𝑥) ∈ (Base‘(Scalar‘𝑇)))
143	49	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐴:𝐼⟶𝐶)
144	143	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝐴‘𝑥) ∈ 𝐶)
145		eqid 2610	. . . . . . . . . . . . 13 ⊢ (+g‘(Scalar‘𝑇)) = (+g‘(Scalar‘𝑇))
146	19, 21, 5, 3, 43, 145	lmodvsdir 18710	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ LMod ∧ ((𝑦‘𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝑧‘𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐴‘𝑥) ∈ 𝐶)) → (((𝑦‘𝑥)(+g‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥)) = (((𝑦‘𝑥) · (𝐴‘𝑥))(+g‘𝑇)((𝑧‘𝑥) · (𝐴‘𝑥))))
147	137, 140, 142, 144, 146	syl13anc 1320	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦‘𝑥)(+g‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥)) = (((𝑦‘𝑥) · (𝐴‘𝑥))(+g‘𝑇)((𝑧‘𝑥) · (𝐴‘𝑥))))
148	136, 147	eqtrd 2644	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)) = (((𝑦‘𝑥) · (𝐴‘𝑥))(+g‘𝑇)((𝑧‘𝑥) · (𝐴‘𝑥))))
149	117	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑦 Fn 𝐼)
150	120	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑧 Fn 𝐼)
151	12	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑋)
152		simpr 476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
153		fnfvof 6809	. . . . . . . . . . . 12 ⊢ (((𝑦 Fn 𝐼 ∧ 𝑧 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → ((𝑦 ∘𝑓 (+g‘𝑅)𝑧)‘𝑥) = ((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥)))
154	149, 150, 151, 152, 153	syl22anc 1319	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∘𝑓 (+g‘𝑅)𝑧)‘𝑥) = ((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥)))
155	154	oveq1d 6564	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘𝑓 (+g‘𝑅)𝑧)‘𝑥) · (𝐴‘𝑥)) = (((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)))
156	123	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝐴 Fn 𝐼)
157		fnfvof 6809	. . . . . . . . . . . 12 ⊢ (((𝑦 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → ((𝑦 ∘𝑓 · 𝐴)‘𝑥) = ((𝑦‘𝑥) · (𝐴‘𝑥)))
158	149, 156, 151, 152, 157	syl22anc 1319	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∘𝑓 · 𝐴)‘𝑥) = ((𝑦‘𝑥) · (𝐴‘𝑥)))
159		fnfvof 6809	. . . . . . . . . . . 12 ⊢ (((𝑧 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → ((𝑧 ∘𝑓 · 𝐴)‘𝑥) = ((𝑧‘𝑥) · (𝐴‘𝑥)))
160	150, 156, 151, 152, 159	syl22anc 1319	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∘𝑓 · 𝐴)‘𝑥) = ((𝑧‘𝑥) · (𝐴‘𝑥)))
161	158, 160	oveq12d 6567	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘𝑓 · 𝐴)‘𝑥)(+g‘𝑇)((𝑧 ∘𝑓 · 𝐴)‘𝑥)) = (((𝑦‘𝑥) · (𝐴‘𝑥))(+g‘𝑇)((𝑧‘𝑥) · (𝐴‘𝑥))))
162	148, 155, 161	3eqtr4d 2654	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘𝑓 (+g‘𝑅)𝑧)‘𝑥) · (𝐴‘𝑥)) = (((𝑦 ∘𝑓 · 𝐴)‘𝑥)(+g‘𝑇)((𝑧 ∘𝑓 · 𝐴)‘𝑥)))
163	121	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∘𝑓 (+g‘𝑅)𝑧) Fn 𝐼)
164		fnfvof 6809	. . . . . . . . . 10 ⊢ ((((𝑦 ∘𝑓 (+g‘𝑅)𝑧) Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → (((𝑦 ∘𝑓 (+g‘𝑅)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦 ∘𝑓 (+g‘𝑅)𝑧)‘𝑥) · (𝐴‘𝑥)))
165	163, 156, 151, 152, 164	syl22anc 1319	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘𝑓 (+g‘𝑅)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦 ∘𝑓 (+g‘𝑅)𝑧)‘𝑥) · (𝐴‘𝑥)))
166	128	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∘𝑓 · 𝐴) Fn 𝐼)
167	131	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑧 ∘𝑓 · 𝐴) Fn 𝐼)
168		fnfvof 6809	. . . . . . . . . 10 ⊢ ((((𝑦 ∘𝑓 · 𝐴) Fn 𝐼 ∧ (𝑧 ∘𝑓 · 𝐴) Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → (((𝑦 ∘𝑓 · 𝐴) ∘𝑓 (+g‘𝑇)(𝑧 ∘𝑓 · 𝐴))‘𝑥) = (((𝑦 ∘𝑓 · 𝐴)‘𝑥)(+g‘𝑇)((𝑧 ∘𝑓 · 𝐴)‘𝑥)))
169	166, 167, 151, 152, 168	syl22anc 1319	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘𝑓 · 𝐴) ∘𝑓 (+g‘𝑇)(𝑧 ∘𝑓 · 𝐴))‘𝑥) = (((𝑦 ∘𝑓 · 𝐴)‘𝑥)(+g‘𝑇)((𝑧 ∘𝑓 · 𝐴)‘𝑥)))
170	162, 165, 169	3eqtr4d 2654	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘𝑓 (+g‘𝑅)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦 ∘𝑓 · 𝐴) ∘𝑓 (+g‘𝑇)(𝑧 ∘𝑓 · 𝐴))‘𝑥))
171	125, 132, 170	eqfnfvd 6222	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦 ∘𝑓 (+g‘𝑅)𝑧) ∘𝑓 · 𝐴) = ((𝑦 ∘𝑓 · 𝐴) ∘𝑓 (+g‘𝑇)(𝑧 ∘𝑓 · 𝐴)))
172	112, 171	eqtrd 2644	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦(+g‘𝐹)𝑧) ∘𝑓 · 𝐴) = ((𝑦 ∘𝑓 · 𝐴) ∘𝑓 (+g‘𝑇)(𝑧 ∘𝑓 · 𝐴)))
173	172	oveq2d 6565	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg ((𝑦(+g‘𝐹)𝑧) ∘𝑓 · 𝐴)) = (𝑇 Σg ((𝑦 ∘𝑓 · 𝐴) ∘𝑓 (+g‘𝑇)(𝑧 ∘𝑓 · 𝐴))))
174	106, 173	eqtrd 2644	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝐸‘(𝑦(+g‘𝐹)𝑧)) = (𝑇 Σg ((𝑦 ∘𝑓 · 𝐴) ∘𝑓 (+g‘𝑇)(𝑧 ∘𝑓 · 𝐴))))
175		oveq1 6556	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∘𝑓 · 𝐴) = (𝑦 ∘𝑓 · 𝐴))
176	175	oveq2d 6565	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑇 Σg (𝑥 ∘𝑓 · 𝐴)) = (𝑇 Σg (𝑦 ∘𝑓 · 𝐴)))
177		ovex 6577	. . . . . . 7 ⊢ (𝑇 Σg (𝑦 ∘𝑓 · 𝐴)) ∈ V
178	176, 81, 177	fvmpt 6191	. . . . . 6 ⊢ (𝑦 ∈ 𝐵 → (𝐸‘𝑦) = (𝑇 Σg (𝑦 ∘𝑓 · 𝐴)))
179	178	ad2antrl 760	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝐸‘𝑦) = (𝑇 Σg (𝑦 ∘𝑓 · 𝐴)))
180		oveq1 6556	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∘𝑓 · 𝐴) = (𝑧 ∘𝑓 · 𝐴))
181	180	oveq2d 6565	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑇 Σg (𝑥 ∘𝑓 · 𝐴)) = (𝑇 Σg (𝑧 ∘𝑓 · 𝐴)))
182		ovex 6577	. . . . . . 7 ⊢ (𝑇 Σg (𝑧 ∘𝑓 · 𝐴)) ∈ V
183	181, 81, 182	fvmpt 6191	. . . . . 6 ⊢ (𝑧 ∈ 𝐵 → (𝐸‘𝑧) = (𝑇 Σg (𝑧 ∘𝑓 · 𝐴)))
184	183	ad2antll 761	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝐸‘𝑧) = (𝑇 Σg (𝑧 ∘𝑓 · 𝐴)))
185	179, 184	oveq12d 6567	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝐸‘𝑦)(+g‘𝑇)(𝐸‘𝑧)) = ((𝑇 Σg (𝑦 ∘𝑓 · 𝐴))(+g‘𝑇)(𝑇 Σg (𝑧 ∘𝑓 · 𝐴))))
186	98, 174, 185	3eqtr4d 2654	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝐸‘(𝑦(+g‘𝐹)𝑧)) = ((𝐸‘𝑦)(+g‘𝑇)(𝐸‘𝑧)))
187	1, 19, 20, 21, 23, 25, 82, 186	isghmd 17492	. 2 ⊢ (𝜑 → 𝐸 ∈ (𝐹 GrpHom 𝑇))
188	8	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝑇 ∈ LMod)
189	12	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝐼 ∈ 𝑋)
190	18	fveq2d 6107	. . . . . . . 8 ⊢ (𝜑 → (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝐹)))
191	190	eleq2d 2673	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ (Base‘(Scalar‘𝑇)) ↔ 𝑦 ∈ (Base‘(Scalar‘𝐹))))
192	191	biimpar 501	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(Scalar‘𝐹))) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
193	192	adantrr 749	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
194	52	adantrl 748	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑧 ∘𝑓 · 𝐴):𝐼⟶𝐶)
195	194	ffvelrnda 6267	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∘𝑓 · 𝐴)‘𝑥) ∈ 𝐶)
196	52	feqmptd 6159	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘𝑓 · 𝐴) = (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘𝑓 · 𝐴)‘𝑥)))
197	196, 78	eqbrtrrd 4607	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘𝑓 · 𝐴)‘𝑥)) finSupp (0g‘𝑇))
198	197	adantrl 748	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘𝑓 · 𝐴)‘𝑥)) finSupp (0g‘𝑇))
199	19, 5, 43, 32, 21, 3, 188, 189, 193, 195, 198	gsumvsmul 18750	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (𝑦 · ((𝑧 ∘𝑓 · 𝐴)‘𝑥)))) = (𝑦 · (𝑇 Σg (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘𝑓 · 𝐴)‘𝑥)))))
200	15	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝐹 ∈ LMod)
201		simprl 790	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝑦 ∈ (Base‘(Scalar‘𝐹)))
202		simprr 792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝑧 ∈ 𝐵)
203	1, 4, 2, 6	lmodvscl 18703	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ LMod ∧ 𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵) → (𝑦( ·𝑠 ‘𝐹)𝑧) ∈ 𝐵)
204	200, 201, 202, 203	syl3anc 1318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑦( ·𝑠 ‘𝐹)𝑧) ∈ 𝐵)
205	13, 46, 1	frlmbasf 19923	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑋 ∧ (𝑦( ·𝑠 ‘𝐹)𝑧) ∈ 𝐵) → (𝑦( ·𝑠 ‘𝐹)𝑧):𝐼⟶(Base‘𝑅))
206	189, 204, 205	syl2anc 691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑦( ·𝑠 ‘𝐹)𝑧):𝐼⟶(Base‘𝑅))
207		ffn 5958	. . . . . . . . . 10 ⊢ ((𝑦( ·𝑠 ‘𝐹)𝑧):𝐼⟶(Base‘𝑅) → (𝑦( ·𝑠 ‘𝐹)𝑧) Fn 𝐼)
208	206, 207	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑦( ·𝑠 ‘𝐹)𝑧) Fn 𝐼)
209	123	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝐴 Fn 𝐼)
210	208, 209, 189, 189, 51	offn 6806	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴) Fn 𝐼)
211		dffn2 5960	. . . . . . . 8 ⊢ (((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴) Fn 𝐼 ↔ ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴):𝐼⟶V)
212	210, 211	sylib 207	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴):𝐼⟶V)
213	212	feqmptd 6159	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴) = (𝑥 ∈ 𝐼 ↦ (((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥)))
214	7	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝜑 → (.r‘𝑅) = (.r‘(Scalar‘𝑇)))
215	214	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (.r‘𝑅) = (.r‘(Scalar‘𝑇)))
216	215	oveqd 6566	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦(.r‘𝑅)(𝑧‘𝑥)) = (𝑦(.r‘(Scalar‘𝑇))(𝑧‘𝑥)))
217	216	oveq1d 6564	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦(.r‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)) = ((𝑦(.r‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥)))
218	8	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ LMod)
219		simplrl 796	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑦 ∈ (Base‘(Scalar‘𝐹)))
220	190	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝐹)))
221	219, 220	eleqtrrd 2691	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
222	48	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑧‘𝑥) ∈ (Base‘𝑅))
223	39	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
224	222, 223	eleqtrd 2690	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑧‘𝑥) ∈ (Base‘(Scalar‘𝑇)))
225	224	adantlrl 752	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑧‘𝑥) ∈ (Base‘(Scalar‘𝑇)))
226	49	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐴‘𝑥) ∈ 𝐶)
227	226	adantlr 747	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝐴‘𝑥) ∈ 𝐶)
228		eqid 2610	. . . . . . . . . . 11 ⊢ (.r‘(Scalar‘𝑇)) = (.r‘(Scalar‘𝑇))
229	19, 5, 3, 43, 228	lmodvsass 18711	. . . . . . . . . 10 ⊢ ((𝑇 ∈ LMod ∧ (𝑦 ∈ (Base‘(Scalar‘𝑇)) ∧ (𝑧‘𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐴‘𝑥) ∈ 𝐶)) → ((𝑦(.r‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥)) = (𝑦 · ((𝑧‘𝑥) · (𝐴‘𝑥))))
230	218, 221, 225, 227, 229	syl13anc 1320	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦(.r‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥)) = (𝑦 · ((𝑧‘𝑥) · (𝐴‘𝑥))))
231	217, 230	eqtrd 2644	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦(.r‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)) = (𝑦 · ((𝑧‘𝑥) · (𝐴‘𝑥))))
232	208	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦( ·𝑠 ‘𝐹)𝑧) Fn 𝐼)
233	123	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝐴 Fn 𝐼)
234	12	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑋)
235		simpr 476	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
236		fnfvof 6809	. . . . . . . . . 10 ⊢ ((((𝑦( ·𝑠 ‘𝐹)𝑧) Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → (((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦( ·𝑠 ‘𝐹)𝑧)‘𝑥) · (𝐴‘𝑥)))
237	232, 233, 234, 235, 236	syl22anc 1319	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦( ·𝑠 ‘𝐹)𝑧)‘𝑥) · (𝐴‘𝑥)))
238	17	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝐹)))
239	238	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝐹)))
240	219, 239	eleqtrrd 2691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑦 ∈ (Base‘𝑅))
241		simplrr 797	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑧 ∈ 𝐵)
242		eqid 2610	. . . . . . . . . . 11 ⊢ (.r‘𝑅) = (.r‘𝑅)
243	13, 1, 46, 234, 240, 241, 235, 2, 242	frlmvscaval 19929	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦( ·𝑠 ‘𝐹)𝑧)‘𝑥) = (𝑦(.r‘𝑅)(𝑧‘𝑥)))
244	243	oveq1d 6564	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦( ·𝑠 ‘𝐹)𝑧)‘𝑥) · (𝐴‘𝑥)) = ((𝑦(.r‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)))
245	237, 244	eqtrd 2644	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = ((𝑦(.r‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)))
246	48, 119	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 Fn 𝐼)
247	246	adantrl 748	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝑧 Fn 𝐼)
248	247	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑧 Fn 𝐼)
249	248, 233, 234, 235, 159	syl22anc 1319	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∘𝑓 · 𝐴)‘𝑥) = ((𝑧‘𝑥) · (𝐴‘𝑥)))
250	249	oveq2d 6565	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦 · ((𝑧 ∘𝑓 · 𝐴)‘𝑥)) = (𝑦 · ((𝑧‘𝑥) · (𝐴‘𝑥))))
251	231, 245, 250	3eqtr4d 2654	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (𝑦 · ((𝑧 ∘𝑓 · 𝐴)‘𝑥)))
252	251	mpteq2dva 4672	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ (((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥)) = (𝑥 ∈ 𝐼 ↦ (𝑦 · ((𝑧 ∘𝑓 · 𝐴)‘𝑥))))
253	213, 252	eqtrd 2644	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴) = (𝑥 ∈ 𝐼 ↦ (𝑦 · ((𝑧 ∘𝑓 · 𝐴)‘𝑥))))
254	253	oveq2d 6565	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (𝑦 · ((𝑧 ∘𝑓 · 𝐴)‘𝑥)))))
255	194	feqmptd 6159	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑧 ∘𝑓 · 𝐴) = (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘𝑓 · 𝐴)‘𝑥)))
256	255	oveq2d 6565	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg (𝑧 ∘𝑓 · 𝐴)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘𝑓 · 𝐴)‘𝑥))))
257	256	oveq2d 6565	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑦 · (𝑇 Σg (𝑧 ∘𝑓 · 𝐴))) = (𝑦 · (𝑇 Σg (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘𝑓 · 𝐴)‘𝑥)))))
258	199, 254, 257	3eqtr4d 2654	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)) = (𝑦 · (𝑇 Σg (𝑧 ∘𝑓 · 𝐴))))
259		oveq1 6556	. . . . . 6 ⊢ (𝑥 = (𝑦( ·𝑠 ‘𝐹)𝑧) → (𝑥 ∘𝑓 · 𝐴) = ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴))
260	259	oveq2d 6565	. . . . 5 ⊢ (𝑥 = (𝑦( ·𝑠 ‘𝐹)𝑧) → (𝑇 Σg (𝑥 ∘𝑓 · 𝐴)) = (𝑇 Σg ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)))
261		ovex 6577	. . . . 5 ⊢ (𝑇 Σg ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)) ∈ V
262	260, 81, 261	fvmpt 6191	. . . 4 ⊢ ((𝑦( ·𝑠 ‘𝐹)𝑧) ∈ 𝐵 → (𝐸‘(𝑦( ·𝑠 ‘𝐹)𝑧)) = (𝑇 Σg ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)))
263	204, 262	syl 17	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝐸‘(𝑦( ·𝑠 ‘𝐹)𝑧)) = (𝑇 Σg ((𝑦( ·𝑠 ‘𝐹)𝑧) ∘𝑓 · 𝐴)))
264	183	oveq2d 6565	. . . 4 ⊢ (𝑧 ∈ 𝐵 → (𝑦 · (𝐸‘𝑧)) = (𝑦 · (𝑇 Σg (𝑧 ∘𝑓 · 𝐴))))
265	264	ad2antll 761	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑦 · (𝐸‘𝑧)) = (𝑦 · (𝑇 Σg (𝑧 ∘𝑓 · 𝐴))))
266	258, 263, 265	3eqtr4d 2654	. 2 ⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝐸‘(𝑦( ·𝑠 ‘𝐹)𝑧)) = (𝑦 · (𝐸‘𝑧)))
267	1, 2, 3, 4, 5, 6, 15, 8, 18, 187, 266	islmhmd 18860	1 ⊢ (𝜑 → 𝐸 ∈ (𝐹 LMHom 𝑇))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540   class class class wbr 4583   ↦ cmpt 4643  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘_𝑓 cof 6793   supp csupp 7182  Fincfn 7841   finSupp cfsupp 8158  Basecbs 15695  +_gcplusg 15768  ._rcmulr 15769  Scalarcsca 15771   ·_𝑠 cvsca 15772  0_gc0g 15923   Σ_g cgsu 15924  Grpcgrp 17245  CMndccmn 18016  Ringcrg 18370  LModclmod 18686   LMHom clmhm 18840   freeLMod cfrlm 19909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-sup 8231  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-hom 15793  df-cco 15794  df-0g 15925  df-gsum 15926  df-prds 15931  df-pws 15933  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mhm 17158  df-submnd 17159  df-grp 17248  df-minusg 17249  df-sbg 17250  df-subg 17414  df-ghm 17481  df-cntz 17573  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-subrg 18601  df-lmod 18688  df-lss 18754  df-lmhm 18843  df-sra 18993  df-rgmod 18994  df-dsmm 19895  df-frlm 19910

This theorem is referenced by:  frlmup3  19958  frlmup4  19959  islindf5  19997  indlcim  19998  lnrfg  36708