MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frlmup1 Structured version   Visualization version   GIF version
Theorem frlmup1 21344
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 2732 . 2 ( ·𝑠 β€˜πΉ) = ( ·𝑠 β€˜πΉ)
3 frlmup.v . 2 Β· = ( ·𝑠 β€˜π‘‡)
4 eqid 2732 . 2 (Scalarβ€˜πΉ) = (Scalarβ€˜πΉ)
5 eqid 2732 . 2 (Scalarβ€˜π‘‡) = (Scalarβ€˜π‘‡)
6 eqid 2732 . 2 (Baseβ€˜(Scalarβ€˜πΉ)) = (Baseβ€˜(Scalarβ€˜πΉ))
7 frlmup.r . . . 4 (πœ‘ β†’ 𝑅 = (Scalarβ€˜π‘‡))
8 frlmup.t . . . . 5 (πœ‘ β†’ 𝑇 ∈ LMod)
95lmodring 20471 . . . . 5 (𝑇 ∈ LMod β†’ (Scalarβ€˜π‘‡) ∈ Ring)
108, 9syl 17 . . . 4 (πœ‘ β†’ (Scalarβ€˜π‘‡) ∈ Ring)
117, 10eqeltrd 2833 . . 3 (πœ‘ β†’ 𝑅 ∈ Ring)
12 frlmup.i . . 3 (πœ‘ β†’ 𝐼 ∈ 𝑋)
13 frlmup.f . . . 4 𝐹 = (𝑅 freeLMod 𝐼)
1413frlmlmod 21295 . . 3 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) β†’ 𝐹 ∈ LMod)
1511, 12, 14syl2anc 584 . 2 (πœ‘ β†’ 𝐹 ∈ LMod)
1613frlmsca 21299 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) β†’ 𝑅 = (Scalarβ€˜πΉ))
1711, 12, 16syl2anc 584 . . 3 (πœ‘ β†’ 𝑅 = (Scalarβ€˜πΉ))
187, 17eqtr3d 2774 . 2 (πœ‘ β†’ (Scalarβ€˜π‘‡) = (Scalarβ€˜πΉ))
19 frlmup.c . . 3 𝐢 = (Baseβ€˜π‘‡)
20 eqid 2732 . . 3 (+gβ€˜πΉ) = (+gβ€˜πΉ)
21 eqid 2732 . . 3 (+gβ€˜π‘‡) = (+gβ€˜π‘‡)
22 lmodgrp 20470 . . . 4 (𝐹 ∈ LMod β†’ 𝐹 ∈ Grp)
2315, 22syl 17 . . 3 (πœ‘ β†’ 𝐹 ∈ Grp)
24 lmodgrp 20470 . . . 4 (𝑇 ∈ LMod β†’ 𝑇 ∈ Grp)
258, 24syl 17 . . 3 (πœ‘ β†’ 𝑇 ∈ Grp)
26 eleq1w 2816 . . . . . . 7 (𝑧 = π‘₯ β†’ (𝑧 ∈ 𝐡 ↔ π‘₯ ∈ 𝐡))
2726anbi2d 629 . . . . . 6 (𝑧 = π‘₯ β†’ ((πœ‘ ∧ 𝑧 ∈ 𝐡) ↔ (πœ‘ ∧ π‘₯ ∈ 𝐡)))
28 oveq1 7412 . . . . . . . 8 (𝑧 = π‘₯ β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∘f Β· 𝐴))
2928oveq2d 7421 . . . . . . 7 (𝑧 = π‘₯ β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)))
3029eleq1d 2818 . . . . . 6 (𝑧 = π‘₯ β†’ ((𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ 𝐢 ↔ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) ∈ 𝐢))
3127, 30imbi12d 344 . . . . 5 (𝑧 = π‘₯ β†’ (((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ 𝐢) ↔ ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) ∈ 𝐢)))
32 eqid 2732 . . . . . 6 (0gβ€˜π‘‡) = (0gβ€˜π‘‡)
33 lmodcmn 20512 . . . . . . . 8 (𝑇 ∈ LMod β†’ 𝑇 ∈ CMnd)
348, 33syl 17 . . . . . . 7 (πœ‘ β†’ 𝑇 ∈ CMnd)
3534adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑇 ∈ CMnd)
3612adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝐼 ∈ 𝑋)
378ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ 𝑇 ∈ LMod)
38 simprl 769 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ π‘₯ ∈ (Baseβ€˜π‘…))
397fveq2d 6892 . . . . . . . . . 10 (πœ‘ β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
4039ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
4138, 40eleqtrd 2835 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
42 simprr 771 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ 𝑦 ∈ 𝐢)
43 eqid 2732 . . . . . . . . 9 (Baseβ€˜(Scalarβ€˜π‘‡)) = (Baseβ€˜(Scalarβ€˜π‘‡))
4419, 5, 3, 43lmodvscl 20481 . . . . . . . 8 ((𝑇 ∈ LMod ∧ π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ Β· 𝑦) ∈ 𝐢)
4537, 41, 42, 44syl3anc 1371 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯ Β· 𝑦) ∈ 𝐢)
46 eqid 2732 . . . . . . . . 9 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
4713, 46, 1frlmbasf 21306 . . . . . . . 8 ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐡) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
4812, 47sylan 580 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
49 frlmup.a . . . . . . . 8 (πœ‘ β†’ 𝐴:𝐼⟢𝐢)
5049adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝐴:𝐼⟢𝐢)
51 inidm 4217 . . . . . . 7 (𝐼 ∩ 𝐼) = 𝐼
5245, 48, 50, 36, 36, 51off 7684 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢)
53 ovexd 7440 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) ∈ V)
5452ffund 6718 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ Fun (𝑧 ∘f Β· 𝐴))
55 fvexd 6903 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (0gβ€˜π‘‡) ∈ V)
56 eqid 2732 . . . . . . . . . . 11 (0gβ€˜π‘…) = (0gβ€˜π‘…)
5713, 56, 1frlmbasfsupp 21304 . . . . . . . . . 10 ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜π‘…))
5812, 57sylan 580 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜π‘…))
597fveq2d 6892 . . . . . . . . . . . 12 (πœ‘ β†’ (0gβ€˜π‘…) = (0gβ€˜(Scalarβ€˜π‘‡)))
6059eqcomd 2738 . . . . . . . . . . 11 (πœ‘ β†’ (0gβ€˜(Scalarβ€˜π‘‡)) = (0gβ€˜π‘…))
6160breq2d 5159 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)) ↔ 𝑧 finSupp (0gβ€˜π‘…)))
6261adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)) ↔ 𝑧 finSupp (0gβ€˜π‘…)))
6358, 62mpbird 256 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)))
6463fsuppimpd 9365 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))) ∈ Fin)
65 ssidd 4004 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))) βŠ† (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))))
668ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ 𝑀 ∈ 𝐢) β†’ 𝑇 ∈ LMod)
67 eqid 2732 . . . . . . . . . 10 (0gβ€˜(Scalarβ€˜π‘‡)) = (0gβ€˜(Scalarβ€˜π‘‡))
6819, 5, 3, 67, 32lmod0vs 20497 . . . . . . . . 9 ((𝑇 ∈ LMod ∧ 𝑀 ∈ 𝐢) β†’ ((0gβ€˜(Scalarβ€˜π‘‡)) Β· 𝑀) = (0gβ€˜π‘‡))
6966, 68sylancom 588 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ 𝑀 ∈ 𝐢) β†’ ((0gβ€˜(Scalarβ€˜π‘‡)) Β· 𝑀) = (0gβ€˜π‘‡))
70 fvexd 6903 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (0gβ€˜(Scalarβ€˜π‘‡)) ∈ V)
7165, 69, 48, 50, 36, 70suppssof1 8180 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ ((𝑧 ∘f Β· 𝐴) supp (0gβ€˜π‘‡)) βŠ† (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))))
72 suppssfifsupp 9374 . . . . . . 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 1378 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡))
7419, 32, 35, 36, 52, 73gsumcl 19777 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ 𝐢)
7531, 74chvarvv 2002 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) ∈ 𝐢)
76 frlmup.e . . . 4 𝐸 = (π‘₯ ∈ 𝐡 ↦ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)))
7775, 76fmptd 7110 . . 3 (πœ‘ β†’ 𝐸:𝐡⟢𝐢)
7834adantr 481 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑇 ∈ CMnd)
7912adantr 481 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐼 ∈ 𝑋)
80 eleq1w 2816 . . . . . . . . 9 (𝑧 = 𝑦 β†’ (𝑧 ∈ 𝐡 ↔ 𝑦 ∈ 𝐡))
8180anbi2d 629 . . . . . . . 8 (𝑧 = 𝑦 β†’ ((πœ‘ ∧ 𝑧 ∈ 𝐡) ↔ (πœ‘ ∧ 𝑦 ∈ 𝐡)))
82 oveq1 7412 . . . . . . . . 9 (𝑧 = 𝑦 β†’ (𝑧 ∘f Β· 𝐴) = (𝑦 ∘f Β· 𝐴))
8382feq1d 6699 . . . . . . . 8 (𝑧 = 𝑦 β†’ ((𝑧 ∘f Β· 𝐴):𝐼⟢𝐢 ↔ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢))
8481, 83imbi12d 344 . . . . . . 7 (𝑧 = 𝑦 β†’ (((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢) ↔ ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)))
8584, 52chvarvv 2002 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)
8685adantrr 715 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)
8752adantrl 714 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢)
8882breq1d 5157 . . . . . . . 8 (𝑧 = 𝑦 β†’ ((𝑧 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡) ↔ (𝑦 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡)))
8981, 88imbi12d 344 . . . . . . 7 (𝑧 = 𝑦 β†’ (((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡)) ↔ ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡))))
9089, 73chvarvv 2002 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡))
9190adantrr 715 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡))
9273adantrl 714 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴) finSupp (0gβ€˜π‘‡))
9319, 32, 21, 78, 79, 86, 87, 91, 92gsumadd 19785 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))) = ((𝑇 Ξ£g (𝑦 ∘f Β· 𝐴))(+gβ€˜π‘‡)(𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
941, 20lmodvacl 20478 . . . . . . . 8 ((𝐹 ∈ LMod ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
95943expb 1120 . . . . . . 7 ((𝐹 ∈ LMod ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
9615, 95sylan 580 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
97 oveq1 7412 . . . . . . . 8 (π‘₯ = (𝑦(+gβ€˜πΉ)𝑧) β†’ (π‘₯ ∘f Β· 𝐴) = ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴))
9897oveq2d 7421 . . . . . . 7 (π‘₯ = (𝑦(+gβ€˜πΉ)𝑧) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)))
99 ovex 7438 . . . . . . 7 (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)) ∈ V
10098, 76, 99fvmpt 6995 . . . . . 6 ((𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡 β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)))
10196, 100syl 17 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)))
10211adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑅 ∈ Ring)
103 simprl 769 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦 ∈ 𝐡)
104 simprr 771 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧 ∈ 𝐡)
105 eqid 2732 . . . . . . . . 9 (+gβ€˜π‘…) = (+gβ€˜π‘…)
10613, 1, 102, 79, 103, 104, 105, 20frlmplusgval 21310 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) = (𝑦 ∘f (+gβ€˜π‘…)𝑧))
107106oveq1d 7420 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴))
10813, 46, 1frlmbasf 21306 . . . . . . . . . . . . 13 ((𝐼 ∈ 𝑋 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
10912, 108sylan 580 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
110109adantrr 715 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
111110ffnd 6715 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦 Fn 𝐼)
11248adantrl 714 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
113112ffnd 6715 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧 Fn 𝐼)
114111, 113, 79, 79, 51offn 7679 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f (+gβ€˜π‘…)𝑧) Fn 𝐼)
11549ffnd 6715 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 Fn 𝐼)
116115adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴 Fn 𝐼)
117114, 116, 79, 79, 51offn 7679 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴) Fn 𝐼)
11885ffnd 6715 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴) Fn 𝐼)
119118adantrr 715 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f Β· 𝐴) Fn 𝐼)
12052ffnd 6715 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) Fn 𝐼)
121120adantrl 714 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴) Fn 𝐼)
122119, 121, 79, 79, 51offn 7679 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)) Fn 𝐼)
1237fveq2d 6892 . . . . . . . . . . . . . 14 (πœ‘ β†’ (+gβ€˜π‘…) = (+gβ€˜(Scalarβ€˜π‘‡)))
124123ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (+gβ€˜π‘…) = (+gβ€˜(Scalarβ€˜π‘‡)))
125124oveqd 7422 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) = ((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)))
126125oveq1d 7420 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
1278ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑇 ∈ LMod)
128110ffvelcdmda 7083 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘¦β€˜π‘₯) ∈ (Baseβ€˜π‘…))
12939ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
130128, 129eleqtrd 2835 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘¦β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
131112ffvelcdmda 7083 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜π‘…))
132131, 129eleqtrd 2835 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
13349adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴:𝐼⟢𝐢)
134133ffvelcdmda 7083 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
135 eqid 2732 . . . . . . . . . . . . 13 (+gβ€˜(Scalarβ€˜π‘‡)) = (+gβ€˜(Scalarβ€˜π‘‡))
13619, 21, 5, 3, 43, 135lmodvsdir 20488 . . . . . . . . . . . 12 ((𝑇 ∈ LMod ∧ ((π‘¦β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π΄β€˜π‘₯) ∈ 𝐢)) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
137127, 130, 132, 134, 136syl13anc 1372 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
138126, 137eqtrd 2772 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
139111adantr 481 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 Fn 𝐼)
140113adantr 481 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑧 Fn 𝐼)
14112ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐼 ∈ 𝑋)
142 simpr 485 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ π‘₯ ∈ 𝐼)
143 fnfvof 7683 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼 ∧ 𝑧 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) = ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)))
144139, 140, 141, 142, 143syl22anc 837 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) = ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)))
145144oveq1d 7420 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
146115ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐴 Fn 𝐼)
147 fnfvof 7683 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑦 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯)))
148139, 146, 141, 142, 147syl22anc 837 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯)))
149 fnfvof 7683 . . . . . . . . . . . 12 (((𝑧 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯)))
150140, 146, 141, 142, 149syl22anc 837 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯)))
151148, 150oveq12d 7423 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f Β· 𝐴)β€˜π‘₯)(+gβ€˜π‘‡)((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
152138, 145, 1513eqtr4d 2782 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = (((𝑦 ∘f Β· 𝐴)β€˜π‘₯)(+gβ€˜π‘‡)((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
153114adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦 ∘f (+gβ€˜π‘…)𝑧) Fn 𝐼)
154 fnfvof 7683 . . . . . . . . . 10 ((((𝑦 ∘f (+gβ€˜π‘…)𝑧) Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
155153, 146, 141, 142, 154syl22anc 837 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
156119adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦 ∘f Β· 𝐴) Fn 𝐼)
157121adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑧 ∘f Β· 𝐴) Fn 𝐼)
158 fnfvof 7683 . . . . . . . . . 10 ((((𝑦 ∘f Β· 𝐴) Fn 𝐼 ∧ (𝑧 ∘f Β· 𝐴) Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ (((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))β€˜π‘₯) = (((𝑦 ∘f Β· 𝐴)β€˜π‘₯)(+gβ€˜π‘‡)((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
159156, 157, 141, 142, 158syl22anc 837 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))β€˜π‘₯) = (((𝑦 ∘f Β· 𝐴)β€˜π‘₯)(+gβ€˜π‘‡)((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
160152, 155, 1593eqtr4d 2782 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))β€˜π‘₯))
161117, 122, 160eqfnfvd 7032 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)))
162107, 161eqtrd 2772 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)))
163162oveq2d 7421 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))))
164101, 163eqtrd 2772 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))))
165 oveq1 7412 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (π‘₯ ∘f Β· 𝐴) = (𝑦 ∘f Β· 𝐴))
166165oveq2d 7421 . . . . . . 7 (π‘₯ = 𝑦 β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
167 ovex 7438 . . . . . . 7 (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)) ∈ V
168166, 76, 167fvmpt 6995 . . . . . 6 (𝑦 ∈ 𝐡 β†’ (πΈβ€˜π‘¦) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
169168ad2antrl 726 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜π‘¦) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
170 oveq1 7412 . . . . . . . 8 (π‘₯ = 𝑧 β†’ (π‘₯ ∘f Β· 𝐴) = (𝑧 ∘f Β· 𝐴))
171170oveq2d 7421 . . . . . . 7 (π‘₯ = 𝑧 β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
172 ovex 7438 . . . . . . 7 (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ V
173171, 76, 172fvmpt 6995 . . . . . 6 (𝑧 ∈ 𝐡 β†’ (πΈβ€˜π‘§) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
174173ad2antll 727 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜π‘§) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
175169, 174oveq12d 7423 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((πΈβ€˜π‘¦)(+gβ€˜π‘‡)(πΈβ€˜π‘§)) = ((𝑇 Ξ£g (𝑦 ∘f Β· 𝐴))(+gβ€˜π‘‡)(𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
17693, 164, 1753eqtr4d 2782 . . 3 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = ((πΈβ€˜π‘¦)(+gβ€˜π‘‡)(πΈβ€˜π‘§)))
1771, 19, 20, 21, 23, 25, 77, 176isghmd 19095 . 2 (πœ‘ β†’ 𝐸 ∈ (𝐹 GrpHom 𝑇))
1788adantr 481 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑇 ∈ LMod)
17912adantr 481 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝐼 ∈ 𝑋)
18018fveq2d 6892 . . . . . . . 8 (πœ‘ β†’ (Baseβ€˜(Scalarβ€˜π‘‡)) = (Baseβ€˜(Scalarβ€˜πΉ)))
181180eleq2d 2819 . . . . . . 7 (πœ‘ β†’ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ↔ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ))))
182181biimpar 478 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ))) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
183182adantrr 715 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
18452adantrl 714 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢)
185184ffvelcdmda 7083 . . . . 5 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) ∈ 𝐢)
18652feqmptd 6957 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
187186, 73eqbrtrrd 5171 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) finSupp (0gβ€˜π‘‡))
188187adantrl 714 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) finSupp (0gβ€˜π‘‡))
18919, 5, 43, 32, 21, 3, 178, 179, 183, 185, 188gsumvsmul 20528 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))) = (𝑦 Β· (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))))
19015adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝐹 ∈ LMod)
191 simprl 769 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)))
192 simprr 771 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧 ∈ 𝐡)
1931, 4, 2, 6lmodvscl 20481 . . . . . . . . . . . 12 ((𝐹 ∈ LMod ∧ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡)
194190, 191, 192, 193syl3anc 1371 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡)
19513, 46, 1frlmbasf 21306 . . . . . . . . . . 11 ((𝐼 ∈ 𝑋 ∧ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧):𝐼⟢(Baseβ€˜π‘…))
196179, 194, 195syl2anc 584 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧):𝐼⟢(Baseβ€˜π‘…))
197196ffnd 6715 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) Fn 𝐼)
198115adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴 Fn 𝐼)
199197, 198, 179, 179, 51offn 7679 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) Fn 𝐼)
200 dffn2 6716 . . . . . . . 8 (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) Fn 𝐼 ↔ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴):𝐼⟢V)
201199, 200sylib 217 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴):𝐼⟢V)
202201feqmptd 6957 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯)))
2037fveq2d 6892 . . . . . . . . . . . 12 (πœ‘ β†’ (.rβ€˜π‘…) = (.rβ€˜(Scalarβ€˜π‘‡)))
204203ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (.rβ€˜π‘…) = (.rβ€˜(Scalarβ€˜π‘‡)))
205204oveqd 7422 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) = (𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)))
206205oveq1d 7420 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = ((𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
2078ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑇 ∈ LMod)
208 simplrl 775 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)))
209180ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜(Scalarβ€˜π‘‡)) = (Baseβ€˜(Scalarβ€˜πΉ)))
210208, 209eleqtrrd 2836 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
21148ffvelcdmda 7083 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜π‘…))
21239ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
213211, 212eleqtrd 2835 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
214213adantlrl 718 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
21549ffvelcdmda 7083 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
216215adantlr 713 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
217 eqid 2732 . . . . . . . . . . 11 (.rβ€˜(Scalarβ€˜π‘‡)) = (.rβ€˜(Scalarβ€˜π‘‡))
21819, 5, 3, 43, 217lmodvsass 20489 . . . . . . . . . 10 ((𝑇 ∈ LMod ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π΄β€˜π‘₯) ∈ 𝐢)) β†’ ((𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
219207, 210, 214, 216, 218syl13anc 1372 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
220206, 219eqtrd 2772 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
221197adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) Fn 𝐼)
222115ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐴 Fn 𝐼)
22312ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐼 ∈ 𝑋)
224 simpr 485 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ π‘₯ ∈ 𝐼)
225 fnfvof 7683 . . . . . . . . . 10 ((((𝑦( ·𝑠 β€˜πΉ)𝑧) Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
226221, 222, 223, 224, 225syl22anc 837 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
22717fveq2d 6892 . . . . . . . . . . . . 13 (πœ‘ β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜πΉ)))
228227ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜πΉ)))
229208, 228eleqtrrd 2836 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 ∈ (Baseβ€˜π‘…))
230 simplrr 776 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑧 ∈ 𝐡)
231 eqid 2732 . . . . . . . . . . 11 (.rβ€˜π‘…) = (.rβ€˜π‘…)
23213, 1, 46, 223, 229, 230, 224, 2, 231frlmvscaval 21314 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) = (𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)))
233232oveq1d 7420 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
234226, 233eqtrd 2772 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
23548ffnd 6715 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 Fn 𝐼)
236235adantrl 714 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧 Fn 𝐼)
237236adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑧 Fn 𝐼)
238237, 222, 223, 224, 149syl22anc 837 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯)))
239238oveq2d 7421 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
240220, 234, 2393eqtr4d 2782 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
241240mpteq2dva 5247 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (π‘₯ ∈ 𝐼 ↦ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯)) = (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
242202, 241eqtrd 2772 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
243242oveq2d 7421 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))))
244184feqmptd 6957 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
245244oveq2d 7421 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
246245oveq2d 7421 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))) = (𝑦 Β· (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))))
247189, 243, 2463eqtr4d 2782 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
248 oveq1 7412 . . . . . 6 (π‘₯ = (𝑦( ·𝑠 β€˜πΉ)𝑧) β†’ (π‘₯ ∘f Β· 𝐴) = ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴))
249248oveq2d 7421 . . . . 5 (π‘₯ = (𝑦( ·𝑠 β€˜πΉ)𝑧) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
250 ovex 7438 . . . . 5 (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) ∈ V
251249, 76, 250fvmpt 6995 . . . 4 ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡 β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
252194, 251syl 17 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
253173oveq2d 7421 . . . 4 (𝑧 ∈ 𝐡 β†’ (𝑦 Β· (πΈβ€˜π‘§)) = (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
254253ad2antll 727 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 Β· (πΈβ€˜π‘§)) = (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
255247, 252, 2543eqtr4d 2782 . 2 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑦 Β· (πΈβ€˜π‘§)))
2561, 2, 3, 4, 5, 6, 15, 8, 18, 177, 255islmhmd 20642 1 (πœ‘ β†’ 𝐸 ∈ (𝐹 LMHom 𝑇))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3474   βŠ† wss 3947   class class class wbr 5147   ↦ cmpt 5230  Fun wfun 6534   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ∘f cof 7664   supp csupp 8142  Fincfn 8935   finSupp cfsupp 9357  Basecbs 17140  +gcplusg 17193  .rcmulr 17194  Scalarcsca 17196   ·𝑠 cvsca 17197  0gc0g 17381   Ξ£g cgsu 17382  Grpcgrp 18815  CMndccmn 19642  Ringcrg 20049  LModclmod 20463   LMHom clmhm 20622   freeLMod cfrlm 21292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-sup 9433  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-fz 13481  df-fzo 13624  df-seq 13963  df-hash 14287  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-hom 17217  df-cco 17218  df-0g 17383  df-gsum 17384  df-prds 17389  df-pws 17391  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-mhm 18667  df-submnd 18668  df-grp 18818  df-minusg 18819  df-sbg 18820  df-subg 18997  df-ghm 19084  df-cntz 19175  df-cmn 19644  df-abl 19645  df-mgp 19982  df-ur 19999  df-ring 20051  df-subrg 20353  df-lmod 20465  df-lss 20535  df-lmhm 20625  df-sra 20777  df-rgmod 20778  df-dsmm 21278  df-frlm 21293
This theorem is referenced by:  frlmup3  21346  frlmup4  21347  islindf5  21385  indlcim  21386  lnrfg  41846
  Copyright terms: Public domain W3C validator