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

Theorem frlmup1 21220
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 2737 . 2 ( ·𝑠 β€˜πΉ) = ( ·𝑠 β€˜πΉ)
3 frlmup.v . 2 Β· = ( ·𝑠 β€˜π‘‡)
4 eqid 2737 . 2 (Scalarβ€˜πΉ) = (Scalarβ€˜πΉ)
5 eqid 2737 . 2 (Scalarβ€˜π‘‡) = (Scalarβ€˜π‘‡)
6 eqid 2737 . 2 (Baseβ€˜(Scalarβ€˜πΉ)) = (Baseβ€˜(Scalarβ€˜πΉ))
7 frlmup.r . . . 4 (πœ‘ β†’ 𝑅 = (Scalarβ€˜π‘‡))
8 frlmup.t . . . . 5 (πœ‘ β†’ 𝑇 ∈ LMod)
95lmodring 20346 . . . . 5 (𝑇 ∈ LMod β†’ (Scalarβ€˜π‘‡) ∈ Ring)
108, 9syl 17 . . . 4 (πœ‘ β†’ (Scalarβ€˜π‘‡) ∈ Ring)
117, 10eqeltrd 2838 . . 3 (πœ‘ β†’ 𝑅 ∈ Ring)
12 frlmup.i . . 3 (πœ‘ β†’ 𝐼 ∈ 𝑋)
13 frlmup.f . . . 4 𝐹 = (𝑅 freeLMod 𝐼)
1413frlmlmod 21171 . . 3 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) β†’ 𝐹 ∈ LMod)
1511, 12, 14syl2anc 585 . 2 (πœ‘ β†’ 𝐹 ∈ LMod)
1613frlmsca 21175 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) β†’ 𝑅 = (Scalarβ€˜πΉ))
1711, 12, 16syl2anc 585 . . 3 (πœ‘ β†’ 𝑅 = (Scalarβ€˜πΉ))
187, 17eqtr3d 2779 . 2 (πœ‘ β†’ (Scalarβ€˜π‘‡) = (Scalarβ€˜πΉ))
19 frlmup.c . . 3 𝐢 = (Baseβ€˜π‘‡)
20 eqid 2737 . . 3 (+gβ€˜πΉ) = (+gβ€˜πΉ)
21 eqid 2737 . . 3 (+gβ€˜π‘‡) = (+gβ€˜π‘‡)
22 lmodgrp 20345 . . . 4 (𝐹 ∈ LMod β†’ 𝐹 ∈ Grp)
2315, 22syl 17 . . 3 (πœ‘ β†’ 𝐹 ∈ Grp)
24 lmodgrp 20345 . . . 4 (𝑇 ∈ LMod β†’ 𝑇 ∈ Grp)
258, 24syl 17 . . 3 (πœ‘ β†’ 𝑇 ∈ Grp)
26 eleq1w 2821 . . . . . . 7 (𝑧 = π‘₯ β†’ (𝑧 ∈ 𝐡 ↔ π‘₯ ∈ 𝐡))
2726anbi2d 630 . . . . . 6 (𝑧 = π‘₯ β†’ ((πœ‘ ∧ 𝑧 ∈ 𝐡) ↔ (πœ‘ ∧ π‘₯ ∈ 𝐡)))
28 oveq1 7369 . . . . . . . 8 (𝑧 = π‘₯ β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∘f Β· 𝐴))
2928oveq2d 7378 . . . . . . 7 (𝑧 = π‘₯ β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)))
3029eleq1d 2823 . . . . . 6 (𝑧 = π‘₯ β†’ ((𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ 𝐢 ↔ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) ∈ 𝐢))
3127, 30imbi12d 345 . . . . 5 (𝑧 = π‘₯ β†’ (((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ 𝐢) ↔ ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) ∈ 𝐢)))
32 eqid 2737 . . . . . 6 (0gβ€˜π‘‡) = (0gβ€˜π‘‡)
33 lmodcmn 20386 . . . . . . . 8 (𝑇 ∈ LMod β†’ 𝑇 ∈ CMnd)
348, 33syl 17 . . . . . . 7 (πœ‘ β†’ 𝑇 ∈ CMnd)
3534adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑇 ∈ CMnd)
3612adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝐼 ∈ 𝑋)
378ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ 𝑇 ∈ LMod)
38 simprl 770 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ π‘₯ ∈ (Baseβ€˜π‘…))
397fveq2d 6851 . . . . . . . . . 10 (πœ‘ β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
4039ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
4138, 40eleqtrd 2840 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
42 simprr 772 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ 𝑦 ∈ 𝐢)
43 eqid 2737 . . . . . . . . 9 (Baseβ€˜(Scalarβ€˜π‘‡)) = (Baseβ€˜(Scalarβ€˜π‘‡))
4419, 5, 3, 43lmodvscl 20355 . . . . . . . 8 ((𝑇 ∈ LMod ∧ π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ Β· 𝑦) ∈ 𝐢)
4537, 41, 42, 44syl3anc 1372 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯ Β· 𝑦) ∈ 𝐢)
46 eqid 2737 . . . . . . . . 9 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
4713, 46, 1frlmbasf 21182 . . . . . . . 8 ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐡) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
4812, 47sylan 581 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
49 frlmup.a . . . . . . . 8 (πœ‘ β†’ 𝐴:𝐼⟢𝐢)
5049adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝐴:𝐼⟢𝐢)
51 inidm 4183 . . . . . . 7 (𝐼 ∩ 𝐼) = 𝐼
5245, 48, 50, 36, 36, 51off 7640 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢)
53 ovexd 7397 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) ∈ V)
5452ffund 6677 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ Fun (𝑧 ∘f Β· 𝐴))
55 fvexd 6862 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (0gβ€˜π‘‡) ∈ V)
56 eqid 2737 . . . . . . . . . . 11 (0gβ€˜π‘…) = (0gβ€˜π‘…)
5713, 56, 1frlmbasfsupp 21180 . . . . . . . . . 10 ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜π‘…))
5812, 57sylan 581 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜π‘…))
597fveq2d 6851 . . . . . . . . . . . 12 (πœ‘ β†’ (0gβ€˜π‘…) = (0gβ€˜(Scalarβ€˜π‘‡)))
6059eqcomd 2743 . . . . . . . . . . 11 (πœ‘ β†’ (0gβ€˜(Scalarβ€˜π‘‡)) = (0gβ€˜π‘…))
6160breq2d 5122 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)) ↔ 𝑧 finSupp (0gβ€˜π‘…)))
6261adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)) ↔ 𝑧 finSupp (0gβ€˜π‘…)))
6358, 62mpbird 257 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)))
6463fsuppimpd 9319 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))) ∈ Fin)
65 ssidd 3972 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))) βŠ† (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))))
668ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ 𝑀 ∈ 𝐢) β†’ 𝑇 ∈ LMod)
67 eqid 2737 . . . . . . . . . 10 (0gβ€˜(Scalarβ€˜π‘‡)) = (0gβ€˜(Scalarβ€˜π‘‡))
6819, 5, 3, 67, 32lmod0vs 20371 . . . . . . . . 9 ((𝑇 ∈ LMod ∧ 𝑀 ∈ 𝐢) β†’ ((0gβ€˜(Scalarβ€˜π‘‡)) Β· 𝑀) = (0gβ€˜π‘‡))
6966, 68sylancom 589 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ 𝑀 ∈ 𝐢) β†’ ((0gβ€˜(Scalarβ€˜π‘‡)) Β· 𝑀) = (0gβ€˜π‘‡))
70 fvexd 6862 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (0gβ€˜(Scalarβ€˜π‘‡)) ∈ V)
7165, 69, 48, 50, 36, 70suppssof1 8135 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ ((𝑧 ∘f Β· 𝐴) supp (0gβ€˜π‘‡)) βŠ† (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))))
72 suppssfifsupp 9327 . . . . . . 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 1379 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡))
7419, 32, 35, 36, 52, 73gsumcl 19699 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ 𝐢)
7531, 74chvarvv 2003 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) ∈ 𝐢)
76 frlmup.e . . . 4 𝐸 = (π‘₯ ∈ 𝐡 ↦ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)))
7775, 76fmptd 7067 . . 3 (πœ‘ β†’ 𝐸:𝐡⟢𝐢)
7834adantr 482 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑇 ∈ CMnd)
7912adantr 482 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐼 ∈ 𝑋)
80 eleq1w 2821 . . . . . . . . 9 (𝑧 = 𝑦 β†’ (𝑧 ∈ 𝐡 ↔ 𝑦 ∈ 𝐡))
8180anbi2d 630 . . . . . . . 8 (𝑧 = 𝑦 β†’ ((πœ‘ ∧ 𝑧 ∈ 𝐡) ↔ (πœ‘ ∧ 𝑦 ∈ 𝐡)))
82 oveq1 7369 . . . . . . . . 9 (𝑧 = 𝑦 β†’ (𝑧 ∘f Β· 𝐴) = (𝑦 ∘f Β· 𝐴))
8382feq1d 6658 . . . . . . . 8 (𝑧 = 𝑦 β†’ ((𝑧 ∘f Β· 𝐴):𝐼⟢𝐢 ↔ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢))
8481, 83imbi12d 345 . . . . . . 7 (𝑧 = 𝑦 β†’ (((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢) ↔ ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)))
8584, 52chvarvv 2003 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)
8685adantrr 716 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)
8752adantrl 715 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢)
8882breq1d 5120 . . . . . . . 8 (𝑧 = 𝑦 β†’ ((𝑧 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡) ↔ (𝑦 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡)))
8981, 88imbi12d 345 . . . . . . 7 (𝑧 = 𝑦 β†’ (((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡)) ↔ ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡))))
9089, 73chvarvv 2003 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡))
9190adantrr 716 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡))
9273adantrl 715 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡))
9319, 32, 21, 78, 79, 86, 87, 91, 92gsumadd 19707 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))) = ((𝑇 Ξ£g (𝑦 ∘f Β· 𝐴))(+gβ€˜π‘‡)(𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
941, 20lmodvacl 20352 . . . . . . . 8 ((𝐹 ∈ LMod ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
95943expb 1121 . . . . . . 7 ((𝐹 ∈ LMod ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
9615, 95sylan 581 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
97 oveq1 7369 . . . . . . . 8 (π‘₯ = (𝑦(+gβ€˜πΉ)𝑧) β†’ (π‘₯ ∘f Β· 𝐴) = ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴))
9897oveq2d 7378 . . . . . . 7 (π‘₯ = (𝑦(+gβ€˜πΉ)𝑧) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)))
99 ovex 7395 . . . . . . 7 (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)) ∈ V
10098, 76, 99fvmpt 6953 . . . . . 6 ((𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡 β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)))
10196, 100syl 17 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)))
10211adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑅 ∈ Ring)
103 simprl 770 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦 ∈ 𝐡)
104 simprr 772 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧 ∈ 𝐡)
105 eqid 2737 . . . . . . . . 9 (+gβ€˜π‘…) = (+gβ€˜π‘…)
10613, 1, 102, 79, 103, 104, 105, 20frlmplusgval 21186 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) = (𝑦 ∘f (+gβ€˜π‘…)𝑧))
107106oveq1d 7377 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴))
10813, 46, 1frlmbasf 21182 . . . . . . . . . . . . 13 ((𝐼 ∈ 𝑋 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
10912, 108sylan 581 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
110109adantrr 716 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
111110ffnd 6674 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦 Fn 𝐼)
11248adantrl 715 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
113112ffnd 6674 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧 Fn 𝐼)
114111, 113, 79, 79, 51offn 7635 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f (+gβ€˜π‘…)𝑧) Fn 𝐼)
11549ffnd 6674 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 Fn 𝐼)
116115adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴 Fn 𝐼)
117114, 116, 79, 79, 51offn 7635 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴) Fn 𝐼)
11885ffnd 6674 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴) Fn 𝐼)
119118adantrr 716 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f Β· 𝐴) Fn 𝐼)
12052ffnd 6674 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) Fn 𝐼)
121120adantrl 715 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴) Fn 𝐼)
122119, 121, 79, 79, 51offn 7635 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)) Fn 𝐼)
1237fveq2d 6851 . . . . . . . . . . . . . 14 (πœ‘ β†’ (+gβ€˜π‘…) = (+gβ€˜(Scalarβ€˜π‘‡)))
124123ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (+gβ€˜π‘…) = (+gβ€˜(Scalarβ€˜π‘‡)))
125124oveqd 7379 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) = ((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)))
126125oveq1d 7377 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
1278ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑇 ∈ LMod)
128110ffvelcdmda 7040 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘¦β€˜π‘₯) ∈ (Baseβ€˜π‘…))
12939ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
130128, 129eleqtrd 2840 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘¦β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
131112ffvelcdmda 7040 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜π‘…))
132131, 129eleqtrd 2840 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
13349adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴:𝐼⟢𝐢)
134133ffvelcdmda 7040 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
135 eqid 2737 . . . . . . . . . . . . 13 (+gβ€˜(Scalarβ€˜π‘‡)) = (+gβ€˜(Scalarβ€˜π‘‡))
13619, 21, 5, 3, 43, 135lmodvsdir 20362 . . . . . . . . . . . 12 ((𝑇 ∈ LMod ∧ ((π‘¦β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π΄β€˜π‘₯) ∈ 𝐢)) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
137127, 130, 132, 134, 136syl13anc 1373 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
138126, 137eqtrd 2777 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
139111adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 Fn 𝐼)
140113adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑧 Fn 𝐼)
14112ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐼 ∈ 𝑋)
142 simpr 486 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ π‘₯ ∈ 𝐼)
143 fnfvof 7639 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼 ∧ 𝑧 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) = ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)))
144139, 140, 141, 142, 143syl22anc 838 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) = ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)))
145144oveq1d 7377 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
146115ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐴 Fn 𝐼)
147 fnfvof 7639 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑦 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯)))
148139, 146, 141, 142, 147syl22anc 838 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯)))
149 fnfvof 7639 . . . . . . . . . . . 12 (((𝑧 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯)))
150140, 146, 141, 142, 149syl22anc 838 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯)))
151148, 150oveq12d 7380 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f Β· 𝐴)β€˜π‘₯)(+gβ€˜π‘‡)((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
152138, 145, 1513eqtr4d 2787 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = (((𝑦 ∘f Β· 𝐴)β€˜π‘₯)(+gβ€˜π‘‡)((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
153114adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦 ∘f (+gβ€˜π‘…)𝑧) Fn 𝐼)
154 fnfvof 7639 . . . . . . . . . 10 ((((𝑦 ∘f (+gβ€˜π‘…)𝑧) Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
155153, 146, 141, 142, 154syl22anc 838 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
156119adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦 ∘f Β· 𝐴) Fn 𝐼)
157121adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑧 ∘f Β· 𝐴) Fn 𝐼)
158 fnfvof 7639 . . . . . . . . . 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 2787 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))β€˜π‘₯))
161117, 122, 160eqfnfvd 6990 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)))
162107, 161eqtrd 2777 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)))
163162oveq2d 7378 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))))
164101, 163eqtrd 2777 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))))
165 oveq1 7369 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (π‘₯ ∘f Β· 𝐴) = (𝑦 ∘f Β· 𝐴))
166165oveq2d 7378 . . . . . . 7 (π‘₯ = 𝑦 β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
167 ovex 7395 . . . . . . 7 (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)) ∈ V
168166, 76, 167fvmpt 6953 . . . . . 6 (𝑦 ∈ 𝐡 β†’ (πΈβ€˜π‘¦) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
169168ad2antrl 727 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜π‘¦) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
170 oveq1 7369 . . . . . . . 8 (π‘₯ = 𝑧 β†’ (π‘₯ ∘f Β· 𝐴) = (𝑧 ∘f Β· 𝐴))
171170oveq2d 7378 . . . . . . 7 (π‘₯ = 𝑧 β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
172 ovex 7395 . . . . . . 7 (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ V
173171, 76, 172fvmpt 6953 . . . . . 6 (𝑧 ∈ 𝐡 β†’ (πΈβ€˜π‘§) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
174173ad2antll 728 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜π‘§) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
175169, 174oveq12d 7380 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((πΈβ€˜π‘¦)(+gβ€˜π‘‡)(πΈβ€˜π‘§)) = ((𝑇 Ξ£g (𝑦 ∘f Β· 𝐴))(+gβ€˜π‘‡)(𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
17693, 164, 1753eqtr4d 2787 . . 3 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = ((πΈβ€˜π‘¦)(+gβ€˜π‘‡)(πΈβ€˜π‘§)))
1771, 19, 20, 21, 23, 25, 77, 176isghmd 19024 . 2 (πœ‘ β†’ 𝐸 ∈ (𝐹 GrpHom 𝑇))
1788adantr 482 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑇 ∈ LMod)
17912adantr 482 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝐼 ∈ 𝑋)
18018fveq2d 6851 . . . . . . . 8 (πœ‘ β†’ (Baseβ€˜(Scalarβ€˜π‘‡)) = (Baseβ€˜(Scalarβ€˜πΉ)))
181180eleq2d 2824 . . . . . . 7 (πœ‘ β†’ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ↔ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ))))
182181biimpar 479 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ))) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
183182adantrr 716 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
18452adantrl 715 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢)
185184ffvelcdmda 7040 . . . . 5 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) ∈ 𝐢)
18652feqmptd 6915 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
187186, 73eqbrtrrd 5134 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) finSupp (0gβ€˜π‘‡))
188187adantrl 715 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) finSupp (0gβ€˜π‘‡))
18919, 5, 43, 32, 21, 3, 178, 179, 183, 185, 188gsumvsmul 20402 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))) = (𝑦 Β· (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))))
19015adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝐹 ∈ LMod)
191 simprl 770 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)))
192 simprr 772 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧 ∈ 𝐡)
1931, 4, 2, 6lmodvscl 20355 . . . . . . . . . . . 12 ((𝐹 ∈ LMod ∧ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡)
194190, 191, 192, 193syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡)
19513, 46, 1frlmbasf 21182 . . . . . . . . . . 11 ((𝐼 ∈ 𝑋 ∧ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧):𝐼⟢(Baseβ€˜π‘…))
196179, 194, 195syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧):𝐼⟢(Baseβ€˜π‘…))
197196ffnd 6674 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) Fn 𝐼)
198115adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴 Fn 𝐼)
199197, 198, 179, 179, 51offn 7635 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) Fn 𝐼)
200 dffn2 6675 . . . . . . . 8 (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) Fn 𝐼 ↔ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴):𝐼⟢V)
201199, 200sylib 217 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴):𝐼⟢V)
202201feqmptd 6915 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯)))
2037fveq2d 6851 . . . . . . . . . . . 12 (πœ‘ β†’ (.rβ€˜π‘…) = (.rβ€˜(Scalarβ€˜π‘‡)))
204203ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (.rβ€˜π‘…) = (.rβ€˜(Scalarβ€˜π‘‡)))
205204oveqd 7379 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) = (𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)))
206205oveq1d 7377 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = ((𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
2078ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑇 ∈ LMod)
208 simplrl 776 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)))
209180ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜(Scalarβ€˜π‘‡)) = (Baseβ€˜(Scalarβ€˜πΉ)))
210208, 209eleqtrrd 2841 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
21148ffvelcdmda 7040 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜π‘…))
21239ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
213211, 212eleqtrd 2840 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
214213adantlrl 719 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
21549ffvelcdmda 7040 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
216215adantlr 714 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
217 eqid 2737 . . . . . . . . . . 11 (.rβ€˜(Scalarβ€˜π‘‡)) = (.rβ€˜(Scalarβ€˜π‘‡))
21819, 5, 3, 43, 217lmodvsass 20363 . . . . . . . . . 10 ((𝑇 ∈ LMod ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π΄β€˜π‘₯) ∈ 𝐢)) β†’ ((𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
219207, 210, 214, 216, 218syl13anc 1373 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
220206, 219eqtrd 2777 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
221197adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) Fn 𝐼)
222115ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐴 Fn 𝐼)
22312ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐼 ∈ 𝑋)
224 simpr 486 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ π‘₯ ∈ 𝐼)
225 fnfvof 7639 . . . . . . . . . 10 ((((𝑦( ·𝑠 β€˜πΉ)𝑧) Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
226221, 222, 223, 224, 225syl22anc 838 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
22717fveq2d 6851 . . . . . . . . . . . . 13 (πœ‘ β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜πΉ)))
228227ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜πΉ)))
229208, 228eleqtrrd 2841 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 ∈ (Baseβ€˜π‘…))
230 simplrr 777 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑧 ∈ 𝐡)
231 eqid 2737 . . . . . . . . . . 11 (.rβ€˜π‘…) = (.rβ€˜π‘…)
23213, 1, 46, 223, 229, 230, 224, 2, 231frlmvscaval 21190 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) = (𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)))
233232oveq1d 7377 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
234226, 233eqtrd 2777 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
23548ffnd 6674 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 Fn 𝐼)
236235adantrl 715 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧 Fn 𝐼)
237236adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑧 Fn 𝐼)
238237, 222, 223, 224, 149syl22anc 838 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯)))
239238oveq2d 7378 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
240220, 234, 2393eqtr4d 2787 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
241240mpteq2dva 5210 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (π‘₯ ∈ 𝐼 ↦ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯)) = (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
242202, 241eqtrd 2777 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
243242oveq2d 7378 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))))
244184feqmptd 6915 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
245244oveq2d 7378 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
246245oveq2d 7378 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))) = (𝑦 Β· (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))))
247189, 243, 2463eqtr4d 2787 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
248 oveq1 7369 . . . . . 6 (π‘₯ = (𝑦( ·𝑠 β€˜πΉ)𝑧) β†’ (π‘₯ ∘f Β· 𝐴) = ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴))
249248oveq2d 7378 . . . . 5 (π‘₯ = (𝑦( ·𝑠 β€˜πΉ)𝑧) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
250 ovex 7395 . . . . 5 (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) ∈ V
251249, 76, 250fvmpt 6953 . . . 4 ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡 β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
252194, 251syl 17 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
253173oveq2d 7378 . . . 4 (𝑧 ∈ 𝐡 β†’ (𝑦 Β· (πΈβ€˜π‘§)) = (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
254253ad2antll 728 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 Β· (πΈβ€˜π‘§)) = (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
255247, 252, 2543eqtr4d 2787 . 2 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑦 Β· (πΈβ€˜π‘§)))
2561, 2, 3, 4, 5, 6, 15, 8, 18, 177, 255islmhmd 20516 1 (πœ‘ β†’ 𝐸 ∈ (𝐹 LMHom 𝑇))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3448   βŠ† wss 3915   class class class wbr 5110   ↦ cmpt 5193  Fun wfun 6495   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ∘f cof 7620   supp csupp 8097  Fincfn 8890   finSupp cfsupp 9312  Basecbs 17090  +gcplusg 17140  .rcmulr 17141  Scalarcsca 17143   ·𝑠 cvsca 17144  0gc0g 17328   Ξ£g cgsu 17329  Grpcgrp 18755  CMndccmn 19569  Ringcrg 19971  LModclmod 20338   LMHom clmhm 20496   freeLMod cfrlm 21168
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-sup 9385  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-fz 13432  df-fzo 13575  df-seq 13914  df-hash 14238  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-hom 17164  df-cco 17165  df-0g 17330  df-gsum 17331  df-prds 17336  df-pws 17338  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-mhm 18608  df-submnd 18609  df-grp 18758  df-minusg 18759  df-sbg 18760  df-subg 18932  df-ghm 19013  df-cntz 19104  df-cmn 19571  df-abl 19572  df-mgp 19904  df-ur 19921  df-ring 19973  df-subrg 20236  df-lmod 20340  df-lss 20409  df-lmhm 20499  df-sra 20649  df-rgmod 20650  df-dsmm 21154  df-frlm 21169
This theorem is referenced by:  frlmup3  21222  frlmup4  21223  islindf5  21261  indlcim  21262  lnrfg  41475
  Copyright terms: Public domain W3C validator