MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frlmup1 Structured version   Visualization version   GIF version
Theorem frlmup1 21353
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 2733 . 2 ( ·𝑠 β€˜πΉ) = ( ·𝑠 β€˜πΉ)
3 frlmup.v . 2 Β· = ( ·𝑠 β€˜π‘‡)
4 eqid 2733 . 2 (Scalarβ€˜πΉ) = (Scalarβ€˜πΉ)
5 eqid 2733 . 2 (Scalarβ€˜π‘‡) = (Scalarβ€˜π‘‡)
6 eqid 2733 . 2 (Baseβ€˜(Scalarβ€˜πΉ)) = (Baseβ€˜(Scalarβ€˜πΉ))
7 frlmup.r . . . 4 (πœ‘ β†’ 𝑅 = (Scalarβ€˜π‘‡))
8 frlmup.t . . . . 5 (πœ‘ β†’ 𝑇 ∈ LMod)
95lmodring 20479 . . . . 5 (𝑇 ∈ LMod β†’ (Scalarβ€˜π‘‡) ∈ Ring)
108, 9syl 17 . . . 4 (πœ‘ β†’ (Scalarβ€˜π‘‡) ∈ Ring)
117, 10eqeltrd 2834 . . 3 (πœ‘ β†’ 𝑅 ∈ Ring)
12 frlmup.i . . 3 (πœ‘ β†’ 𝐼 ∈ 𝑋)
13 frlmup.f . . . 4 𝐹 = (𝑅 freeLMod 𝐼)
1413frlmlmod 21304 . . 3 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) β†’ 𝐹 ∈ LMod)
1511, 12, 14syl2anc 585 . 2 (πœ‘ β†’ 𝐹 ∈ LMod)
1613frlmsca 21308 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) β†’ 𝑅 = (Scalarβ€˜πΉ))
1711, 12, 16syl2anc 585 . . 3 (πœ‘ β†’ 𝑅 = (Scalarβ€˜πΉ))
187, 17eqtr3d 2775 . 2 (πœ‘ β†’ (Scalarβ€˜π‘‡) = (Scalarβ€˜πΉ))
19 frlmup.c . . 3 𝐢 = (Baseβ€˜π‘‡)
20 eqid 2733 . . 3 (+gβ€˜πΉ) = (+gβ€˜πΉ)
21 eqid 2733 . . 3 (+gβ€˜π‘‡) = (+gβ€˜π‘‡)
22 lmodgrp 20478 . . . 4 (𝐹 ∈ LMod β†’ 𝐹 ∈ Grp)
2315, 22syl 17 . . 3 (πœ‘ β†’ 𝐹 ∈ Grp)
24 lmodgrp 20478 . . . 4 (𝑇 ∈ LMod β†’ 𝑇 ∈ Grp)
258, 24syl 17 . . 3 (πœ‘ β†’ 𝑇 ∈ Grp)
26 eleq1w 2817 . . . . . . 7 (𝑧 = π‘₯ β†’ (𝑧 ∈ 𝐡 ↔ π‘₯ ∈ 𝐡))
2726anbi2d 630 . . . . . 6 (𝑧 = π‘₯ β†’ ((πœ‘ ∧ 𝑧 ∈ 𝐡) ↔ (πœ‘ ∧ π‘₯ ∈ 𝐡)))
28 oveq1 7416 . . . . . . . 8 (𝑧 = π‘₯ β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∘f Β· 𝐴))
2928oveq2d 7425 . . . . . . 7 (𝑧 = π‘₯ β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)))
3029eleq1d 2819 . . . . . 6 (𝑧 = π‘₯ β†’ ((𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ 𝐢 ↔ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) ∈ 𝐢))
3127, 30imbi12d 345 . . . . 5 (𝑧 = π‘₯ β†’ (((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ 𝐢) ↔ ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) ∈ 𝐢)))
32 eqid 2733 . . . . . 6 (0gβ€˜π‘‡) = (0gβ€˜π‘‡)
33 lmodcmn 20520 . . . . . . . 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 6896 . . . . . . . . . 10 (πœ‘ β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
4039ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
4138, 40eleqtrd 2836 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
42 simprr 772 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ 𝑦 ∈ 𝐢)
43 eqid 2733 . . . . . . . . 9 (Baseβ€˜(Scalarβ€˜π‘‡)) = (Baseβ€˜(Scalarβ€˜π‘‡))
4419, 5, 3, 43lmodvscl 20489 . . . . . . . 8 ((𝑇 ∈ LMod ∧ π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ Β· 𝑦) ∈ 𝐢)
4537, 41, 42, 44syl3anc 1372 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯ Β· 𝑦) ∈ 𝐢)
46 eqid 2733 . . . . . . . . 9 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
4713, 46, 1frlmbasf 21315 . . . . . . . 8 ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐡) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
4812, 47sylan 581 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
49 frlmup.a . . . . . . . 8 (πœ‘ β†’ 𝐴:𝐼⟢𝐢)
5049adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝐴:𝐼⟢𝐢)
51 inidm 4219 . . . . . . 7 (𝐼 ∩ 𝐼) = 𝐼
5245, 48, 50, 36, 36, 51off 7688 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢)
53 ovexd 7444 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) ∈ V)
5452ffund 6722 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ Fun (𝑧 ∘f Β· 𝐴))
55 fvexd 6907 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (0gβ€˜π‘‡) ∈ V)
56 eqid 2733 . . . . . . . . . . 11 (0gβ€˜π‘…) = (0gβ€˜π‘…)
5713, 56, 1frlmbasfsupp 21313 . . . . . . . . . 10 ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜π‘…))
5812, 57sylan 581 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜π‘…))
597fveq2d 6896 . . . . . . . . . . . 12 (πœ‘ β†’ (0gβ€˜π‘…) = (0gβ€˜(Scalarβ€˜π‘‡)))
6059eqcomd 2739 . . . . . . . . . . 11 (πœ‘ β†’ (0gβ€˜(Scalarβ€˜π‘‡)) = (0gβ€˜π‘…))
6160breq2d 5161 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)) ↔ 𝑧 finSupp (0gβ€˜π‘…)))
6261adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)) ↔ 𝑧 finSupp (0gβ€˜π‘…)))
6358, 62mpbird 257 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)))
6463fsuppimpd 9369 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))) ∈ Fin)
65 ssidd 4006 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))) βŠ† (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))))
668ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ 𝑀 ∈ 𝐢) β†’ 𝑇 ∈ LMod)
67 eqid 2733 . . . . . . . . . 10 (0gβ€˜(Scalarβ€˜π‘‡)) = (0gβ€˜(Scalarβ€˜π‘‡))
6819, 5, 3, 67, 32lmod0vs 20505 . . . . . . . . 9 ((𝑇 ∈ LMod ∧ 𝑀 ∈ 𝐢) β†’ ((0gβ€˜(Scalarβ€˜π‘‡)) Β· 𝑀) = (0gβ€˜π‘‡))
6966, 68sylancom 589 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ 𝑀 ∈ 𝐢) β†’ ((0gβ€˜(Scalarβ€˜π‘‡)) Β· 𝑀) = (0gβ€˜π‘‡))
70 fvexd 6907 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (0gβ€˜(Scalarβ€˜π‘‡)) ∈ V)
7165, 69, 48, 50, 36, 70suppssof1 8184 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ ((𝑧 ∘f Β· 𝐴) supp (0gβ€˜π‘‡)) βŠ† (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))))
72 suppssfifsupp 9378 . . . . . . 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 19783 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ 𝐢)
7531, 74chvarvv 2003 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) ∈ 𝐢)
76 frlmup.e . . . 4 𝐸 = (π‘₯ ∈ 𝐡 ↦ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)))
7775, 76fmptd 7114 . . 3 (πœ‘ β†’ 𝐸:𝐡⟢𝐢)
7834adantr 482 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑇 ∈ CMnd)
7912adantr 482 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐼 ∈ 𝑋)
80 eleq1w 2817 . . . . . . . . 9 (𝑧 = 𝑦 β†’ (𝑧 ∈ 𝐡 ↔ 𝑦 ∈ 𝐡))
8180anbi2d 630 . . . . . . . 8 (𝑧 = 𝑦 β†’ ((πœ‘ ∧ 𝑧 ∈ 𝐡) ↔ (πœ‘ ∧ 𝑦 ∈ 𝐡)))
82 oveq1 7416 . . . . . . . . 9 (𝑧 = 𝑦 β†’ (𝑧 ∘f Β· 𝐴) = (𝑦 ∘f Β· 𝐴))
8382feq1d 6703 . . . . . . . 8 (𝑧 = 𝑦 β†’ ((𝑧 ∘f Β· 𝐴):𝐼⟢𝐢 ↔ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢))
8481, 83imbi12d 345 . . . . . . 7 (𝑧 = 𝑦 β†’ (((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢) ↔ ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)))
8584, 52chvarvv 2003 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)
8685adantrr 716 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)
8752adantrl 715 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢)
8882breq1d 5159 . . . . . . . 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 19791 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))) = ((𝑇 Ξ£g (𝑦 ∘f Β· 𝐴))(+gβ€˜π‘‡)(𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
941, 20lmodvacl 20486 . . . . . . . 8 ((𝐹 ∈ LMod ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
95943expb 1121 . . . . . . 7 ((𝐹 ∈ LMod ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
9615, 95sylan 581 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
97 oveq1 7416 . . . . . . . 8 (π‘₯ = (𝑦(+gβ€˜πΉ)𝑧) β†’ (π‘₯ ∘f Β· 𝐴) = ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴))
9897oveq2d 7425 . . . . . . 7 (π‘₯ = (𝑦(+gβ€˜πΉ)𝑧) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)))
99 ovex 7442 . . . . . . 7 (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)) ∈ V
10098, 76, 99fvmpt 6999 . . . . . 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 2733 . . . . . . . . 9 (+gβ€˜π‘…) = (+gβ€˜π‘…)
10613, 1, 102, 79, 103, 104, 105, 20frlmplusgval 21319 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) = (𝑦 ∘f (+gβ€˜π‘…)𝑧))
107106oveq1d 7424 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴))
10813, 46, 1frlmbasf 21315 . . . . . . . . . . . . 13 ((𝐼 ∈ 𝑋 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
10912, 108sylan 581 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
110109adantrr 716 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
111110ffnd 6719 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦 Fn 𝐼)
11248adantrl 715 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
113112ffnd 6719 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧 Fn 𝐼)
114111, 113, 79, 79, 51offn 7683 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f (+gβ€˜π‘…)𝑧) Fn 𝐼)
11549ffnd 6719 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 Fn 𝐼)
116115adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴 Fn 𝐼)
117114, 116, 79, 79, 51offn 7683 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴) Fn 𝐼)
11885ffnd 6719 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴) Fn 𝐼)
119118adantrr 716 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f Β· 𝐴) Fn 𝐼)
12052ffnd 6719 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) Fn 𝐼)
121120adantrl 715 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴) Fn 𝐼)
122119, 121, 79, 79, 51offn 7683 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)) Fn 𝐼)
1237fveq2d 6896 . . . . . . . . . . . . . 14 (πœ‘ β†’ (+gβ€˜π‘…) = (+gβ€˜(Scalarβ€˜π‘‡)))
124123ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (+gβ€˜π‘…) = (+gβ€˜(Scalarβ€˜π‘‡)))
125124oveqd 7426 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) = ((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)))
126125oveq1d 7424 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
1278ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑇 ∈ LMod)
128110ffvelcdmda 7087 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘¦β€˜π‘₯) ∈ (Baseβ€˜π‘…))
12939ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
130128, 129eleqtrd 2836 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘¦β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
131112ffvelcdmda 7087 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜π‘…))
132131, 129eleqtrd 2836 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
13349adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴:𝐼⟢𝐢)
134133ffvelcdmda 7087 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
135 eqid 2733 . . . . . . . . . . . . 13 (+gβ€˜(Scalarβ€˜π‘‡)) = (+gβ€˜(Scalarβ€˜π‘‡))
13619, 21, 5, 3, 43, 135lmodvsdir 20496 . . . . . . . . . . . 12 ((𝑇 ∈ LMod ∧ ((π‘¦β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π΄β€˜π‘₯) ∈ 𝐢)) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
137127, 130, 132, 134, 136syl13anc 1373 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
138126, 137eqtrd 2773 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
139111adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 Fn 𝐼)
140113adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑧 Fn 𝐼)
14112ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐼 ∈ 𝑋)
142 simpr 486 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ π‘₯ ∈ 𝐼)
143 fnfvof 7687 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼 ∧ 𝑧 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) = ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)))
144139, 140, 141, 142, 143syl22anc 838 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) = ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)))
145144oveq1d 7424 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
146115ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐴 Fn 𝐼)
147 fnfvof 7687 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑦 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯)))
148139, 146, 141, 142, 147syl22anc 838 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯)))
149 fnfvof 7687 . . . . . . . . . . . 12 (((𝑧 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯)))
150140, 146, 141, 142, 149syl22anc 838 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯)))
151148, 150oveq12d 7427 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f Β· 𝐴)β€˜π‘₯)(+gβ€˜π‘‡)((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
152138, 145, 1513eqtr4d 2783 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = (((𝑦 ∘f Β· 𝐴)β€˜π‘₯)(+gβ€˜π‘‡)((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
153114adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦 ∘f (+gβ€˜π‘…)𝑧) Fn 𝐼)
154 fnfvof 7687 . . . . . . . . . 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 7687 . . . . . . . . . 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 2783 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))β€˜π‘₯))
161117, 122, 160eqfnfvd 7036 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)))
162107, 161eqtrd 2773 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)))
163162oveq2d 7425 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))))
164101, 163eqtrd 2773 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))))
165 oveq1 7416 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (π‘₯ ∘f Β· 𝐴) = (𝑦 ∘f Β· 𝐴))
166165oveq2d 7425 . . . . . . 7 (π‘₯ = 𝑦 β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
167 ovex 7442 . . . . . . 7 (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)) ∈ V
168166, 76, 167fvmpt 6999 . . . . . 6 (𝑦 ∈ 𝐡 β†’ (πΈβ€˜π‘¦) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
169168ad2antrl 727 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜π‘¦) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
170 oveq1 7416 . . . . . . . 8 (π‘₯ = 𝑧 β†’ (π‘₯ ∘f Β· 𝐴) = (𝑧 ∘f Β· 𝐴))
171170oveq2d 7425 . . . . . . 7 (π‘₯ = 𝑧 β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
172 ovex 7442 . . . . . . 7 (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ V
173171, 76, 172fvmpt 6999 . . . . . 6 (𝑧 ∈ 𝐡 β†’ (πΈβ€˜π‘§) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
174173ad2antll 728 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜π‘§) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
175169, 174oveq12d 7427 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((πΈβ€˜π‘¦)(+gβ€˜π‘‡)(πΈβ€˜π‘§)) = ((𝑇 Ξ£g (𝑦 ∘f Β· 𝐴))(+gβ€˜π‘‡)(𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
17693, 164, 1753eqtr4d 2783 . . 3 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = ((πΈβ€˜π‘¦)(+gβ€˜π‘‡)(πΈβ€˜π‘§)))
1771, 19, 20, 21, 23, 25, 77, 176isghmd 19101 . 2 (πœ‘ β†’ 𝐸 ∈ (𝐹 GrpHom 𝑇))
1788adantr 482 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑇 ∈ LMod)
17912adantr 482 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝐼 ∈ 𝑋)
18018fveq2d 6896 . . . . . . . 8 (πœ‘ β†’ (Baseβ€˜(Scalarβ€˜π‘‡)) = (Baseβ€˜(Scalarβ€˜πΉ)))
181180eleq2d 2820 . . . . . . 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 7087 . . . . 5 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) ∈ 𝐢)
18652feqmptd 6961 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
187186, 73eqbrtrrd 5173 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) finSupp (0gβ€˜π‘‡))
188187adantrl 715 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) finSupp (0gβ€˜π‘‡))
18919, 5, 43, 32, 21, 3, 178, 179, 183, 185, 188gsumvsmul 20536 . . . 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 20489 . . . . . . . . . . . 12 ((𝐹 ∈ LMod ∧ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡)
194190, 191, 192, 193syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡)
19513, 46, 1frlmbasf 21315 . . . . . . . . . . 11 ((𝐼 ∈ 𝑋 ∧ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧):𝐼⟢(Baseβ€˜π‘…))
196179, 194, 195syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧):𝐼⟢(Baseβ€˜π‘…))
197196ffnd 6719 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) Fn 𝐼)
198115adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴 Fn 𝐼)
199197, 198, 179, 179, 51offn 7683 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) Fn 𝐼)
200 dffn2 6720 . . . . . . . 8 (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) Fn 𝐼 ↔ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴):𝐼⟢V)
201199, 200sylib 217 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴):𝐼⟢V)
202201feqmptd 6961 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯)))
2037fveq2d 6896 . . . . . . . . . . . 12 (πœ‘ β†’ (.rβ€˜π‘…) = (.rβ€˜(Scalarβ€˜π‘‡)))
204203ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (.rβ€˜π‘…) = (.rβ€˜(Scalarβ€˜π‘‡)))
205204oveqd 7426 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) = (𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)))
206205oveq1d 7424 . . . . . . . . 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 2837 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
21148ffvelcdmda 7087 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜π‘…))
21239ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
213211, 212eleqtrd 2836 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
214213adantlrl 719 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
21549ffvelcdmda 7087 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
216215adantlr 714 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
217 eqid 2733 . . . . . . . . . . 11 (.rβ€˜(Scalarβ€˜π‘‡)) = (.rβ€˜(Scalarβ€˜π‘‡))
21819, 5, 3, 43, 217lmodvsass 20497 . . . . . . . . . 10 ((𝑇 ∈ LMod ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ (π΄β€˜π‘₯) ∈ 𝐢)) β†’ ((𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
219207, 210, 214, 216, 218syl13anc 1373 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
220206, 219eqtrd 2773 . . . . . . . 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 7687 . . . . . . . . . 10 ((((𝑦( ·𝑠 β€˜πΉ)𝑧) Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
226221, 222, 223, 224, 225syl22anc 838 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
22717fveq2d 6896 . . . . . . . . . . . . 13 (πœ‘ β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜πΉ)))
228227ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜πΉ)))
229208, 228eleqtrrd 2837 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑦 ∈ (Baseβ€˜π‘…))
230 simplrr 777 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑧 ∈ 𝐡)
231 eqid 2733 . . . . . . . . . . 11 (.rβ€˜π‘…) = (.rβ€˜π‘…)
23213, 1, 46, 223, 229, 230, 224, 2, 231frlmvscaval 21323 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) = (𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)))
233232oveq1d 7424 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
234226, 233eqtrd 2773 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
23548ffnd 6719 . . . . . . . . . . . 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 7425 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
240220, 234, 2393eqtr4d 2783 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
241240mpteq2dva 5249 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (π‘₯ ∈ 𝐼 ↦ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯)) = (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
242202, 241eqtrd 2773 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
243242oveq2d 7425 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))))
244184feqmptd 6961 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
245244oveq2d 7425 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
246245oveq2d 7425 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))) = (𝑦 Β· (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))))
247189, 243, 2463eqtr4d 2783 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
248 oveq1 7416 . . . . . 6 (π‘₯ = (𝑦( ·𝑠 β€˜πΉ)𝑧) β†’ (π‘₯ ∘f Β· 𝐴) = ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴))
249248oveq2d 7425 . . . . 5 (π‘₯ = (𝑦( ·𝑠 β€˜πΉ)𝑧) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
250 ovex 7442 . . . . 5 (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) ∈ V
251249, 76, 250fvmpt 6999 . . . 4 ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡 β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
252194, 251syl 17 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
253173oveq2d 7425 . . . 4 (𝑧 ∈ 𝐡 β†’ (𝑦 Β· (πΈβ€˜π‘§)) = (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
254253ad2antll 728 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 Β· (πΈβ€˜π‘§)) = (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
255247, 252, 2543eqtr4d 2783 . 2 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑦 Β· (πΈβ€˜π‘§)))
2561, 2, 3, 4, 5, 6, 15, 8, 18, 177, 255islmhmd 20650 1 (πœ‘ β†’ 𝐸 ∈ (𝐹 LMHom 𝑇))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475   βŠ† wss 3949   class class class wbr 5149   ↦ cmpt 5232  Fun wfun 6538   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∘f cof 7668   supp csupp 8146  Fincfn 8939   finSupp cfsupp 9361  Basecbs 17144  +gcplusg 17197  .rcmulr 17198  Scalarcsca 17200   ·𝑠 cvsca 17201  0gc0g 17385   Ξ£g cgsu 17386  Grpcgrp 18819  CMndccmn 19648  Ringcrg 20056  LModclmod 20471   LMHom clmhm 20630   freeLMod cfrlm 21301
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 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-sup 9437  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-fz 13485  df-fzo 13628  df-seq 13967  df-hash 14291  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-sca 17213  df-vsca 17214  df-ip 17215  df-tset 17216  df-ple 17217  df-ds 17219  df-hom 17221  df-cco 17222  df-0g 17387  df-gsum 17388  df-prds 17393  df-pws 17395  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-mhm 18671  df-submnd 18672  df-grp 18822  df-minusg 18823  df-sbg 18824  df-subg 19003  df-ghm 19090  df-cntz 19181  df-cmn 19650  df-abl 19651  df-mgp 19988  df-ur 20005  df-ring 20058  df-subrg 20317  df-lmod 20473  df-lss 20543  df-lmhm 20633  df-sra 20785  df-rgmod 20786  df-dsmm 21287  df-frlm 21302
This theorem is referenced by:  frlmup3  21355  frlmup4  21356  islindf5  21394  indlcim  21395  lnrfg  41909
  Copyright terms: Public domain W3C validator