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

Theorem frlmup1 20059
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 2621 . 2 ( ·𝑠𝐹) = ( ·𝑠𝐹)
3 frlmup.v . 2 · = ( ·𝑠𝑇)
4 eqid 2621 . 2 (Scalar‘𝐹) = (Scalar‘𝐹)
5 eqid 2621 . 2 (Scalar‘𝑇) = (Scalar‘𝑇)
6 eqid 2621 . 2 (Base‘(Scalar‘𝐹)) = (Base‘(Scalar‘𝐹))
7 frlmup.r . . . 4 (𝜑𝑅 = (Scalar‘𝑇))
8 frlmup.t . . . . 5 (𝜑𝑇 ∈ LMod)
95lmodring 18795 . . . . 5 (𝑇 ∈ LMod → (Scalar‘𝑇) ∈ Ring)
108, 9syl 17 . . . 4 (𝜑 → (Scalar‘𝑇) ∈ Ring)
117, 10eqeltrd 2698 . . 3 (𝜑𝑅 ∈ Ring)
12 frlmup.i . . 3 (𝜑𝐼𝑋)
13 frlmup.f . . . 4 𝐹 = (𝑅 freeLMod 𝐼)
1413frlmlmod 20015 . . 3 ((𝑅 ∈ Ring ∧ 𝐼𝑋) → 𝐹 ∈ LMod)
1511, 12, 14syl2anc 692 . 2 (𝜑𝐹 ∈ LMod)
1613frlmsca 20019 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼𝑋) → 𝑅 = (Scalar‘𝐹))
1711, 12, 16syl2anc 692 . . 3 (𝜑𝑅 = (Scalar‘𝐹))
187, 17eqtr3d 2657 . 2 (𝜑 → (Scalar‘𝑇) = (Scalar‘𝐹))
19 frlmup.c . . 3 𝐶 = (Base‘𝑇)
20 eqid 2621 . . 3 (+g𝐹) = (+g𝐹)
21 eqid 2621 . . 3 (+g𝑇) = (+g𝑇)
22 lmodgrp 18794 . . . 4 (𝐹 ∈ LMod → 𝐹 ∈ Grp)
2315, 22syl 17 . . 3 (𝜑𝐹 ∈ Grp)
24 lmodgrp 18794 . . . 4 (𝑇 ∈ LMod → 𝑇 ∈ Grp)
258, 24syl 17 . . 3 (𝜑𝑇 ∈ Grp)
26 eleq1 2686 . . . . . . 7 (𝑧 = 𝑥 → (𝑧𝐵𝑥𝐵))
2726anbi2d 739 . . . . . 6 (𝑧 = 𝑥 → ((𝜑𝑧𝐵) ↔ (𝜑𝑥𝐵)))
28 oveq1 6614 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧𝑓 · 𝐴) = (𝑥𝑓 · 𝐴))
2928oveq2d 6623 . . . . . . 7 (𝑧 = 𝑥 → (𝑇 Σg (𝑧𝑓 · 𝐴)) = (𝑇 Σg (𝑥𝑓 · 𝐴)))
3029eleq1d 2683 . . . . . 6 (𝑧 = 𝑥 → ((𝑇 Σg (𝑧𝑓 · 𝐴)) ∈ 𝐶 ↔ (𝑇 Σg (𝑥𝑓 · 𝐴)) ∈ 𝐶))
3127, 30imbi12d 334 . . . . 5 (𝑧 = 𝑥 → (((𝜑𝑧𝐵) → (𝑇 Σg (𝑧𝑓 · 𝐴)) ∈ 𝐶) ↔ ((𝜑𝑥𝐵) → (𝑇 Σg (𝑥𝑓 · 𝐴)) ∈ 𝐶)))
32 eqid 2621 . . . . . 6 (0g𝑇) = (0g𝑇)
33 lmodcmn 18835 . . . . . . . 8 (𝑇 ∈ LMod → 𝑇 ∈ CMnd)
348, 33syl 17 . . . . . . 7 (𝜑𝑇 ∈ CMnd)
3534adantr 481 . . . . . 6 ((𝜑𝑧𝐵) → 𝑇 ∈ CMnd)
3612adantr 481 . . . . . 6 ((𝜑𝑧𝐵) → 𝐼𝑋)
378ad2antrr 761 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑇 ∈ LMod)
38 simprl 793 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑥 ∈ (Base‘𝑅))
397fveq2d 6154 . . . . . . . . . 10 (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
4039ad2antrr 761 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
4138, 40eleqtrd 2700 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑥 ∈ (Base‘(Scalar‘𝑇)))
42 simprr 795 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → 𝑦𝐶)
43 eqid 2621 . . . . . . . . 9 (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇))
4419, 5, 3, 43lmodvscl 18804 . . . . . . . 8 ((𝑇 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑦𝐶) → (𝑥 · 𝑦) ∈ 𝐶)
4537, 41, 42, 44syl3anc 1323 . . . . . . 7 (((𝜑𝑧𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦𝐶)) → (𝑥 · 𝑦) ∈ 𝐶)
46 eqid 2621 . . . . . . . . 9 (Base‘𝑅) = (Base‘𝑅)
4713, 46, 1frlmbasf 20026 . . . . . . . 8 ((𝐼𝑋𝑧𝐵) → 𝑧:𝐼⟶(Base‘𝑅))
4812, 47sylan 488 . . . . . . 7 ((𝜑𝑧𝐵) → 𝑧:𝐼⟶(Base‘𝑅))
49 frlmup.a . . . . . . . 8 (𝜑𝐴:𝐼𝐶)
5049adantr 481 . . . . . . 7 ((𝜑𝑧𝐵) → 𝐴:𝐼𝐶)
51 inidm 3802 . . . . . . 7 (𝐼𝐼) = 𝐼
5245, 48, 50, 36, 36, 51off 6868 . . . . . 6 ((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴):𝐼𝐶)
53 ovex 6635 . . . . . . . 8 (𝑧𝑓 · 𝐴) ∈ V
5453a1i 11 . . . . . . 7 ((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴) ∈ V)
55 ffun 6007 . . . . . . . 8 ((𝑧𝑓 · 𝐴):𝐼𝐶 → Fun (𝑧𝑓 · 𝐴))
5652, 55syl 17 . . . . . . 7 ((𝜑𝑧𝐵) → Fun (𝑧𝑓 · 𝐴))
57 fvex 6160 . . . . . . . 8 (0g𝑇) ∈ V
5857a1i 11 . . . . . . 7 ((𝜑𝑧𝐵) → (0g𝑇) ∈ V)
59 eqid 2621 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
6013, 59, 1frlmbasfsupp 20024 . . . . . . . . . 10 ((𝐼𝑋𝑧𝐵) → 𝑧 finSupp (0g𝑅))
6112, 60sylan 488 . . . . . . . . 9 ((𝜑𝑧𝐵) → 𝑧 finSupp (0g𝑅))
627fveq2d 6154 . . . . . . . . . . . 12 (𝜑 → (0g𝑅) = (0g‘(Scalar‘𝑇)))
6362eqcomd 2627 . . . . . . . . . . 11 (𝜑 → (0g‘(Scalar‘𝑇)) = (0g𝑅))
6463breq2d 4627 . . . . . . . . . 10 (𝜑 → (𝑧 finSupp (0g‘(Scalar‘𝑇)) ↔ 𝑧 finSupp (0g𝑅)))
6564adantr 481 . . . . . . . . 9 ((𝜑𝑧𝐵) → (𝑧 finSupp (0g‘(Scalar‘𝑇)) ↔ 𝑧 finSupp (0g𝑅)))
6661, 65mpbird 247 . . . . . . . 8 ((𝜑𝑧𝐵) → 𝑧 finSupp (0g‘(Scalar‘𝑇)))
6766fsuppimpd 8229 . . . . . . 7 ((𝜑𝑧𝐵) → (𝑧 supp (0g‘(Scalar‘𝑇))) ∈ Fin)
68 ssid 3605 . . . . . . . . 9 (𝑧 supp (0g‘(Scalar‘𝑇))) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇)))
6968a1i 11 . . . . . . . 8 ((𝜑𝑧𝐵) → (𝑧 supp (0g‘(Scalar‘𝑇))) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))
708ad2antrr 761 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ 𝑤𝐶) → 𝑇 ∈ LMod)
71 eqid 2621 . . . . . . . . . 10 (0g‘(Scalar‘𝑇)) = (0g‘(Scalar‘𝑇))
7219, 5, 3, 71, 32lmod0vs 18820 . . . . . . . . 9 ((𝑇 ∈ LMod ∧ 𝑤𝐶) → ((0g‘(Scalar‘𝑇)) · 𝑤) = (0g𝑇))
7370, 72sylancom 700 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ 𝑤𝐶) → ((0g‘(Scalar‘𝑇)) · 𝑤) = (0g𝑇))
74 fvex 6160 . . . . . . . . 9 (0g‘(Scalar‘𝑇)) ∈ V
7574a1i 11 . . . . . . . 8 ((𝜑𝑧𝐵) → (0g‘(Scalar‘𝑇)) ∈ V)
7669, 73, 48, 50, 36, 75suppssof1 7276 . . . . . . 7 ((𝜑𝑧𝐵) → ((𝑧𝑓 · 𝐴) supp (0g𝑇)) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))
77 suppssfifsupp 8237 . . . . . . 7 ((((𝑧𝑓 · 𝐴) ∈ V ∧ Fun (𝑧𝑓 · 𝐴) ∧ (0g𝑇) ∈ V) ∧ ((𝑧 supp (0g‘(Scalar‘𝑇))) ∈ Fin ∧ ((𝑧𝑓 · 𝐴) supp (0g𝑇)) ⊆ (𝑧 supp (0g‘(Scalar‘𝑇))))) → (𝑧𝑓 · 𝐴) finSupp (0g𝑇))
7854, 56, 58, 67, 76, 77syl32anc 1331 . . . . . 6 ((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴) finSupp (0g𝑇))
7919, 32, 35, 36, 52, 78gsumcl 18240 . . . . 5 ((𝜑𝑧𝐵) → (𝑇 Σg (𝑧𝑓 · 𝐴)) ∈ 𝐶)
8031, 79chvarv 2262 . . . 4 ((𝜑𝑥𝐵) → (𝑇 Σg (𝑥𝑓 · 𝐴)) ∈ 𝐶)
81 frlmup.e . . . 4 𝐸 = (𝑥𝐵 ↦ (𝑇 Σg (𝑥𝑓 · 𝐴)))
8280, 81fmptd 6343 . . 3 (𝜑𝐸:𝐵𝐶)
8334adantr 481 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑇 ∈ CMnd)
8412adantr 481 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝐼𝑋)
85 eleq1 2686 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧𝐵𝑦𝐵))
8685anbi2d 739 . . . . . . . 8 (𝑧 = 𝑦 → ((𝜑𝑧𝐵) ↔ (𝜑𝑦𝐵)))
87 oveq1 6614 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧𝑓 · 𝐴) = (𝑦𝑓 · 𝐴))
8887feq1d 5989 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧𝑓 · 𝐴):𝐼𝐶 ↔ (𝑦𝑓 · 𝐴):𝐼𝐶))
8986, 88imbi12d 334 . . . . . . 7 (𝑧 = 𝑦 → (((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴):𝐼𝐶) ↔ ((𝜑𝑦𝐵) → (𝑦𝑓 · 𝐴):𝐼𝐶)))
9089, 52chvarv 2262 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦𝑓 · 𝐴):𝐼𝐶)
9190adantrr 752 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦𝑓 · 𝐴):𝐼𝐶)
9252adantrl 751 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑧𝑓 · 𝐴):𝐼𝐶)
9387breq1d 4625 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑧𝑓 · 𝐴) finSupp (0g𝑇) ↔ (𝑦𝑓 · 𝐴) finSupp (0g𝑇)))
9486, 93imbi12d 334 . . . . . . 7 (𝑧 = 𝑦 → (((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴) finSupp (0g𝑇)) ↔ ((𝜑𝑦𝐵) → (𝑦𝑓 · 𝐴) finSupp (0g𝑇))))
9594, 78chvarv 2262 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦𝑓 · 𝐴) finSupp (0g𝑇))
9695adantrr 752 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦𝑓 · 𝐴) finSupp (0g𝑇))
9778adantrl 751 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑧𝑓 · 𝐴) finSupp (0g𝑇))
9819, 32, 21, 83, 84, 91, 92, 96, 97gsumadd 18247 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑇 Σg ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))) = ((𝑇 Σg (𝑦𝑓 · 𝐴))(+g𝑇)(𝑇 Σg (𝑧𝑓 · 𝐴))))
991, 20lmodvacl 18801 . . . . . . . 8 ((𝐹 ∈ LMod ∧ 𝑦𝐵𝑧𝐵) → (𝑦(+g𝐹)𝑧) ∈ 𝐵)
100993expb 1263 . . . . . . 7 ((𝐹 ∈ LMod ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(+g𝐹)𝑧) ∈ 𝐵)
10115, 100sylan 488 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(+g𝐹)𝑧) ∈ 𝐵)
102 oveq1 6614 . . . . . . . 8 (𝑥 = (𝑦(+g𝐹)𝑧) → (𝑥𝑓 · 𝐴) = ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴))
103102oveq2d 6623 . . . . . . 7 (𝑥 = (𝑦(+g𝐹)𝑧) → (𝑇 Σg (𝑥𝑓 · 𝐴)) = (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴)))
104 ovex 6635 . . . . . . 7 (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴)) ∈ V
105103, 81, 104fvmpt 6241 . . . . . 6 ((𝑦(+g𝐹)𝑧) ∈ 𝐵 → (𝐸‘(𝑦(+g𝐹)𝑧)) = (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴)))
106101, 105syl 17 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸‘(𝑦(+g𝐹)𝑧)) = (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴)))
10711adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑅 ∈ Ring)
108 simprl 793 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑦𝐵)
109 simprr 795 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑧𝐵)
110 eqid 2621 . . . . . . . . 9 (+g𝑅) = (+g𝑅)
11113, 1, 107, 84, 108, 109, 110, 20frlmplusgval 20029 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(+g𝐹)𝑧) = (𝑦𝑓 (+g𝑅)𝑧))
112111oveq1d 6622 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴) = ((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴))
11313, 46, 1frlmbasf 20026 . . . . . . . . . . . . 13 ((𝐼𝑋𝑦𝐵) → 𝑦:𝐼⟶(Base‘𝑅))
11412, 113sylan 488 . . . . . . . . . . . 12 ((𝜑𝑦𝐵) → 𝑦:𝐼⟶(Base‘𝑅))
115114adantrr 752 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑦:𝐼⟶(Base‘𝑅))
116 ffn 6004 . . . . . . . . . . 11 (𝑦:𝐼⟶(Base‘𝑅) → 𝑦 Fn 𝐼)
117115, 116syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑦 Fn 𝐼)
11848adantrl 751 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑧:𝐼⟶(Base‘𝑅))
119 ffn 6004 . . . . . . . . . . 11 (𝑧:𝐼⟶(Base‘𝑅) → 𝑧 Fn 𝐼)
120118, 119syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝑧 Fn 𝐼)
121117, 120, 84, 84, 51offn 6864 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦𝑓 (+g𝑅)𝑧) Fn 𝐼)
122 ffn 6004 . . . . . . . . . . 11 (𝐴:𝐼𝐶𝐴 Fn 𝐼)
12349, 122syl 17 . . . . . . . . . 10 (𝜑𝐴 Fn 𝐼)
124123adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝐴 Fn 𝐼)
125121, 124, 84, 84, 51offn 6864 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴) Fn 𝐼)
126 ffn 6004 . . . . . . . . . . 11 ((𝑦𝑓 · 𝐴):𝐼𝐶 → (𝑦𝑓 · 𝐴) Fn 𝐼)
12790, 126syl 17 . . . . . . . . . 10 ((𝜑𝑦𝐵) → (𝑦𝑓 · 𝐴) Fn 𝐼)
128127adantrr 752 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦𝑓 · 𝐴) Fn 𝐼)
129 ffn 6004 . . . . . . . . . . 11 ((𝑧𝑓 · 𝐴):𝐼𝐶 → (𝑧𝑓 · 𝐴) Fn 𝐼)
13052, 129syl 17 . . . . . . . . . 10 ((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴) Fn 𝐼)
131130adantrl 751 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑧𝑓 · 𝐴) Fn 𝐼)
132128, 131, 84, 84, 51offn 6864 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴)) Fn 𝐼)
1337fveq2d 6154 . . . . . . . . . . . . . 14 (𝜑 → (+g𝑅) = (+g‘(Scalar‘𝑇)))
134133ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (+g𝑅) = (+g‘(Scalar‘𝑇)))
135134oveqd 6624 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦𝑥)(+g𝑅)(𝑧𝑥)) = ((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)))
136135oveq1d 6622 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑥)(+g𝑅)(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)))
1378ad2antrr 761 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑇 ∈ LMod)
138115ffvelrnda 6317 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦𝑥) ∈ (Base‘𝑅))
13939ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
140138, 139eleqtrd 2700 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦𝑥) ∈ (Base‘(Scalar‘𝑇)))
141118ffvelrnda 6317 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘𝑅))
142141, 139eleqtrd 2700 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)))
14349adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → 𝐴:𝐼𝐶)
144143ffvelrnda 6317 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝐴𝑥) ∈ 𝐶)
145 eqid 2621 . . . . . . . . . . . . 13 (+g‘(Scalar‘𝑇)) = (+g‘(Scalar‘𝑇))
14619, 21, 5, 3, 43, 145lmodvsdir 18811 . . . . . . . . . . . 12 ((𝑇 ∈ LMod ∧ ((𝑦𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐴𝑥) ∈ 𝐶)) → (((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
147137, 140, 142, 144, 146syl13anc 1325 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑥)(+g‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
148136, 147eqtrd 2655 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑥)(+g𝑅)(𝑧𝑥)) · (𝐴𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
149117adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 Fn 𝐼)
150120adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑧 Fn 𝐼)
15112ad2antrr 761 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝐼𝑋)
152 simpr 477 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝑥𝐼)
153 fnfvof 6867 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼𝑧 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → ((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) = ((𝑦𝑥)(+g𝑅)(𝑧𝑥)))
154149, 150, 151, 152, 153syl22anc 1324 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) = ((𝑦𝑥)(+g𝑅)(𝑧𝑥)))
155154oveq1d 6622 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)) = (((𝑦𝑥)(+g𝑅)(𝑧𝑥)) · (𝐴𝑥)))
156123ad2antrr 761 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → 𝐴 Fn 𝐼)
157 fnfvof 6867 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → ((𝑦𝑓 · 𝐴)‘𝑥) = ((𝑦𝑥) · (𝐴𝑥)))
158149, 156, 151, 152, 157syl22anc 1324 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦𝑓 · 𝐴)‘𝑥) = ((𝑦𝑥) · (𝐴𝑥)))
159 fnfvof 6867 . . . . . . . . . . . 12 (((𝑧 Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → ((𝑧𝑓 · 𝐴)‘𝑥) = ((𝑧𝑥) · (𝐴𝑥)))
160150, 156, 151, 152, 159syl22anc 1324 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑧𝑓 · 𝐴)‘𝑥) = ((𝑧𝑥) · (𝐴𝑥)))
161158, 160oveq12d 6625 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 · 𝐴)‘𝑥)(+g𝑇)((𝑧𝑓 · 𝐴)‘𝑥)) = (((𝑦𝑥) · (𝐴𝑥))(+g𝑇)((𝑧𝑥) · (𝐴𝑥))))
162148, 155, 1613eqtr4d 2665 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)) = (((𝑦𝑓 · 𝐴)‘𝑥)(+g𝑇)((𝑧𝑓 · 𝐴)‘𝑥)))
163121adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦𝑓 (+g𝑅)𝑧) Fn 𝐼)
164 fnfvof 6867 . . . . . . . . . 10 ((((𝑦𝑓 (+g𝑅)𝑧) Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → (((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)))
165163, 156, 151, 152, 164syl22anc 1324 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦𝑓 (+g𝑅)𝑧)‘𝑥) · (𝐴𝑥)))
166128adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦𝑓 · 𝐴) Fn 𝐼)
167131adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑓 · 𝐴) Fn 𝐼)
168 fnfvof 6867 . . . . . . . . . 10 ((((𝑦𝑓 · 𝐴) Fn 𝐼 ∧ (𝑧𝑓 · 𝐴) Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → (((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))‘𝑥) = (((𝑦𝑓 · 𝐴)‘𝑥)(+g𝑇)((𝑧𝑓 · 𝐴)‘𝑥)))
169166, 167, 151, 152, 168syl22anc 1324 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))‘𝑥) = (((𝑦𝑓 · 𝐴)‘𝑥)(+g𝑇)((𝑧𝑓 · 𝐴)‘𝑥)))
170162, 165, 1693eqtr4d 2665 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))‘𝑥))
171125, 132, 170eqfnfvd 6272 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦𝑓 (+g𝑅)𝑧) ∘𝑓 · 𝐴) = ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴)))
172112, 171eqtrd 2655 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴) = ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴)))
173172oveq2d 6623 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑇 Σg ((𝑦(+g𝐹)𝑧) ∘𝑓 · 𝐴)) = (𝑇 Σg ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))))
174106, 173eqtrd 2655 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸‘(𝑦(+g𝐹)𝑧)) = (𝑇 Σg ((𝑦𝑓 · 𝐴) ∘𝑓 (+g𝑇)(𝑧𝑓 · 𝐴))))
175 oveq1 6614 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝑓 · 𝐴) = (𝑦𝑓 · 𝐴))
176175oveq2d 6623 . . . . . . 7 (𝑥 = 𝑦 → (𝑇 Σg (𝑥𝑓 · 𝐴)) = (𝑇 Σg (𝑦𝑓 · 𝐴)))
177 ovex 6635 . . . . . . 7 (𝑇 Σg (𝑦𝑓 · 𝐴)) ∈ V
178176, 81, 177fvmpt 6241 . . . . . 6 (𝑦𝐵 → (𝐸𝑦) = (𝑇 Σg (𝑦𝑓 · 𝐴)))
179178ad2antrl 763 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸𝑦) = (𝑇 Σg (𝑦𝑓 · 𝐴)))
180 oveq1 6614 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥𝑓 · 𝐴) = (𝑧𝑓 · 𝐴))
181180oveq2d 6623 . . . . . . 7 (𝑥 = 𝑧 → (𝑇 Σg (𝑥𝑓 · 𝐴)) = (𝑇 Σg (𝑧𝑓 · 𝐴)))
182 ovex 6635 . . . . . . 7 (𝑇 Σg (𝑧𝑓 · 𝐴)) ∈ V
183181, 81, 182fvmpt 6241 . . . . . 6 (𝑧𝐵 → (𝐸𝑧) = (𝑇 Σg (𝑧𝑓 · 𝐴)))
184183ad2antll 764 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸𝑧) = (𝑇 Σg (𝑧𝑓 · 𝐴)))
185179, 184oveq12d 6625 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → ((𝐸𝑦)(+g𝑇)(𝐸𝑧)) = ((𝑇 Σg (𝑦𝑓 · 𝐴))(+g𝑇)(𝑇 Σg (𝑧𝑓 · 𝐴))))
18698, 174, 1853eqtr4d 2665 . . 3 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝐸‘(𝑦(+g𝐹)𝑧)) = ((𝐸𝑦)(+g𝑇)(𝐸𝑧)))
1871, 19, 20, 21, 23, 25, 82, 186isghmd 17593 . 2 (𝜑𝐸 ∈ (𝐹 GrpHom 𝑇))
1888adantr 481 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑇 ∈ LMod)
18912adantr 481 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝐼𝑋)
19018fveq2d 6154 . . . . . . . 8 (𝜑 → (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝐹)))
191190eleq2d 2684 . . . . . . 7 (𝜑 → (𝑦 ∈ (Base‘(Scalar‘𝑇)) ↔ 𝑦 ∈ (Base‘(Scalar‘𝐹))))
192191biimpar 502 . . . . . 6 ((𝜑𝑦 ∈ (Base‘(Scalar‘𝐹))) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
193192adantrr 752 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
19452adantrl 751 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑧𝑓 · 𝐴):𝐼𝐶)
195194ffvelrnda 6317 . . . . 5 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑧𝑓 · 𝐴)‘𝑥) ∈ 𝐶)
19652feqmptd 6208 . . . . . . 7 ((𝜑𝑧𝐵) → (𝑧𝑓 · 𝐴) = (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)))
197196, 78eqbrtrrd 4639 . . . . . 6 ((𝜑𝑧𝐵) → (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)) finSupp (0g𝑇))
198197adantrl 751 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)) finSupp (0g𝑇))
19919, 5, 43, 32, 21, 3, 188, 189, 193, 195, 198gsumvsmul 18851 . . . 4 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg (𝑥𝐼 ↦ (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥)))) = (𝑦 · (𝑇 Σg (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)))))
20015adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝐹 ∈ LMod)
201 simprl 793 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑦 ∈ (Base‘(Scalar‘𝐹)))
202 simprr 795 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑧𝐵)
2031, 4, 2, 6lmodvscl 18804 . . . . . . . . . . . 12 ((𝐹 ∈ LMod ∧ 𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵) → (𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵)
204200, 201, 202, 203syl3anc 1323 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵)
20513, 46, 1frlmbasf 20026 . . . . . . . . . . 11 ((𝐼𝑋 ∧ (𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵) → (𝑦( ·𝑠𝐹)𝑧):𝐼⟶(Base‘𝑅))
206189, 204, 205syl2anc 692 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦( ·𝑠𝐹)𝑧):𝐼⟶(Base‘𝑅))
207 ffn 6004 . . . . . . . . . 10 ((𝑦( ·𝑠𝐹)𝑧):𝐼⟶(Base‘𝑅) → (𝑦( ·𝑠𝐹)𝑧) Fn 𝐼)
208206, 207syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦( ·𝑠𝐹)𝑧) Fn 𝐼)
209123adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝐴 Fn 𝐼)
210208, 209, 189, 189, 51offn 6864 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴) Fn 𝐼)
211 dffn2 6006 . . . . . . . 8 (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴) Fn 𝐼 ↔ ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴):𝐼⟶V)
212210, 211sylib 208 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴):𝐼⟶V)
213212feqmptd 6208 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴) = (𝑥𝐼 ↦ (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥)))
2147fveq2d 6154 . . . . . . . . . . . 12 (𝜑 → (.r𝑅) = (.r‘(Scalar‘𝑇)))
215214ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (.r𝑅) = (.r‘(Scalar‘𝑇)))
216215oveqd 6624 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦(.r𝑅)(𝑧𝑥)) = (𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)))
217216oveq1d 6622 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)) = ((𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)))
2188ad2antrr 761 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑇 ∈ LMod)
219 simplrl 799 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 ∈ (Base‘(Scalar‘𝐹)))
220190ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝐹)))
221219, 220eleqtrrd 2701 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 ∈ (Base‘(Scalar‘𝑇)))
22248ffvelrnda 6317 . . . . . . . . . . . 12 (((𝜑𝑧𝐵) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘𝑅))
22339ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑧𝐵) ∧ 𝑥𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑇)))
224222, 223eleqtrd 2700 . . . . . . . . . . 11 (((𝜑𝑧𝐵) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)))
225224adantlrl 755 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)))
22649ffvelrnda 6317 . . . . . . . . . . 11 ((𝜑𝑥𝐼) → (𝐴𝑥) ∈ 𝐶)
227226adantlr 750 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝐴𝑥) ∈ 𝐶)
228 eqid 2621 . . . . . . . . . . 11 (.r‘(Scalar‘𝑇)) = (.r‘(Scalar‘𝑇))
22919, 5, 3, 43, 228lmodvsass 18812 . . . . . . . . . 10 ((𝑇 ∈ LMod ∧ (𝑦 ∈ (Base‘(Scalar‘𝑇)) ∧ (𝑧𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐴𝑥) ∈ 𝐶)) → ((𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
230218, 221, 225, 227, 229syl13anc 1325 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦(.r‘(Scalar‘𝑇))(𝑧𝑥)) · (𝐴𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
231217, 230eqtrd 2655 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
232208adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦( ·𝑠𝐹)𝑧) Fn 𝐼)
233123ad2antrr 761 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝐴 Fn 𝐼)
23412ad2antrr 761 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝐼𝑋)
235 simpr 477 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑥𝐼)
236 fnfvof 6867 . . . . . . . . . 10 ((((𝑦( ·𝑠𝐹)𝑧) Fn 𝐼𝐴 Fn 𝐼) ∧ (𝐼𝑋𝑥𝐼)) → (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦( ·𝑠𝐹)𝑧)‘𝑥) · (𝐴𝑥)))
237232, 233, 234, 235, 236syl22anc 1324 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (((𝑦( ·𝑠𝐹)𝑧)‘𝑥) · (𝐴𝑥)))
23817fveq2d 6154 . . . . . . . . . . . . 13 (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝐹)))
239238ad2antrr 761 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝐹)))
240219, 239eleqtrrd 2701 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑦 ∈ (Base‘𝑅))
241 simplrr 800 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑧𝐵)
242 eqid 2621 . . . . . . . . . . 11 (.r𝑅) = (.r𝑅)
24313, 1, 46, 234, 240, 241, 235, 2, 242frlmvscaval 20032 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑦( ·𝑠𝐹)𝑧)‘𝑥) = (𝑦(.r𝑅)(𝑧𝑥)))
244243oveq1d 6622 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧)‘𝑥) · (𝐴𝑥)) = ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)))
245237, 244eqtrd 2655 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = ((𝑦(.r𝑅)(𝑧𝑥)) · (𝐴𝑥)))
24648, 119syl 17 . . . . . . . . . . . 12 ((𝜑𝑧𝐵) → 𝑧 Fn 𝐼)
247246adantrl 751 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → 𝑧 Fn 𝐼)
248247adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → 𝑧 Fn 𝐼)
249248, 233, 234, 235, 159syl22anc 1324 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → ((𝑧𝑓 · 𝐴)‘𝑥) = ((𝑧𝑥) · (𝐴𝑥)))
250249oveq2d 6623 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥)) = (𝑦 · ((𝑧𝑥) · (𝐴𝑥))))
251231, 245, 2503eqtr4d 2665 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) ∧ 𝑥𝐼) → (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥) = (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥)))
252251mpteq2dva 4706 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑥𝐼 ↦ (((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)‘𝑥)) = (𝑥𝐼 ↦ (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥))))
253213, 252eqtrd 2655 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴) = (𝑥𝐼 ↦ (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥))))
254253oveq2d 6623 . . . 4 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)) = (𝑇 Σg (𝑥𝐼 ↦ (𝑦 · ((𝑧𝑓 · 𝐴)‘𝑥)))))
255194feqmptd 6208 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑧𝑓 · 𝐴) = (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)))
256255oveq2d 6623 . . . . 5 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg (𝑧𝑓 · 𝐴)) = (𝑇 Σg (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥))))
257256oveq2d 6623 . . . 4 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦 · (𝑇 Σg (𝑧𝑓 · 𝐴))) = (𝑦 · (𝑇 Σg (𝑥𝐼 ↦ ((𝑧𝑓 · 𝐴)‘𝑥)))))
258199, 254, 2573eqtr4d 2665 . . 3 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)) = (𝑦 · (𝑇 Σg (𝑧𝑓 · 𝐴))))
259 oveq1 6614 . . . . . 6 (𝑥 = (𝑦( ·𝑠𝐹)𝑧) → (𝑥𝑓 · 𝐴) = ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴))
260259oveq2d 6623 . . . . 5 (𝑥 = (𝑦( ·𝑠𝐹)𝑧) → (𝑇 Σg (𝑥𝑓 · 𝐴)) = (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)))
261 ovex 6635 . . . . 5 (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)) ∈ V
262260, 81, 261fvmpt 6241 . . . 4 ((𝑦( ·𝑠𝐹)𝑧) ∈ 𝐵 → (𝐸‘(𝑦( ·𝑠𝐹)𝑧)) = (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)))
263204, 262syl 17 . . 3 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝐸‘(𝑦( ·𝑠𝐹)𝑧)) = (𝑇 Σg ((𝑦( ·𝑠𝐹)𝑧) ∘𝑓 · 𝐴)))
264183oveq2d 6623 . . . 4 (𝑧𝐵 → (𝑦 · (𝐸𝑧)) = (𝑦 · (𝑇 Σg (𝑧𝑓 · 𝐴))))
265264ad2antll 764 . . 3 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝑦 · (𝐸𝑧)) = (𝑦 · (𝑇 Σg (𝑧𝑓 · 𝐴))))
266258, 263, 2653eqtr4d 2665 . 2 ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧𝐵)) → (𝐸‘(𝑦( ·𝑠𝐹)𝑧)) = (𝑦 · (𝐸𝑧)))
2671, 2, 3, 4, 5, 6, 15, 8, 18, 187, 266islmhmd 18961 1 (𝜑𝐸 ∈ (𝐹 LMHom 𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  Vcvv 3186  wss 3556   class class class wbr 4615  cmpt 4675  Fun wfun 5843   Fn wfn 5844  wf 5845  cfv 5849  (class class class)co 6607  𝑓 cof 6851   supp csupp 7243  Fincfn 7902   finSupp cfsupp 8222  Basecbs 15784  +gcplusg 15865  .rcmulr 15866  Scalarcsca 15868   ·𝑠 cvsca 15869  0gc0g 16024   Σg cgsu 16025  Grpcgrp 17346  CMndccmn 18117  Ringcrg 18471  LModclmod 18787   LMHom clmhm 18941   freeLMod cfrlm 20012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-se 5036  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-isom 5858  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-of 6853  df-om 7016  df-1st 7116  df-2nd 7117  df-supp 7244  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-oadd 7512  df-er 7690  df-map 7807  df-ixp 7856  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-fsupp 8223  df-sup 8295  df-oi 8362  df-card 8712  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-nn 10968  df-2 11026  df-3 11027  df-4 11028  df-5 11029  df-6 11030  df-7 11031  df-8 11032  df-9 11033  df-n0 11240  df-z 11325  df-dec 11441  df-uz 11635  df-fz 12272  df-fzo 12410  df-seq 12745  df-hash 13061  df-struct 15786  df-ndx 15787  df-slot 15788  df-base 15789  df-sets 15790  df-ress 15791  df-plusg 15878  df-mulr 15879  df-sca 15881  df-vsca 15882  df-ip 15883  df-tset 15884  df-ple 15885  df-ds 15888  df-hom 15890  df-cco 15891  df-0g 16026  df-gsum 16027  df-prds 16032  df-pws 16034  df-mgm 17166  df-sgrp 17208  df-mnd 17219  df-mhm 17259  df-submnd 17260  df-grp 17349  df-minusg 17350  df-sbg 17351  df-subg 17515  df-ghm 17582  df-cntz 17674  df-cmn 18119  df-abl 18120  df-mgp 18414  df-ur 18426  df-ring 18473  df-subrg 18702  df-lmod 18789  df-lss 18855  df-lmhm 18944  df-sra 19094  df-rgmod 19095  df-dsmm 19998  df-frlm 20013
This theorem is referenced by:  frlmup3  20061  frlmup4  20062  islindf5  20100  indlcim  20101  lnrfg  37191
  Copyright terms: Public domain W3C validator