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

Theorem frlmup1 20511
 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.
StepHypRef Expression
1 frlmup.b . 2 𝐵 = (Base‘𝐹)
2 eqid 2825 . 2 ( ·𝑠𝐹) = ( ·𝑠𝐹)
3 frlmup.v . 2 · = ( ·𝑠𝑇)
4 eqid 2825 . 2 (Scalar‘𝐹) = (Scalar‘𝐹)
5 eqid 2825 . 2 (Scalar‘𝑇) = (Scalar‘𝑇)
6 eqid 2825 . 2 (Base‘(Scalar‘𝐹)) = (Base‘(Scalar‘𝐹))
7 frlmup.r . . . 4 (𝜑𝑅 = (Scalar‘𝑇))
8 frlmup.t . . . . 5 (𝜑𝑇 ∈ LMod)
95lmodring 19234 . . . . 5 (𝑇 ∈ LMod → (Scalar‘𝑇) ∈ Ring)
108, 9syl 17 . . . 4 (𝜑 → (Scalar‘𝑇) ∈ Ring)
117, 10eqeltrd 2906 . . 3 (𝜑𝑅 ∈ Ring)
12 frlmup.i . . 3 (𝜑𝐼𝑋)
13 frlmup.f . . . 4 𝐹 = (𝑅 freeLMod 𝐼)
1413frlmlmod 20463 . . 3 ((𝑅 ∈ Ring ∧ 𝐼𝑋) → 𝐹 ∈ LMod)
1511, 12, 14syl2anc 579 . 2 (𝜑𝐹 ∈ LMod)
1613frlmsca 20467 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼𝑋) → 𝑅 = (Scalar‘𝐹))
1711, 12, 16syl2anc 579 . . 3 (𝜑𝑅 = (Scalar‘𝐹))
187, 17eqtr3d 2863 . 2 (𝜑 → (Scalar‘𝑇) = (Scalar‘𝐹))
19 frlmup.c . . 3 𝐶 = (Base‘𝑇)
20 eqid 2825 . . 3 (+g𝐹) = (+g𝐹)
21 eqid 2825 . . 3 (+g𝑇) = (+g𝑇)
22 lmodgrp 19233 . . . 4 (𝐹 ∈ LMod → 𝐹 ∈ Grp)
2315, 22syl 17 . . 3 (𝜑𝐹 ∈ Grp)
24 lmodgrp 19233 . . . 4 (𝑇 ∈ LMod → 𝑇 ∈ Grp)
258, 24syl 17 . . 3 (𝜑𝑇 ∈ Grp)
26 eleq1w 2889 . . . . . . 7 (𝑧 = 𝑥 → (𝑧𝐵𝑥𝐵))
2726anbi2d 622 . . . . . 6 (𝑧 = 𝑥 → ((𝜑𝑧𝐵) ↔ (𝜑𝑥𝐵)))
28 oveq1 6917 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧𝑓 · 𝐴) = (𝑥𝑓 · 𝐴))
2928oveq2d 6926 . . . . . . 7 (𝑧 = 𝑥 → (𝑇 Σg (𝑧𝑓 · 𝐴)) = (𝑇 Σg (𝑥𝑓 · 𝐴)))
3029eleq1d 2891 . . . . . 6 (𝑧 = 𝑥 → ((𝑇 Σg (𝑧𝑓 · 𝐴)) ∈ 𝐶 ↔ (𝑇 Σg (𝑥𝑓 · 𝐴)) ∈ 𝐶))
3127, 30imbi12d 336 . . . . 5 (𝑧 = 𝑥 → (((𝜑𝑧𝐵) → (𝑇 Σg (𝑧𝑓 · 𝐴)) ∈ 𝐶) ↔ ((𝜑𝑥𝐵) → (𝑇 Σg (𝑥𝑓 · 𝐴)) ∈ 𝐶)))
32 eqid 2825 . . . . . 6 (0g𝑇) = (0g𝑇)
33 lmodcmn 19274 . . . . . . . 8 (𝑇 ∈ LMod → 𝑇 ∈ CMnd)
348, 33syl 17 . . . . . . 7 (𝜑𝑇 ∈ CMnd)
3534adantr 474 . . . . . 6 ((𝜑𝑧𝐵) → 𝑇 ∈ CMnd)
3612adantr 474 . . . . . 6 ((𝜑𝑧𝐵) → 𝐼𝑋)
378ad2antrr 717 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑇 ∈ LMod)
38 simprl 787 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑥 ∈ (Base‘𝑅))
397fveq2d 6441 . . . . . . . . . 10 (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
4039ad2antrr 717 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
4138, 40eleqtrd 2908 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑥 ∈ (Base‘(Scalar‘𝑇)))
42 simprr 789 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑦𝐶)
43 eqid 2825 . . . . . . . . 9 (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇))
4419, 5, 3, 43lmodvscl 19243 . . . . . . . 8 ((𝑇 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑦𝐶) → (𝑥 · 𝑦) ∈ 𝐶)
4537, 41, 42, 44syl3anc 1494 . . . . . . 7 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → (𝑥 · 𝑦) ∈ 𝐶)
46 eqid 2825 . . . . . . . . 9 (Base‘𝑅) = (Base‘𝑅)
4713, 46, 1frlmbasf 20474 . . . . . . . 8 ((𝐼𝑋𝑧𝐵) → 𝑧:𝐼⟶(Base‘𝑅))
4812, 47sylan 575 . . . . . . 7 ((𝜑𝑧𝐵) → 𝑧:𝐼⟶(Base‘𝑅))
49 frlmup.a . . . . . . . 8 (𝜑𝐴:𝐼𝐶)
5049adantr 474 . . . . . . 7 ((𝜑𝑧𝐵) → 𝐴:𝐼𝐶)
51 inidm 4049 . . . . . . 7 (𝐼𝐼) = 𝐼
5245, 48, 50, 36, 36, 51off 7177 . . . . . 6 ((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴):𝐼𝐶)
53 ovex 6942 . . . . . . . 8 (𝑧𝑓 · 𝐴) ∈ V
5453a1i 11 . . . . . . 7 ((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴) ∈ V)
5552ffund 6286 . . . . . . 7 ((𝜑𝑧𝐵) → Fun (𝑧𝑓 · 𝐴))
56 fvexd 6452 . . . . . . 7 ((𝜑𝑧𝐵) → (0g𝑇) ∈ V)
57 eqid 2825 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
5813, 57, 1frlmbasfsupp 20472 . . . . . . . . . 10 ((𝐼𝑋𝑧𝐵) → 𝑧 finSupp (0g𝑅))
5912, 58sylan 575 . . . . . . . . 9 ((𝜑𝑧𝐵) → 𝑧 finSupp (0g𝑅))
607fveq2d 6441 . . . . . . . . . . . 12 (𝜑 → (0g𝑅) = (0g‘(Scalar‘𝑇)))
6160eqcomd 2831 . . . . . . . . . . 11 (𝜑 → (0g‘(Scalar‘𝑇)) = (0g𝑅))
6261breq2d 4887 . . . . . . . . . 10 (𝜑 → (𝑧 finSupp (0g‘(Scalar‘𝑇)) ↔ 𝑧 finSupp (0g𝑅)))
6362adantr 474 . . . . . . . . 9 ((𝜑𝑧𝐵) → (𝑧 finSupp (0g‘(Scalar‘𝑇)) ↔ 𝑧 finSupp (0g𝑅)))
6459, 63mpbird 249 . . . . . . . 8 ((𝜑𝑧𝐵) → 𝑧 finSupp (0g‘(Scalar‘𝑇)))
6564fsuppimpd 8557 . . . . . . 7 ((𝜑𝑧𝐵) → (𝑧 supp (0g‘(Scalar‘𝑇))) ∈ Fin)
66 ssidd 3849 . . . . . . . 8 ((𝜑𝑧𝐵) → (𝑧 supp (0g‘(Scalar‘𝑇))) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))
678ad2antrr 717 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ 𝑤𝐶) → 𝑇 ∈ LMod)
68 eqid 2825 . . . . . . . . . 10 (0g‘(Scalar‘𝑇)) = (0g‘(Scalar‘𝑇))
6919, 5, 3, 68, 32lmod0vs 19259 . . . . . . . . 9 ((𝑇 ∈ LMod ∧ 𝑤𝐶) → ((0g‘(Scalar‘𝑇)) · 𝑤) = (0g𝑇))
7067, 69sylancom 582 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ 𝑤𝐶) → ((0g‘(Scalar‘𝑇)) · 𝑤) = (0g𝑇))
71 fvexd 6452 . . . . . . . 8 ((𝜑𝑧𝐵) → (0g‘(Scalar‘𝑇)) ∈ V)
7266, 70, 48, 50, 36, 71suppssof1 7598 . . . . . . 7 ((𝜑𝑧𝐵) → ((𝑧𝑓 · 𝐴) supp (0g𝑇)) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))
73 suppssfifsupp 8565 . . . . . . 7 ((((𝑧𝑓 · 𝐴) ∈ V ∧ Fun (𝑧𝑓 · 𝐴) ∧ (0g𝑇) ∈ V) ∧ ((𝑧 supp (0g‘(Scalar‘𝑇))) ∈ Fin ∧ ((𝑧𝑓 · 𝐴) supp (0g𝑇)) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))) → (𝑧𝑓 · 𝐴) finSupp (0g𝑇))
7454, 55, 56, 65, 72, 73syl32anc 1501 . . . . . 6 ((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴) finSupp (0g𝑇))
7519, 32, 35, 36, 52, 74gsumcl 18676 . . . . 5 ((𝜑𝑧𝐵) → (𝑇 Σg (𝑧𝑓 · 𝐴)) ∈ 𝐶)
7631, 75chvarv 2416 . . . 4 ((𝜑𝑥𝐵) → (𝑇 Σg (𝑥𝑓 · 𝐴)) ∈ 𝐶)
77 frlmup.e . . . 4 𝐸 = (𝑥𝐵 ↦ (𝑇 Σg (𝑥𝑓 · 𝐴)))
7876, 77fmptd 6638 . . 3 (𝜑𝐸:𝐵𝐶)
7934adantr 474 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑇 ∈ CMnd)
8012adantr 474 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝐼𝑋)
81 eleq1w 2889 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧𝐵𝑦𝐵))
8281anbi2d 622 . . . . . . . 8 (𝑧 = 𝑦 → ((𝜑𝑧𝐵) ↔ (𝜑𝑦𝐵)))
83 oveq1 6917 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧𝑓 · 𝐴) = (𝑦𝑓 · 𝐴))
8483feq1d 6267 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧𝑓 · 𝐴):𝐼𝐶 ↔ (𝑦𝑓 · 𝐴):𝐼𝐶))
8582, 84imbi12d 336 . . . . . . 7 (𝑧 = 𝑦 → (((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴):𝐼𝐶) ↔ ((𝜑𝑦𝐵) → (𝑦𝑓 · 𝐴):𝐼𝐶)))
8685, 52chvarv 2416 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦𝑓 · 𝐴):𝐼𝐶)
8786adantrr 708 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦𝑓 · 𝐴):𝐼𝐶)
8852adantrl 707 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑧𝑓 · 𝐴):𝐼𝐶)
8983breq1d 4885 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧𝑓 · 𝐴) finSupp (0g𝑇) ↔ (𝑦𝑓 · 𝐴) finSupp (0g𝑇)))
9082, 89imbi12d 336 . . . . . . 7 (𝑧 = 𝑦 → (((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴) finSupp (0g𝑇)) ↔ ((𝜑𝑦𝐵) → (𝑦𝑓 · 𝐴) finSupp (0g𝑇))))
9190, 74chvarv 2416 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦𝑓 · 𝐴) finSupp (0g𝑇))
9291adantrr 708 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦𝑓 · 𝐴) finSupp (0g𝑇))
9374adantrl 707 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑧𝑓 · 𝐴) finSupp (0g𝑇))
9419, 32, 21, 79, 80, 87, 88, 92, 93gsumadd 18683 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑇 Σg ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))) = ((𝑇 Σg (𝑦𝑓 · 𝐴))(+g𝑇)(𝑇 Σg (𝑧𝑓 · 𝐴))))
951, 20lmodvacl 19240 . . . . . . . 8 ((𝐹 ∈ LMod ∧ 𝑦𝐵𝑧𝐵) → (𝑦(+g𝐹)𝑧) ∈ 𝐵)
96953expb 1153 . . . . . . 7 ((𝐹 ∈ LMod ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(+g𝐹)𝑧) ∈ 𝐵)
9715, 96sylan 575 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(+g𝐹)𝑧) ∈ 𝐵)
98 oveq1 6917 . . . . . . . 8 (𝑥 = (𝑦(+g𝐹)𝑧) → (𝑥𝑓 · 𝐴) = ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴))
9998oveq2d 6926 . . . . . . 7 (𝑥 = (𝑦(+g𝐹)𝑧) → (𝑇 Σg (𝑥𝑓 · 𝐴)) = (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴)))
100 ovex 6942 . . . . . . 7 (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴)) ∈ V
10199, 77, 100fvmpt 6533 . . . . . 6 ((𝑦(+g𝐹)𝑧) ∈ 𝐵 → (𝐸‘(𝑦(+g𝐹)𝑧)) = (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴)))
10297, 101syl 17 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸‘(𝑦(+g𝐹)𝑧)) = (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴)))
10311adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑅 ∈ Ring)
104 simprl 787 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑦𝐵)
105 simprr 789 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑧𝐵)
106 eqid 2825 . . . . . . . . 9 (+g𝑅) = (+g𝑅)
10713, 1, 103, 80, 104, 105, 106, 20frlmplusgval 20477 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(+g𝐹)𝑧) = (𝑦𝑓 (+g𝑅)𝑧))
108107oveq1d 6925 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴) = ((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴))
10913, 46, 1frlmbasf 20474 . . . . . . . . . . . . 13 ((𝐼𝑋𝑦𝐵) → 𝑦:𝐼⟶(Base‘𝑅))
11012, 109sylan 575 . . . . . . . . . . . 12 ((𝜑𝑦𝐵) → 𝑦:𝐼⟶(Base‘𝑅))
111110adantrr 708 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑦:𝐼⟶(Base‘𝑅))
112111ffnd 6283 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑦 Fn 𝐼)
11348adantrl 707 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑧:𝐼⟶(Base‘𝑅))
114113ffnd 6283 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑧 Fn 𝐼)
115112, 114, 80, 80, 51offn 7173 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦𝑓 (+g𝑅)𝑧) Fn 𝐼)
11649ffnd 6283 . . . . . . . . . 10 (𝜑𝐴 Fn 𝐼)
117116adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝐴 Fn 𝐼)
118115, 117, 80, 80, 51offn 7173 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴) Fn 𝐼)
11986ffnd 6283 . . . . . . . . . 10 ((𝜑𝑦𝐵) → (𝑦𝑓 · 𝐴) Fn 𝐼)
120119adantrr 708 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦𝑓 · 𝐴) Fn 𝐼)
12152ffnd 6283 . . . . . . . . . 10 ((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴) Fn 𝐼)
122121adantrl 707 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑧𝑓 · 𝐴) Fn 𝐼)
123120, 122, 80, 80, 51offn 7173 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴)) Fn 𝐼)
1247fveq2d 6441 . . . . . . . . . . . . . 14 (𝜑 → (+g𝑅) = (+g‘(Scalar‘𝑇)))
125124ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (+g𝑅) = (+g‘(Scalar‘𝑇)))
126125oveqd 6927 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦𝑥)(+g𝑅)(𝑧𝑥)) = ((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)))
127126oveq1d 6925 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑥)(+g𝑅)(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)))
1288ad2antrr 717 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑇 ∈ LMod)
129111ffvelrnda 6613 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦𝑥) ∈ (Base‘𝑅))
13039ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
131129, 130eleqtrd 2908 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦𝑥) ∈ (Base‘(Scalar‘𝑇)))
132113ffvelrnda 6613 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘𝑅))
133132, 130eleqtrd 2908 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)))
13449adantr 474 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝐴:𝐼𝐶)
135134ffvelrnda 6613 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝐴𝑥) ∈ 𝐶)
136 eqid 2825 . . . . . . . . . . . . 13 (+g‘(Scalar‘𝑇)) = (+g‘(Scalar‘𝑇))
13719, 21, 5, 3, 43, 136lmodvsdir 19250 . . . . . . . . . . . 12 ((𝑇 ∈ LMod ∧ ((𝑦𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐴𝑥) ∈ 𝐶)) → (((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
138128, 131, 133, 135, 137syl13anc 1495 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
139127, 138eqtrd 2861 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑥)(+g𝑅)(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
140112adantr 474 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 Fn 𝐼)
141114adantr 474 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑧 Fn 𝐼)
14212ad2antrr 717 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝐼𝑋)
143 simpr 479 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑥𝐼)
144 fnfvof 7176 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼𝑧 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → ((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) = ((𝑦𝑥)(+g𝑅)(𝑧𝑥)))
145140, 141, 142, 143, 144syl22anc 872 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) = ((𝑦𝑥)(+g𝑅)(𝑧𝑥)))
146145oveq1d 6925 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)) = (((𝑦𝑥)(+g𝑅)(𝑧𝑥)) · (𝐴𝑥)))
147116ad2antrr 717 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝐴 Fn 𝐼)
148 fnfvof 7176 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → ((𝑦𝑓 · 𝐴)‘𝑥) = ((𝑦𝑥) · (𝐴𝑥)))
149140, 147, 142, 143, 148syl22anc 872 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦𝑓 · 𝐴)‘𝑥) = ((𝑦𝑥) · (𝐴𝑥)))
150 fnfvof 7176 . . . . . . . . . . . 12 (((𝑧 Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → ((𝑧𝑓 · 𝐴)‘𝑥) = ((𝑧𝑥) · (𝐴𝑥)))
151141, 147, 142, 143, 150syl22anc 872 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑧𝑓 · 𝐴)‘𝑥) = ((𝑧𝑥) · (𝐴𝑥)))
152149, 151oveq12d 6928 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 · 𝐴)‘𝑥)(+g𝑇)((𝑧𝑓 · 𝐴)‘𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
153139, 146, 1523eqtr4d 2871 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)) = (((𝑦𝑓 · 𝐴)‘𝑥)(+g𝑇)((𝑧𝑓 · 𝐴)‘𝑥)))
154115adantr 474 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦𝑓 (+g𝑅)𝑧) Fn 𝐼)
155 fnfvof 7176 . . . . . . . . . 10 ((((𝑦𝑓 (+g𝑅)𝑧) Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → (((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)))
156154, 147, 142, 143, 155syl22anc 872 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)))
157120adantr 474 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦𝑓 · 𝐴) Fn 𝐼)
158122adantr 474 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑓 · 𝐴) Fn 𝐼)
159 fnfvof 7176 . . . . . . . . . 10 ((((𝑦𝑓 · 𝐴) Fn 𝐼 ∧ (𝑧𝑓 · 𝐴) Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → (((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))‘𝑥) = (((𝑦𝑓 · 𝐴)‘𝑥)(+g𝑇)((𝑧𝑓 · 𝐴)‘𝑥)))
160157, 158, 142, 143, 159syl22anc 872 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))‘𝑥) = (((𝑦𝑓 · 𝐴)‘𝑥)(+g𝑇)((𝑧𝑓 · 𝐴)‘𝑥)))
161153, 156, 1603eqtr4d 2871 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))‘𝑥))
162118, 123, 161eqfnfvd 6568 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴) = ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴)))
163108, 162eqtrd 2861 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴) = ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴)))
164163oveq2d 6926 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴)) = (𝑇 Σg ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))))
165102, 164eqtrd 2861 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸‘(𝑦(+g𝐹)𝑧)) = (𝑇 Σg ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))))
166 oveq1 6917 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝑓 · 𝐴) = (𝑦𝑓 · 𝐴))
167166oveq2d 6926 . . . . . . 7 (𝑥 = 𝑦 → (𝑇 Σg (𝑥𝑓 · 𝐴)) = (𝑇 Σg (𝑦𝑓 · 𝐴)))
168 ovex 6942 . . . . . . 7 (𝑇 Σg (𝑦𝑓 · 𝐴)) ∈ V
169167, 77, 168fvmpt 6533 . . . . . 6 (𝑦𝐵 → (𝐸𝑦) = (𝑇 Σg (𝑦𝑓 · 𝐴)))
170169ad2antrl 719 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸𝑦) = (𝑇 Σg (𝑦𝑓 · 𝐴)))
171 oveq1 6917 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥𝑓 · 𝐴) = (𝑧𝑓 · 𝐴))
172171oveq2d 6926 . . . . . . 7 (𝑥 = 𝑧 → (𝑇 Σg (𝑥𝑓 · 𝐴)) = (𝑇 Σg (𝑧𝑓 · 𝐴)))
173 ovex 6942 . . . . . . 7 (𝑇 Σg (𝑧𝑓 · 𝐴)) ∈ V
174172, 77, 173fvmpt 6533 . . . . . 6 (𝑧𝐵 → (𝐸𝑧) = (𝑇 Σg (𝑧𝑓 · 𝐴)))
175174ad2antll 720 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸𝑧) = (𝑇 Σg (𝑧𝑓 · 𝐴)))
176170, 175oveq12d 6928 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝐸𝑦)(+g𝑇)(𝐸𝑧)) = ((𝑇 Σg (𝑦𝑓 · 𝐴))(+g𝑇)(𝑇 Σg (𝑧𝑓 · 𝐴))))
17794, 165, 1763eqtr4d 2871 . . 3 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸‘(𝑦(+g𝐹)𝑧)) = ((𝐸𝑦)(+g𝑇)(𝐸𝑧)))
1781, 19, 20, 21, 23, 25, 78, 177isghmd 18027 . 2 (𝜑𝐸 ∈ (𝐹 GrpHom 𝑇))
1798adantr 474 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑇 ∈ LMod)
18012adantr 474 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝐼𝑋)
18118fveq2d 6441 . . . . . . . 8 (𝜑 → (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝐹)))
182181eleq2d 2892 . . . . . . 7 (𝜑 → (𝑦 ∈ (Base‘(Scalar‘𝑇)) ↔ 𝑦 ∈ (Base‘(Scalar‘𝐹))))
183182biimpar 471 . . . . . 6 ((𝜑𝑦 ∈ (Base‘(Scalar‘𝐹))) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
184183adantrr 708 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
18552adantrl 707 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑧𝑓 · 𝐴):𝐼𝐶)
186185ffvelrnda 6613 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑧𝑓 · 𝐴)‘𝑥) ∈ 𝐶)
18752feqmptd 6500 . . . . . . 7 ((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴) = (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)))
188187, 74eqbrtrrd 4899 . . . . . 6 ((𝜑𝑧𝐵) → (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)) finSupp (0g𝑇))
189188adantrl 707 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)) finSupp (0g𝑇))
19019, 5, 43, 32, 21, 3, 179, 180, 184, 186, 189gsumvsmul 19290 . . . 4 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg (𝑥𝐼 ↦ (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥)))) = (𝑦 · (𝑇 Σg (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)))))
19115adantr 474 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝐹 ∈ LMod)
192 simprl 787 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑦 ∈ (Base‘(Scalar‘𝐹)))
193 simprr 789 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑧𝐵)
1941, 4, 2, 6lmodvscl 19243 . . . . . . . . . . . 12 ((𝐹 ∈ LMod ∧ 𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵) → (𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵)
195191, 192, 193, 194syl3anc 1494 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵)
19613, 46, 1frlmbasf 20474 . . . . . . . . . . 11 ((𝐼𝑋 ∧ (𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵) → (𝑦( ·𝑠𝐹)𝑧):𝐼⟶(Base‘𝑅))
197180, 195, 196syl2anc 579 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦( ·𝑠𝐹)𝑧):𝐼⟶(Base‘𝑅))
198197ffnd 6283 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦( ·𝑠𝐹)𝑧) Fn 𝐼)
199116adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝐴 Fn 𝐼)
200198, 199, 180, 180, 51offn 7173 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴) Fn 𝐼)
201 dffn2 6284 . . . . . . . 8 (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴) Fn 𝐼 ↔ ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴):𝐼⟶V)
202200, 201sylib 210 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴):𝐼⟶V)
203202feqmptd 6500 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴) = (𝑥𝐼 ↦ (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥)))
2047fveq2d 6441 . . . . . . . . . . . 12 (𝜑 → (.r𝑅) = (.r‘(Scalar‘𝑇)))
205204ad2antrr 717 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (.r𝑅) = (.r‘(Scalar‘𝑇)))
206205oveqd 6927 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦(.r𝑅)(𝑧𝑥)) = (𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)))
207206oveq1d 6925 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)) = ((𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)))
2088ad2antrr 717 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑇 ∈ LMod)
209 simplrl 795 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 ∈ (Base‘(Scalar‘𝐹)))
210181ad2antrr 717 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝐹)))
211209, 210eleqtrrd 2909 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
21248ffvelrnda 6613 . . . . . . . . . . . 12 (((𝜑𝑧𝐵) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘𝑅))
21339ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑧𝐵) ∧ 𝑥𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
214212, 213eleqtrd 2908 . . . . . . . . . . 11 (((𝜑𝑧𝐵) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)))
215214adantlrl 711 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)))
21649ffvelrnda 6613 . . . . . . . . . . 11 ((𝜑𝑥𝐼) → (𝐴𝑥) ∈ 𝐶)
217216adantlr 706 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝐴𝑥) ∈ 𝐶)
218 eqid 2825 . . . . . . . . . . 11 (.r‘(Scalar‘𝑇)) = (.r‘(Scalar‘𝑇))
21919, 5, 3, 43, 218lmodvsass 19251 . . . . . . . . . 10 ((𝑇 ∈ LMod ∧ (𝑦 ∈ (Base‘(Scalar‘𝑇)) ∧ (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐴𝑥) ∈ 𝐶)) → ((𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
220208, 211, 215, 217, 219syl13anc 1495 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
221207, 220eqtrd 2861 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
222198adantr 474 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦( ·𝑠𝐹)𝑧) Fn 𝐼)
223116ad2antrr 717 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝐴 Fn 𝐼)
22412ad2antrr 717 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝐼𝑋)
225 simpr 479 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑥𝐼)
226 fnfvof 7176 . . . . . . . . . 10 ((((𝑦( ·𝑠𝐹)𝑧) Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦( ·𝑠𝐹)𝑧)‘𝑥) · (𝐴𝑥)))
227222, 223, 224, 225, 226syl22anc 872 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦( ·𝑠𝐹)𝑧)‘𝑥) · (𝐴𝑥)))
22817fveq2d 6441 . . . . . . . . . . . . 13 (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝐹)))
229228ad2antrr 717 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝐹)))
230209, 229eleqtrrd 2909 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 ∈ (Base‘𝑅))
231 simplrr 796 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑧𝐵)
232 eqid 2825 . . . . . . . . . . 11 (.r𝑅) = (.r𝑅)
23313, 1, 46, 224, 230, 231, 225, 2, 232frlmvscaval 20481 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦( ·𝑠𝐹)𝑧)‘𝑥) = (𝑦(.r𝑅)(𝑧𝑥)))
234233oveq1d 6925 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧)‘𝑥) · (𝐴𝑥)) = ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)))
235227, 234eqtrd 2861 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)))
23648ffnd 6283 . . . . . . . . . . . 12 ((𝜑𝑧𝐵) → 𝑧 Fn 𝐼)
237236adantrl 707 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑧 Fn 𝐼)
238237adantr 474 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑧 Fn 𝐼)
239238, 223, 224, 225, 150syl22anc 872 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑧𝑓 · 𝐴)‘𝑥) = ((𝑧𝑥) · (𝐴𝑥)))
240239oveq2d 6926 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
241221, 235, 2403eqtr4d 2871 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥)))
242241mpteq2dva 4969 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑥𝐼 ↦ (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥)) = (𝑥𝐼 ↦ (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥))))
243203, 242eqtrd 2861 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴) = (𝑥𝐼 ↦ (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥))))
244243oveq2d 6926 . . . 4 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)) = (𝑇 Σg (𝑥𝐼 ↦ (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥)))))
245185feqmptd 6500 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑧𝑓 · 𝐴) = (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)))
246245oveq2d 6926 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg (𝑧𝑓 · 𝐴)) = (𝑇 Σg (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥))))
247246oveq2d 6926 . . . 4 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦 · (𝑇 Σg (𝑧𝑓 · 𝐴))) = (𝑦 · (𝑇 Σg (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)))))
248190, 244, 2473eqtr4d 2871 . . 3 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)) = (𝑦 · (𝑇 Σg (𝑧𝑓 · 𝐴))))
249 oveq1 6917 . . . . . 6 (𝑥 = (𝑦( ·𝑠𝐹)𝑧) → (𝑥𝑓 · 𝐴) = ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴))
250249oveq2d 6926 . . . . 5 (𝑥 = (𝑦( ·𝑠𝐹)𝑧) → (𝑇 Σg (𝑥𝑓 · 𝐴)) = (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)))
251 ovex 6942 . . . . 5 (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)) ∈ V
252250, 77, 251fvmpt 6533 . . . 4 ((𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵 → (𝐸‘(𝑦( ·𝑠𝐹)𝑧)) = (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)))
253195, 252syl 17 . . 3 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝐸‘(𝑦( ·𝑠𝐹)𝑧)) = (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)))
254174oveq2d 6926 . . . 4 (𝑧𝐵 → (𝑦 · (𝐸𝑧)) = (𝑦 · (𝑇 Σg (𝑧𝑓 · 𝐴))))
255254ad2antll 720 . . 3 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦 · (𝐸𝑧)) = (𝑦 · (𝑇 Σg (𝑧𝑓 · 𝐴))))
256248, 253, 2553eqtr4d 2871 . 2 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝐸‘(𝑦( ·𝑠𝐹)𝑧)) = (𝑦 · (𝐸𝑧)))
2571, 2, 3, 4, 5, 6, 15, 8, 18, 178, 256islmhmd 19405 1 (𝜑𝐸 ∈ (𝐹 LMHom 𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1656   ∈ wcel 2164  Vcvv 3414   ⊆ wss 3798   class class class wbr 4875   ↦ cmpt 4954  Fun wfun 6121   Fn wfn 6122  ⟶wf 6123  ‘cfv 6127  (class class class)co 6910   ∘𝑓 cof 7160   supp csupp 7564  Fincfn 8228   finSupp cfsupp 8550  Basecbs 16229  +gcplusg 16312  .rcmulr 16313  Scalarcsca 16315   ·𝑠 cvsca 16316  0gc0g 16460   Σg cgsu 16461  Grpcgrp 17783  CMndccmn 18553  Ringcrg 18908  LModclmod 19226   LMHom clmhm 19385   freeLMod cfrlm 20460 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-cnex 10315  ax-resscn 10316  ax-1cn 10317  ax-icn 10318  ax-addcl 10319  ax-addrcl 10320  ax-mulcl 10321  ax-mulrcl 10322  ax-mulcom 10323  ax-addass 10324  ax-mulass 10325  ax-distr 10326  ax-i2m1 10327  ax-1ne0 10328  ax-1rid 10329  ax-rnegex 10330  ax-rrecex 10331  ax-cnre 10332  ax-pre-lttri 10333  ax-pre-lttrn 10334  ax-pre-ltadd 10335  ax-pre-mulgt0 10336 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-int 4700  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-se 5306  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-isom 6136  df-riota 6871  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-of 7162  df-om 7332  df-1st 7433  df-2nd 7434  df-supp 7565  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-oadd 7835  df-er 8014  df-map 8129  df-ixp 8182  df-en 8229  df-dom 8230  df-sdom 8231  df-fin 8232  df-fsupp 8551  df-sup 8623  df-oi 8691  df-card 9085  df-pnf 10400  df-mnf 10401  df-xr 10402  df-ltxr 10403  df-le 10404  df-sub 10594  df-neg 10595  df-nn 11358  df-2 11421  df-3 11422  df-4 11423  df-5 11424  df-6 11425  df-7 11426  df-8 11427  df-9 11428  df-n0 11626  df-z 11712  df-dec 11829  df-uz 11976  df-fz 12627  df-fzo 12768  df-seq 13103  df-hash 13418  df-struct 16231  df-ndx 16232  df-slot 16233  df-base 16235  df-sets 16236  df-ress 16237  df-plusg 16325  df-mulr 16326  df-sca 16328  df-vsca 16329  df-ip 16330  df-tset 16331  df-ple 16332  df-ds 16334  df-hom 16336  df-cco 16337  df-0g 16462  df-gsum 16463  df-prds 16468  df-pws 16470  df-mgm 17602  df-sgrp 17644  df-mnd 17655  df-mhm 17695  df-submnd 17696  df-grp 17786  df-minusg 17787  df-sbg 17788  df-subg 17949  df-ghm 18016  df-cntz 18107  df-cmn 18555  df-abl 18556  df-mgp 18851  df-ur 18863  df-ring 18910  df-subrg 19141  df-lmod 19228  df-lss 19296  df-lmhm 19388  df-sra 19540  df-rgmod 19541  df-dsmm 20446  df-frlm 20461 This theorem is referenced by:  frlmup3  20513  frlmup4  20514  islindf5  20552  indlcim  20553  lnrfg  38531
 Copyright terms: Public domain W3C validator