Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  frlmup1 Structured version   Visualization version   GIF version

Theorem frlmup1 20564
 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 (𝑥f · 𝐴)))
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.
StepHypRef Expression
1 frlmup.b . 2 𝐵 = (Base‘𝐹)
2 eqid 2759 . 2 ( ·𝑠𝐹) = ( ·𝑠𝐹)
3 frlmup.v . 2 · = ( ·𝑠𝑇)
4 eqid 2759 . 2 (Scalar‘𝐹) = (Scalar‘𝐹)
5 eqid 2759 . 2 (Scalar‘𝑇) = (Scalar‘𝑇)
6 eqid 2759 . 2 (Base‘(Scalar‘𝐹)) = (Base‘(Scalar‘𝐹))
7 frlmup.r . . . 4 (𝜑𝑅 = (Scalar‘𝑇))
8 frlmup.t . . . . 5 (𝜑𝑇 ∈ LMod)
95lmodring 19711 . . . . 5 (𝑇 ∈ LMod → (Scalar‘𝑇) ∈ Ring)
108, 9syl 17 . . . 4 (𝜑 → (Scalar‘𝑇) ∈ Ring)
117, 10eqeltrd 2853 . . 3 (𝜑𝑅 ∈ Ring)
12 frlmup.i . . 3 (𝜑𝐼𝑋)
13 frlmup.f . . . 4 𝐹 = (𝑅 freeLMod 𝐼)
1413frlmlmod 20515 . . 3 ((𝑅 ∈ Ring ∧ 𝐼𝑋) → 𝐹 ∈ LMod)
1511, 12, 14syl2anc 588 . 2 (𝜑𝐹 ∈ LMod)
1613frlmsca 20519 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼𝑋) → 𝑅 = (Scalar‘𝐹))
1711, 12, 16syl2anc 588 . . 3 (𝜑𝑅 = (Scalar‘𝐹))
187, 17eqtr3d 2796 . 2 (𝜑 → (Scalar‘𝑇) = (Scalar‘𝐹))
19 frlmup.c . . 3 𝐶 = (Base‘𝑇)
20 eqid 2759 . . 3 (+g𝐹) = (+g𝐹)
21 eqid 2759 . . 3 (+g𝑇) = (+g𝑇)
22 lmodgrp 19710 . . . 4 (𝐹 ∈ LMod → 𝐹 ∈ Grp)
2315, 22syl 17 . . 3 (𝜑𝐹 ∈ Grp)
24 lmodgrp 19710 . . . 4 (𝑇 ∈ LMod → 𝑇 ∈ Grp)
258, 24syl 17 . . 3 (𝜑𝑇 ∈ Grp)
26 eleq1w 2835 . . . . . . 7 (𝑧 = 𝑥 → (𝑧𝐵𝑥𝐵))
2726anbi2d 632 . . . . . 6 (𝑧 = 𝑥 → ((𝜑𝑧𝐵) ↔ (𝜑𝑥𝐵)))
28 oveq1 7158 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧f · 𝐴) = (𝑥f · 𝐴))
2928oveq2d 7167 . . . . . . 7 (𝑧 = 𝑥 → (𝑇 Σg (𝑧f · 𝐴)) = (𝑇 Σg (𝑥f · 𝐴)))
3029eleq1d 2837 . . . . . 6 (𝑧 = 𝑥 → ((𝑇 Σg (𝑧f · 𝐴)) ∈ 𝐶 ↔ (𝑇 Σg (𝑥f · 𝐴)) ∈ 𝐶))
3127, 30imbi12d 349 . . . . 5 (𝑧 = 𝑥 → (((𝜑𝑧𝐵) → (𝑇 Σg (𝑧f · 𝐴)) ∈ 𝐶) ↔ ((𝜑𝑥𝐵) → (𝑇 Σg (𝑥f · 𝐴)) ∈ 𝐶)))
32 eqid 2759 . . . . . 6 (0g𝑇) = (0g𝑇)
33 lmodcmn 19751 . . . . . . . 8 (𝑇 ∈ LMod → 𝑇 ∈ CMnd)
348, 33syl 17 . . . . . . 7 (𝜑𝑇 ∈ CMnd)
3534adantr 485 . . . . . 6 ((𝜑𝑧𝐵) → 𝑇 ∈ CMnd)
3612adantr 485 . . . . . 6 ((𝜑𝑧𝐵) → 𝐼𝑋)
378ad2antrr 726 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑇 ∈ LMod)
38 simprl 771 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑥 ∈ (Base‘𝑅))
397fveq2d 6663 . . . . . . . . . 10 (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
4039ad2antrr 726 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
4138, 40eleqtrd 2855 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑥 ∈ (Base‘(Scalar‘𝑇)))
42 simprr 773 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑦𝐶)
43 eqid 2759 . . . . . . . . 9 (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇))
4419, 5, 3, 43lmodvscl 19720 . . . . . . . 8 ((𝑇 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑦𝐶) → (𝑥 · 𝑦) ∈ 𝐶)
4537, 41, 42, 44syl3anc 1369 . . . . . . 7 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → (𝑥 · 𝑦) ∈ 𝐶)
46 eqid 2759 . . . . . . . . 9 (Base‘𝑅) = (Base‘𝑅)
4713, 46, 1frlmbasf 20526 . . . . . . . 8 ((𝐼𝑋𝑧𝐵) → 𝑧:𝐼⟶(Base‘𝑅))
4812, 47sylan 584 . . . . . . 7 ((𝜑𝑧𝐵) → 𝑧:𝐼⟶(Base‘𝑅))
49 frlmup.a . . . . . . . 8 (𝜑𝐴:𝐼𝐶)
5049adantr 485 . . . . . . 7 ((𝜑𝑧𝐵) → 𝐴:𝐼𝐶)
51 inidm 4124 . . . . . . 7 (𝐼𝐼) = 𝐼
5245, 48, 50, 36, 36, 51off 7423 . . . . . 6 ((𝜑𝑧𝐵) → (𝑧f · 𝐴):𝐼𝐶)
53 ovexd 7186 . . . . . . 7 ((𝜑𝑧𝐵) → (𝑧f · 𝐴) ∈ V)
5452ffund 6503 . . . . . . 7 ((𝜑𝑧𝐵) → Fun (𝑧f · 𝐴))
55 fvexd 6674 . . . . . . 7 ((𝜑𝑧𝐵) → (0g𝑇) ∈ V)
56 eqid 2759 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
5713, 56, 1frlmbasfsupp 20524 . . . . . . . . . 10 ((𝐼𝑋𝑧𝐵) → 𝑧 finSupp (0g𝑅))
5812, 57sylan 584 . . . . . . . . 9 ((𝜑𝑧𝐵) → 𝑧 finSupp (0g𝑅))
597fveq2d 6663 . . . . . . . . . . . 12 (𝜑 → (0g𝑅) = (0g‘(Scalar‘𝑇)))
6059eqcomd 2765 . . . . . . . . . . 11 (𝜑 → (0g‘(Scalar‘𝑇)) = (0g𝑅))
6160breq2d 5045 . . . . . . . . . 10 (𝜑 → (𝑧 finSupp (0g‘(Scalar‘𝑇)) ↔ 𝑧 finSupp (0g𝑅)))
6261adantr 485 . . . . . . . . 9 ((𝜑𝑧𝐵) → (𝑧 finSupp (0g‘(Scalar‘𝑇)) ↔ 𝑧 finSupp (0g𝑅)))
6358, 62mpbird 260 . . . . . . . 8 ((𝜑𝑧𝐵) → 𝑧 finSupp (0g‘(Scalar‘𝑇)))
6463fsuppimpd 8874 . . . . . . 7 ((𝜑𝑧𝐵) → (𝑧 supp (0g‘(Scalar‘𝑇))) ∈ Fin)
65 ssidd 3916 . . . . . . . 8 ((𝜑𝑧𝐵) → (𝑧 supp (0g‘(Scalar‘𝑇))) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))
668ad2antrr 726 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ 𝑤𝐶) → 𝑇 ∈ LMod)
67 eqid 2759 . . . . . . . . . 10 (0g‘(Scalar‘𝑇)) = (0g‘(Scalar‘𝑇))
6819, 5, 3, 67, 32lmod0vs 19736 . . . . . . . . 9 ((𝑇 ∈ LMod ∧ 𝑤𝐶) → ((0g‘(Scalar‘𝑇)) · 𝑤) = (0g𝑇))
6966, 68sylancom 592 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ 𝑤𝐶) → ((0g‘(Scalar‘𝑇)) · 𝑤) = (0g𝑇))
70 fvexd 6674 . . . . . . . 8 ((𝜑𝑧𝐵) → (0g‘(Scalar‘𝑇)) ∈ V)
7165, 69, 48, 50, 36, 70suppssof1 7874 . . . . . . 7 ((𝜑𝑧𝐵) → ((𝑧f · 𝐴) supp (0g𝑇)) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))
72 suppssfifsupp 8882 . . . . . . 7 ((((𝑧f · 𝐴) ∈ V ∧ Fun (𝑧f · 𝐴) ∧ (0g𝑇) ∈ V) ∧ ((𝑧 supp (0g‘(Scalar‘𝑇))) ∈ Fin ∧ ((𝑧f · 𝐴) supp (0g𝑇)) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))) → (𝑧f · 𝐴) finSupp (0g𝑇))
7353, 54, 55, 64, 71, 72syl32anc 1376 . . . . . 6 ((𝜑𝑧𝐵) → (𝑧f · 𝐴) finSupp (0g𝑇))
7419, 32, 35, 36, 52, 73gsumcl 19104 . . . . 5 ((𝜑𝑧𝐵) → (𝑇 Σg (𝑧f · 𝐴)) ∈ 𝐶)
7531, 74chvarvv 2006 . . . 4 ((𝜑𝑥𝐵) → (𝑇 Σg (𝑥f · 𝐴)) ∈ 𝐶)
76 frlmup.e . . . 4 𝐸 = (𝑥𝐵 ↦ (𝑇 Σg (𝑥f · 𝐴)))
7775, 76fmptd 6870 . . 3 (𝜑𝐸:𝐵𝐶)
7834adantr 485 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑇 ∈ CMnd)
7912adantr 485 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝐼𝑋)
80 eleq1w 2835 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧𝐵𝑦𝐵))
8180anbi2d 632 . . . . . . . 8 (𝑧 = 𝑦 → ((𝜑𝑧𝐵) ↔ (𝜑𝑦𝐵)))
82 oveq1 7158 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧f · 𝐴) = (𝑦f · 𝐴))
8382feq1d 6484 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧f · 𝐴):𝐼𝐶 ↔ (𝑦f · 𝐴):𝐼𝐶))
8481, 83imbi12d 349 . . . . . . 7 (𝑧 = 𝑦 → (((𝜑𝑧𝐵) → (𝑧f · 𝐴):𝐼𝐶) ↔ ((𝜑𝑦𝐵) → (𝑦f · 𝐴):𝐼𝐶)))
8584, 52chvarvv 2006 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦f · 𝐴):𝐼𝐶)
8685adantrr 717 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦f · 𝐴):𝐼𝐶)
8752adantrl 716 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑧f · 𝐴):𝐼𝐶)
8882breq1d 5043 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧f · 𝐴) finSupp (0g𝑇) ↔ (𝑦f · 𝐴) finSupp (0g𝑇)))
8981, 88imbi12d 349 . . . . . . 7 (𝑧 = 𝑦 → (((𝜑𝑧𝐵) → (𝑧f · 𝐴) finSupp (0g𝑇)) ↔ ((𝜑𝑦𝐵) → (𝑦f · 𝐴) finSupp (0g𝑇))))
9089, 73chvarvv 2006 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦f · 𝐴) finSupp (0g𝑇))
9190adantrr 717 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦f · 𝐴) finSupp (0g𝑇))
9273adantrl 716 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑧f · 𝐴) finSupp (0g𝑇))
9319, 32, 21, 78, 79, 86, 87, 91, 92gsumadd 19112 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑇 Σg ((𝑦f · 𝐴) ∘f (+g𝑇)(𝑧f · 𝐴))) = ((𝑇 Σg (𝑦f · 𝐴))(+g𝑇)(𝑇 Σg (𝑧f · 𝐴))))
941, 20lmodvacl 19717 . . . . . . . 8 ((𝐹 ∈ LMod ∧ 𝑦𝐵𝑧𝐵) → (𝑦(+g𝐹)𝑧) ∈ 𝐵)
95943expb 1118 . . . . . . 7 ((𝐹 ∈ LMod ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(+g𝐹)𝑧) ∈ 𝐵)
9615, 95sylan 584 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(+g𝐹)𝑧) ∈ 𝐵)
97 oveq1 7158 . . . . . . . 8 (𝑥 = (𝑦(+g𝐹)𝑧) → (𝑥f · 𝐴) = ((𝑦(+g𝐹)𝑧) ∘f · 𝐴))
9897oveq2d 7167 . . . . . . 7 (𝑥 = (𝑦(+g𝐹)𝑧) → (𝑇 Σg (𝑥f · 𝐴)) = (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘f · 𝐴)))
99 ovex 7184 . . . . . . 7 (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘f · 𝐴)) ∈ V
10098, 76, 99fvmpt 6760 . . . . . 6 ((𝑦(+g𝐹)𝑧) ∈ 𝐵 → (𝐸‘(𝑦(+g𝐹)𝑧)) = (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘f · 𝐴)))
10196, 100syl 17 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸‘(𝑦(+g𝐹)𝑧)) = (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘f · 𝐴)))
10211adantr 485 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑅 ∈ Ring)
103 simprl 771 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑦𝐵)
104 simprr 773 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑧𝐵)
105 eqid 2759 . . . . . . . . 9 (+g𝑅) = (+g𝑅)
10613, 1, 102, 79, 103, 104, 105, 20frlmplusgval 20530 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(+g𝐹)𝑧) = (𝑦f (+g𝑅)𝑧))
107106oveq1d 7166 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦(+g𝐹)𝑧) ∘f · 𝐴) = ((𝑦f (+g𝑅)𝑧) ∘f · 𝐴))
10813, 46, 1frlmbasf 20526 . . . . . . . . . . . . 13 ((𝐼𝑋𝑦𝐵) → 𝑦:𝐼⟶(Base‘𝑅))
10912, 108sylan 584 . . . . . . . . . . . 12 ((𝜑𝑦𝐵) → 𝑦:𝐼⟶(Base‘𝑅))
110109adantrr 717 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑦:𝐼⟶(Base‘𝑅))
111110ffnd 6500 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑦 Fn 𝐼)
11248adantrl 716 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑧:𝐼⟶(Base‘𝑅))
113112ffnd 6500 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑧 Fn 𝐼)
114111, 113, 79, 79, 51offn 7418 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦f (+g𝑅)𝑧) Fn 𝐼)
11549ffnd 6500 . . . . . . . . . 10 (𝜑𝐴 Fn 𝐼)
116115adantr 485 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝐴 Fn 𝐼)
117114, 116, 79, 79, 51offn 7418 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦f (+g𝑅)𝑧) ∘f · 𝐴) Fn 𝐼)
11885ffnd 6500 . . . . . . . . . 10 ((𝜑𝑦𝐵) → (𝑦f · 𝐴) Fn 𝐼)
119118adantrr 717 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦f · 𝐴) Fn 𝐼)
12052ffnd 6500 . . . . . . . . . 10 ((𝜑𝑧𝐵) → (𝑧f · 𝐴) Fn 𝐼)
121120adantrl 716 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑧f · 𝐴) Fn 𝐼)
122119, 121, 79, 79, 51offn 7418 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦f · 𝐴) ∘f (+g𝑇)(𝑧f · 𝐴)) Fn 𝐼)
1237fveq2d 6663 . . . . . . . . . . . . . 14 (𝜑 → (+g𝑅) = (+g‘(Scalar‘𝑇)))
124123ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (+g𝑅) = (+g‘(Scalar‘𝑇)))
125124oveqd 7168 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦𝑥)(+g𝑅)(𝑧𝑥)) = ((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)))
126125oveq1d 7166 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑥)(+g𝑅)(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)))
1278ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑇 ∈ LMod)
128110ffvelrnda 6843 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦𝑥) ∈ (Base‘𝑅))
12939ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
130128, 129eleqtrd 2855 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦𝑥) ∈ (Base‘(Scalar‘𝑇)))
131112ffvelrnda 6843 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘𝑅))
132131, 129eleqtrd 2855 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)))
13349adantr 485 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝐴:𝐼𝐶)
134133ffvelrnda 6843 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝐴𝑥) ∈ 𝐶)
135 eqid 2759 . . . . . . . . . . . . 13 (+g‘(Scalar‘𝑇)) = (+g‘(Scalar‘𝑇))
13619, 21, 5, 3, 43, 135lmodvsdir 19727 . . . . . . . . . . . 12 ((𝑇 ∈ LMod ∧ ((𝑦𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐴𝑥) ∈ 𝐶)) → (((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
137127, 130, 132, 134, 136syl13anc 1370 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
138126, 137eqtrd 2794 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑥)(+g𝑅)(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
139111adantr 485 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 Fn 𝐼)
140113adantr 485 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑧 Fn 𝐼)
14112ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝐼𝑋)
142 simpr 489 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑥𝐼)
143 fnfvof 7422 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼𝑧 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → ((𝑦f (+g𝑅)𝑧)‘𝑥) = ((𝑦𝑥)(+g𝑅)(𝑧𝑥)))
144139, 140, 141, 142, 143syl22anc 838 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦f (+g𝑅)𝑧)‘𝑥) = ((𝑦𝑥)(+g𝑅)(𝑧𝑥)))
145144oveq1d 7166 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦f (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)) = (((𝑦𝑥)(+g𝑅)(𝑧𝑥)) · (𝐴𝑥)))
146115ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝐴 Fn 𝐼)
147 fnfvof 7422 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → ((𝑦f · 𝐴)‘𝑥) = ((𝑦𝑥) · (𝐴𝑥)))
148139, 146, 141, 142, 147syl22anc 838 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦f · 𝐴)‘𝑥) = ((𝑦𝑥) · (𝐴𝑥)))
149 fnfvof 7422 . . . . . . . . . . . 12 (((𝑧 Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → ((𝑧f · 𝐴)‘𝑥) = ((𝑧𝑥) · (𝐴𝑥)))
150140, 146, 141, 142, 149syl22anc 838 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑧f · 𝐴)‘𝑥) = ((𝑧𝑥) · (𝐴𝑥)))
151148, 150oveq12d 7169 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦f · 𝐴)‘𝑥)(+g𝑇)((𝑧f · 𝐴)‘𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
152138, 145, 1513eqtr4d 2804 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦f (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)) = (((𝑦f · 𝐴)‘𝑥)(+g𝑇)((𝑧f · 𝐴)‘𝑥)))
153114adantr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦f (+g𝑅)𝑧) Fn 𝐼)
154 fnfvof 7422 . . . . . . . . . 10 ((((𝑦f (+g𝑅)𝑧) Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → (((𝑦f (+g𝑅)𝑧) ∘f · 𝐴)‘𝑥) = (((𝑦f (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)))
155153, 146, 141, 142, 154syl22anc 838 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦f (+g𝑅)𝑧) ∘f · 𝐴)‘𝑥) = (((𝑦f (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)))
156119adantr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦f · 𝐴) Fn 𝐼)
157121adantr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧f · 𝐴) Fn 𝐼)
158 fnfvof 7422 . . . . . . . . . 10 ((((𝑦f · 𝐴) Fn 𝐼 ∧ (𝑧f · 𝐴) Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → (((𝑦f · 𝐴) ∘f (+g𝑇)(𝑧f · 𝐴))‘𝑥) = (((𝑦f · 𝐴)‘𝑥)(+g𝑇)((𝑧f · 𝐴)‘𝑥)))
159156, 157, 141, 142, 158syl22anc 838 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦f · 𝐴) ∘f (+g𝑇)(𝑧f · 𝐴))‘𝑥) = (((𝑦f · 𝐴)‘𝑥)(+g𝑇)((𝑧f · 𝐴)‘𝑥)))
160152, 155, 1593eqtr4d 2804 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦f (+g𝑅)𝑧) ∘f · 𝐴)‘𝑥) = (((𝑦f · 𝐴) ∘f (+g𝑇)(𝑧f · 𝐴))‘𝑥))
161117, 122, 160eqfnfvd 6797 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦f (+g𝑅)𝑧) ∘f · 𝐴) = ((𝑦f · 𝐴) ∘f (+g𝑇)(𝑧f · 𝐴)))
162107, 161eqtrd 2794 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦(+g𝐹)𝑧) ∘f · 𝐴) = ((𝑦f · 𝐴) ∘f (+g𝑇)(𝑧f · 𝐴)))
163162oveq2d 7167 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘f · 𝐴)) = (𝑇 Σg ((𝑦f · 𝐴) ∘f (+g𝑇)(𝑧f · 𝐴))))
164101, 163eqtrd 2794 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸‘(𝑦(+g𝐹)𝑧)) = (𝑇 Σg ((𝑦f · 𝐴) ∘f (+g𝑇)(𝑧f · 𝐴))))
165 oveq1 7158 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥f · 𝐴) = (𝑦f · 𝐴))
166165oveq2d 7167 . . . . . . 7 (𝑥 = 𝑦 → (𝑇 Σg (𝑥f · 𝐴)) = (𝑇 Σg (𝑦f · 𝐴)))
167 ovex 7184 . . . . . . 7 (𝑇 Σg (𝑦f · 𝐴)) ∈ V
168166, 76, 167fvmpt 6760 . . . . . 6 (𝑦𝐵 → (𝐸𝑦) = (𝑇 Σg (𝑦f · 𝐴)))
169168ad2antrl 728 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸𝑦) = (𝑇 Σg (𝑦f · 𝐴)))
170 oveq1 7158 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥f · 𝐴) = (𝑧f · 𝐴))
171170oveq2d 7167 . . . . . . 7 (𝑥 = 𝑧 → (𝑇 Σg (𝑥f · 𝐴)) = (𝑇 Σg (𝑧f · 𝐴)))
172 ovex 7184 . . . . . . 7 (𝑇 Σg (𝑧f · 𝐴)) ∈ V
173171, 76, 172fvmpt 6760 . . . . . 6 (𝑧𝐵 → (𝐸𝑧) = (𝑇 Σg (𝑧f · 𝐴)))
174173ad2antll 729 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸𝑧) = (𝑇 Σg (𝑧f · 𝐴)))
175169, 174oveq12d 7169 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝐸𝑦)(+g𝑇)(𝐸𝑧)) = ((𝑇 Σg (𝑦f · 𝐴))(+g𝑇)(𝑇 Σg (𝑧f · 𝐴))))
17693, 164, 1753eqtr4d 2804 . . 3 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸‘(𝑦(+g𝐹)𝑧)) = ((𝐸𝑦)(+g𝑇)(𝐸𝑧)))
1771, 19, 20, 21, 23, 25, 77, 176isghmd 18435 . 2 (𝜑𝐸 ∈ (𝐹 GrpHom 𝑇))
1788adantr 485 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑇 ∈ LMod)
17912adantr 485 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝐼𝑋)
18018fveq2d 6663 . . . . . . . 8 (𝜑 → (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝐹)))
181180eleq2d 2838 . . . . . . 7 (𝜑 → (𝑦 ∈ (Base‘(Scalar‘𝑇)) ↔ 𝑦 ∈ (Base‘(Scalar‘𝐹))))
182181biimpar 482 . . . . . 6 ((𝜑𝑦 ∈ (Base‘(Scalar‘𝐹))) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
183182adantrr 717 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
18452adantrl 716 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑧f · 𝐴):𝐼𝐶)
185184ffvelrnda 6843 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑧f · 𝐴)‘𝑥) ∈ 𝐶)
18652feqmptd 6722 . . . . . . 7 ((𝜑𝑧𝐵) → (𝑧f · 𝐴) = (𝑥𝐼 ↦ ((𝑧f · 𝐴)‘𝑥)))
187186, 73eqbrtrrd 5057 . . . . . 6 ((𝜑𝑧𝐵) → (𝑥𝐼 ↦ ((𝑧f · 𝐴)‘𝑥)) finSupp (0g𝑇))
188187adantrl 716 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑥𝐼 ↦ ((𝑧f · 𝐴)‘𝑥)) finSupp (0g𝑇))
18919, 5, 43, 32, 21, 3, 178, 179, 183, 185, 188gsumvsmul 19767 . . . 4 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg (𝑥𝐼 ↦ (𝑦 · ((𝑧f · 𝐴)‘𝑥)))) = (𝑦 · (𝑇 Σg (𝑥𝐼 ↦ ((𝑧f · 𝐴)‘𝑥)))))
19015adantr 485 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝐹 ∈ LMod)
191 simprl 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑦 ∈ (Base‘(Scalar‘𝐹)))
192 simprr 773 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑧𝐵)
1931, 4, 2, 6lmodvscl 19720 . . . . . . . . . . . 12 ((𝐹 ∈ LMod ∧ 𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵) → (𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵)
194190, 191, 192, 193syl3anc 1369 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵)
19513, 46, 1frlmbasf 20526 . . . . . . . . . . 11 ((𝐼𝑋 ∧ (𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵) → (𝑦( ·𝑠𝐹)𝑧):𝐼⟶(Base‘𝑅))
196179, 194, 195syl2anc 588 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦( ·𝑠𝐹)𝑧):𝐼⟶(Base‘𝑅))
197196ffnd 6500 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦( ·𝑠𝐹)𝑧) Fn 𝐼)
198115adantr 485 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝐴 Fn 𝐼)
199197, 198, 179, 179, 51offn 7418 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴) Fn 𝐼)
200 dffn2 6501 . . . . . . . 8 (((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴) Fn 𝐼 ↔ ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴):𝐼⟶V)
201199, 200sylib 221 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴):𝐼⟶V)
202201feqmptd 6722 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴) = (𝑥𝐼 ↦ (((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)‘𝑥)))
2037fveq2d 6663 . . . . . . . . . . . 12 (𝜑 → (.r𝑅) = (.r‘(Scalar‘𝑇)))
204203ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (.r𝑅) = (.r‘(Scalar‘𝑇)))
205204oveqd 7168 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦(.r𝑅)(𝑧𝑥)) = (𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)))
206205oveq1d 7166 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)) = ((𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)))
2078ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑇 ∈ LMod)
208 simplrl 777 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 ∈ (Base‘(Scalar‘𝐹)))
209180ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝐹)))
210208, 209eleqtrrd 2856 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
21148ffvelrnda 6843 . . . . . . . . . . . 12 (((𝜑𝑧𝐵) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘𝑅))
21239ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑧𝐵) ∧ 𝑥𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
213211, 212eleqtrd 2855 . . . . . . . . . . 11 (((𝜑𝑧𝐵) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)))
214213adantlrl 720 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)))
21549ffvelrnda 6843 . . . . . . . . . . 11 ((𝜑𝑥𝐼) → (𝐴𝑥) ∈ 𝐶)
216215adantlr 715 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝐴𝑥) ∈ 𝐶)
217 eqid 2759 . . . . . . . . . . 11 (.r‘(Scalar‘𝑇)) = (.r‘(Scalar‘𝑇))
21819, 5, 3, 43, 217lmodvsass 19728 . . . . . . . . . 10 ((𝑇 ∈ LMod ∧ (𝑦 ∈ (Base‘(Scalar‘𝑇)) ∧ (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐴𝑥) ∈ 𝐶)) → ((𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
219207, 210, 214, 216, 218syl13anc 1370 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
220206, 219eqtrd 2794 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
221197adantr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦( ·𝑠𝐹)𝑧) Fn 𝐼)
222115ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝐴 Fn 𝐼)
22312ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝐼𝑋)
224 simpr 489 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑥𝐼)
225 fnfvof 7422 . . . . . . . . . 10 ((((𝑦( ·𝑠𝐹)𝑧) Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → (((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)‘𝑥) = (((𝑦( ·𝑠𝐹)𝑧)‘𝑥) · (𝐴𝑥)))
226221, 222, 223, 224, 225syl22anc 838 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)‘𝑥) = (((𝑦( ·𝑠𝐹)𝑧)‘𝑥) · (𝐴𝑥)))
22717fveq2d 6663 . . . . . . . . . . . . 13 (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝐹)))
228227ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝐹)))
229208, 228eleqtrrd 2856 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 ∈ (Base‘𝑅))
230 simplrr 778 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑧𝐵)
231 eqid 2759 . . . . . . . . . . 11 (.r𝑅) = (.r𝑅)
23213, 1, 46, 223, 229, 230, 224, 2, 231frlmvscaval 20534 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦( ·𝑠𝐹)𝑧)‘𝑥) = (𝑦(.r𝑅)(𝑧𝑥)))
233232oveq1d 7166 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧)‘𝑥) · (𝐴𝑥)) = ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)))
234226, 233eqtrd 2794 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)‘𝑥) = ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)))
23548ffnd 6500 . . . . . . . . . . . 12 ((𝜑𝑧𝐵) → 𝑧 Fn 𝐼)
236235adantrl 716 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑧 Fn 𝐼)
237236adantr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑧 Fn 𝐼)
238237, 222, 223, 224, 149syl22anc 838 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑧f · 𝐴)‘𝑥) = ((𝑧𝑥) · (𝐴𝑥)))
239238oveq2d 7167 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦 · ((𝑧f · 𝐴)‘𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
240220, 234, 2393eqtr4d 2804 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)‘𝑥) = (𝑦 · ((𝑧f · 𝐴)‘𝑥)))
241240mpteq2dva 5128 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑥𝐼 ↦ (((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)‘𝑥)) = (𝑥𝐼 ↦ (𝑦 · ((𝑧f · 𝐴)‘𝑥))))
242202, 241eqtrd 2794 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴) = (𝑥𝐼 ↦ (𝑦 · ((𝑧f · 𝐴)‘𝑥))))
243242oveq2d 7167 . . . 4 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)) = (𝑇 Σg (𝑥𝐼 ↦ (𝑦 · ((𝑧f · 𝐴)‘𝑥)))))
244184feqmptd 6722 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑧f · 𝐴) = (𝑥𝐼 ↦ ((𝑧f · 𝐴)‘𝑥)))
245244oveq2d 7167 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg (𝑧f · 𝐴)) = (𝑇 Σg (𝑥𝐼 ↦ ((𝑧f · 𝐴)‘𝑥))))
246245oveq2d 7167 . . . 4 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦 · (𝑇 Σg (𝑧f · 𝐴))) = (𝑦 · (𝑇 Σg (𝑥𝐼 ↦ ((𝑧f · 𝐴)‘𝑥)))))
247189, 243, 2463eqtr4d 2804 . . 3 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)) = (𝑦 · (𝑇 Σg (𝑧f · 𝐴))))
248 oveq1 7158 . . . . . 6 (𝑥 = (𝑦( ·𝑠𝐹)𝑧) → (𝑥f · 𝐴) = ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴))
249248oveq2d 7167 . . . . 5 (𝑥 = (𝑦( ·𝑠𝐹)𝑧) → (𝑇 Σg (𝑥f · 𝐴)) = (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)))
250 ovex 7184 . . . . 5 (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)) ∈ V
251249, 76, 250fvmpt 6760 . . . 4 ((𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵 → (𝐸‘(𝑦( ·𝑠𝐹)𝑧)) = (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)))
252194, 251syl 17 . . 3 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝐸‘(𝑦( ·𝑠𝐹)𝑧)) = (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘f · 𝐴)))
253173oveq2d 7167 . . . 4 (𝑧𝐵 → (𝑦 · (𝐸𝑧)) = (𝑦 · (𝑇 Σg (𝑧f · 𝐴))))
254253ad2antll 729 . . 3 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦 · (𝐸𝑧)) = (𝑦 · (𝑇 Σg (𝑧f · 𝐴))))
255247, 252, 2543eqtr4d 2804 . 2 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝐸‘(𝑦( ·𝑠𝐹)𝑧)) = (𝑦 · (𝐸𝑧)))
2561, 2, 3, 4, 5, 6, 15, 8, 18, 177, 255islmhmd 19880 1 (𝜑𝐸 ∈ (𝐹 LMHom 𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539   ∈ wcel 2112  Vcvv 3410   ⊆ wss 3859   class class class wbr 5033   ↦ cmpt 5113  Fun wfun 6330   Fn wfn 6331  ⟶wf 6332  ‘cfv 6336  (class class class)co 7151   ∘f cof 7404   supp csupp 7836  Fincfn 8528   finSupp cfsupp 8867  Basecbs 16542  +gcplusg 16624  .rcmulr 16625  Scalarcsca 16627   ·𝑠 cvsca 16628  0gc0g 16772   Σg cgsu 16773  Grpcgrp 18170  CMndccmn 18974  Ringcrg 19366  LModclmod 19703   LMHom clmhm 19860   freeLMod cfrlm 20512 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10632  ax-resscn 10633  ax-1cn 10634  ax-icn 10635  ax-addcl 10636  ax-addrcl 10637  ax-mulcl 10638  ax-mulrcl 10639  ax-mulcom 10640  ax-addass 10641  ax-mulass 10642  ax-distr 10643  ax-i2m1 10644  ax-1ne0 10645  ax-1rid 10646  ax-rnegex 10647  ax-rrecex 10648  ax-cnre 10649  ax-pre-lttri 10650  ax-pre-lttrn 10651  ax-pre-ltadd 10652  ax-pre-mulgt0 10653 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7406  df-om 7581  df-1st 7694  df-2nd 7695  df-supp 7837  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-er 8300  df-map 8419  df-ixp 8481  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-fsupp 8868  df-sup 8940  df-oi 9008  df-card 9402  df-pnf 10716  df-mnf 10717  df-xr 10718  df-ltxr 10719  df-le 10720  df-sub 10911  df-neg 10912  df-nn 11676  df-2 11738  df-3 11739  df-4 11740  df-5 11741  df-6 11742  df-7 11743  df-8 11744  df-9 11745  df-n0 11936  df-z 12022  df-dec 12139  df-uz 12284  df-fz 12941  df-fzo 13084  df-seq 13420  df-hash 13742  df-struct 16544  df-ndx 16545  df-slot 16546  df-base 16548  df-sets 16549  df-ress 16550  df-plusg 16637  df-mulr 16638  df-sca 16640  df-vsca 16641  df-ip 16642  df-tset 16643  df-ple 16644  df-ds 16646  df-hom 16648  df-cco 16649  df-0g 16774  df-gsum 16775  df-prds 16780  df-pws 16782  df-mgm 17919  df-sgrp 17968  df-mnd 17979  df-mhm 18023  df-submnd 18024  df-grp 18173  df-minusg 18174  df-sbg 18175  df-subg 18344  df-ghm 18424  df-cntz 18515  df-cmn 18976  df-abl 18977  df-mgp 19309  df-ur 19321  df-ring 19368  df-subrg 19602  df-lmod 19705  df-lss 19773  df-lmhm 19863  df-sra 20013  df-rgmod 20014  df-dsmm 20498  df-frlm 20513 This theorem is referenced by:  frlmup3  20566  frlmup4  20567  islindf5  20605  indlcim  20606  lnrfg  40437
 Copyright terms: Public domain W3C validator