MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frlmup1 Structured version   Visualization version   GIF version
Theorem frlmup1 21572
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 20622 . . . . 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 21523 . . 3 ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) β†’ 𝐹 ∈ LMod)
1511, 12, 14syl2anc 584 . 2 (πœ‘ β†’ 𝐹 ∈ LMod)
1613frlmsca 21527 . . . 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 20621 . . . 4 (𝐹 ∈ LMod β†’ 𝐹 ∈ Grp)
2315, 22syl 17 . . 3 (πœ‘ β†’ 𝐹 ∈ Grp)
24 lmodgrp 20621 . . . 4 (𝑇 ∈ LMod β†’ 𝑇 ∈ Grp)
258, 24syl 17 . . 3 (πœ‘ β†’ 𝑇 ∈ Grp)
26 eleq1w 2816 . . . . . . 7 (𝑧 = π‘₯ β†’ (𝑧 ∈ 𝐡 ↔ π‘₯ ∈ 𝐡))
2726anbi2d 629 . . . . . 6 (𝑧 = π‘₯ β†’ ((πœ‘ ∧ 𝑧 ∈ 𝐡) ↔ (πœ‘ ∧ π‘₯ ∈ 𝐡)))
28 oveq1 7418 . . . . . . . 8 (𝑧 = π‘₯ β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∘f Β· 𝐴))
2928oveq2d 7427 . . . . . . 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 20664 . . . . . . . 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 6895 . . . . . . . . . 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 20632 . . . . . . . 8 ((𝑇 ∈ LMod ∧ π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘‡)) ∧ 𝑦 ∈ 𝐢) β†’ (π‘₯ Β· 𝑦) ∈ 𝐢)
4537, 41, 42, 44syl3anc 1371 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ (π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ 𝐢)) β†’ (π‘₯ Β· 𝑦) ∈ 𝐢)
46 eqid 2732 . . . . . . . . 9 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
4713, 46, 1frlmbasf 21534 . . . . . . . 8 ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐡) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
4812, 47sylan 580 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
49 frlmup.a . . . . . . . 8 (πœ‘ β†’ 𝐴:𝐼⟢𝐢)
5049adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝐴:𝐼⟢𝐢)
51 inidm 4218 . . . . . . 7 (𝐼 ∩ 𝐼) = 𝐼
5245, 48, 50, 36, 36, 51off 7690 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢)
53 ovexd 7446 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) ∈ V)
5452ffund 6721 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ Fun (𝑧 ∘f Β· 𝐴))
55 fvexd 6906 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (0gβ€˜π‘‡) ∈ V)
56 eqid 2732 . . . . . . . . . . 11 (0gβ€˜π‘…) = (0gβ€˜π‘…)
5713, 56, 1frlmbasfsupp 21532 . . . . . . . . . 10 ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜π‘…))
5812, 57sylan 580 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜π‘…))
597fveq2d 6895 . . . . . . . . . . . 12 (πœ‘ β†’ (0gβ€˜π‘…) = (0gβ€˜(Scalarβ€˜π‘‡)))
6059eqcomd 2738 . . . . . . . . . . 11 (πœ‘ β†’ (0gβ€˜(Scalarβ€˜π‘‡)) = (0gβ€˜π‘…))
6160breq2d 5160 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)) ↔ 𝑧 finSupp (0gβ€˜π‘…)))
6261adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)) ↔ 𝑧 finSupp (0gβ€˜π‘…)))
6358, 62mpbird 256 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 finSupp (0gβ€˜(Scalarβ€˜π‘‡)))
6463fsuppimpd 9371 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))) ∈ Fin)
65 ssidd 4005 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))) βŠ† (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))))
668ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ 𝑀 ∈ 𝐢) β†’ 𝑇 ∈ LMod)
67 eqid 2732 . . . . . . . . . 10 (0gβ€˜(Scalarβ€˜π‘‡)) = (0gβ€˜(Scalarβ€˜π‘‡))
6819, 5, 3, 67, 32lmod0vs 20649 . . . . . . . . 9 ((𝑇 ∈ LMod ∧ 𝑀 ∈ 𝐢) β†’ ((0gβ€˜(Scalarβ€˜π‘‡)) Β· 𝑀) = (0gβ€˜π‘‡))
6966, 68sylancom 588 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ 𝑀 ∈ 𝐢) β†’ ((0gβ€˜(Scalarβ€˜π‘‡)) Β· 𝑀) = (0gβ€˜π‘‡))
70 fvexd 6906 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (0gβ€˜(Scalarβ€˜π‘‡)) ∈ V)
7165, 69, 48, 50, 36, 70suppssof1 8186 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ ((𝑧 ∘f Β· 𝐴) supp (0gβ€˜π‘‡)) βŠ† (𝑧 supp (0gβ€˜(Scalarβ€˜π‘‡))))
72 suppssfifsupp 9380 . . . . . . 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 19824 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ 𝐢)
7531, 74chvarvv 2002 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) ∈ 𝐢)
76 frlmup.e . . . 4 𝐸 = (π‘₯ ∈ 𝐡 ↦ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)))
7775, 76fmptd 7115 . . 3 (πœ‘ β†’ 𝐸:𝐡⟢𝐢)
7834adantr 481 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑇 ∈ CMnd)
7912adantr 481 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐼 ∈ 𝑋)
80 eleq1w 2816 . . . . . . . . 9 (𝑧 = 𝑦 β†’ (𝑧 ∈ 𝐡 ↔ 𝑦 ∈ 𝐡))
8180anbi2d 629 . . . . . . . 8 (𝑧 = 𝑦 β†’ ((πœ‘ ∧ 𝑧 ∈ 𝐡) ↔ (πœ‘ ∧ 𝑦 ∈ 𝐡)))
82 oveq1 7418 . . . . . . . . 9 (𝑧 = 𝑦 β†’ (𝑧 ∘f Β· 𝐴) = (𝑦 ∘f Β· 𝐴))
8382feq1d 6702 . . . . . . . 8 (𝑧 = 𝑦 β†’ ((𝑧 ∘f Β· 𝐴):𝐼⟢𝐢 ↔ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢))
8481, 83imbi12d 344 . . . . . . 7 (𝑧 = 𝑦 β†’ (((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢) ↔ ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)))
8584, 52chvarvv 2002 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)
8685adantrr 715 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f Β· 𝐴):𝐼⟢𝐢)
8752adantrl 714 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴):𝐼⟢𝐢)
8882breq1d 5158 . . . . . . . 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 19832 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))) = ((𝑇 Ξ£g (𝑦 ∘f Β· 𝐴))(+gβ€˜π‘‡)(𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
941, 20lmodvacl 20629 . . . . . . . 8 ((𝐹 ∈ LMod ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
95943expb 1120 . . . . . . 7 ((𝐹 ∈ LMod ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
9615, 95sylan 580 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) ∈ 𝐡)
97 oveq1 7418 . . . . . . . 8 (π‘₯ = (𝑦(+gβ€˜πΉ)𝑧) β†’ (π‘₯ ∘f Β· 𝐴) = ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴))
9897oveq2d 7427 . . . . . . 7 (π‘₯ = (𝑦(+gβ€˜πΉ)𝑧) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)))
99 ovex 7444 . . . . . . 7 (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)) ∈ V
10098, 76, 99fvmpt 6998 . . . . . 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 21538 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦(+gβ€˜πΉ)𝑧) = (𝑦 ∘f (+gβ€˜π‘…)𝑧))
107106oveq1d 7426 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴))
10813, 46, 1frlmbasf 21534 . . . . . . . . . . . . 13 ((𝐼 ∈ 𝑋 ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
10912, 108sylan 580 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
110109adantrr 715 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦:𝐼⟢(Baseβ€˜π‘…))
111110ffnd 6718 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑦 Fn 𝐼)
11248adantrl 714 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧:𝐼⟢(Baseβ€˜π‘…))
113112ffnd 6718 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝑧 Fn 𝐼)
114111, 113, 79, 79, 51offn 7685 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f (+gβ€˜π‘…)𝑧) Fn 𝐼)
11549ffnd 6718 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 Fn 𝐼)
116115adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴 Fn 𝐼)
117114, 116, 79, 79, 51offn 7685 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴) Fn 𝐼)
11885ffnd 6718 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 ∘f Β· 𝐴) Fn 𝐼)
119118adantrr 715 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 ∘f Β· 𝐴) Fn 𝐼)
12052ffnd 6718 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) Fn 𝐼)
121120adantrl 714 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴) Fn 𝐼)
122119, 121, 79, 79, 51offn 7685 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)) Fn 𝐼)
1237fveq2d 6895 . . . . . . . . . . . . . 14 (πœ‘ β†’ (+gβ€˜π‘…) = (+gβ€˜(Scalarβ€˜π‘‡)))
124123ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (+gβ€˜π‘…) = (+gβ€˜(Scalarβ€˜π‘‡)))
125124oveqd 7428 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) = ((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)))
126125oveq1d 7426 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯)(+gβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
1278ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝑇 ∈ LMod)
128110ffvelcdmda 7086 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘¦β€˜π‘₯) ∈ (Baseβ€˜π‘…))
12939ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
130128, 129eleqtrd 2835 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘¦β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
131112ffvelcdmda 7086 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜π‘…))
132131, 129eleqtrd 2835 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
13349adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴:𝐼⟢𝐢)
134133ffvelcdmda 7086 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
135 eqid 2732 . . . . . . . . . . . . 13 (+gβ€˜(Scalarβ€˜π‘‡)) = (+gβ€˜(Scalarβ€˜π‘‡))
13619, 21, 5, 3, 43, 135lmodvsdir 20640 . . . . . . . . . . . 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 7689 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼 ∧ 𝑧 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) = ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)))
144139, 140, 141, 142, 143syl22anc 837 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) = ((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)))
145144oveq1d 7426 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = (((π‘¦β€˜π‘₯)(+gβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
146115ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ 𝐴 Fn 𝐼)
147 fnfvof 7689 . . . . . . . . . . . 12 (((𝑦 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑦 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯)))
148139, 146, 141, 142, 147syl22anc 837 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯)))
149 fnfvof 7689 . . . . . . . . . . . 12 (((𝑧 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯)))
150140, 146, 141, 142, 149syl22anc 837 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) = ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯)))
151148, 150oveq12d 7429 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f Β· 𝐴)β€˜π‘₯)(+gβ€˜π‘‡)((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) = (((π‘¦β€˜π‘₯) Β· (π΄β€˜π‘₯))(+gβ€˜π‘‡)((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
152138, 145, 1513eqtr4d 2782 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦 ∘f (+gβ€˜π‘…)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = (((𝑦 ∘f Β· 𝐴)β€˜π‘₯)(+gβ€˜π‘‡)((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
153114adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦 ∘f (+gβ€˜π‘…)𝑧) Fn 𝐼)
154 fnfvof 7689 . . . . . . . . . 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 7689 . . . . . . . . . 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 7035 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦 ∘f (+gβ€˜π‘…)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)))
162107, 161eqtrd 2772 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴) = ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴)))
163162oveq2d 7427 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦(+gβ€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))))
164101, 163eqtrd 2772 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦 ∘f Β· 𝐴) ∘f (+gβ€˜π‘‡)(𝑧 ∘f Β· 𝐴))))
165 oveq1 7418 . . . . . . . 8 (π‘₯ = 𝑦 β†’ (π‘₯ ∘f Β· 𝐴) = (𝑦 ∘f Β· 𝐴))
166165oveq2d 7427 . . . . . . 7 (π‘₯ = 𝑦 β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
167 ovex 7444 . . . . . . 7 (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)) ∈ V
168166, 76, 167fvmpt 6998 . . . . . 6 (𝑦 ∈ 𝐡 β†’ (πΈβ€˜π‘¦) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
169168ad2antrl 726 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜π‘¦) = (𝑇 Ξ£g (𝑦 ∘f Β· 𝐴)))
170 oveq1 7418 . . . . . . . 8 (π‘₯ = 𝑧 β†’ (π‘₯ ∘f Β· 𝐴) = (𝑧 ∘f Β· 𝐴))
171170oveq2d 7427 . . . . . . 7 (π‘₯ = 𝑧 β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
172 ovex 7444 . . . . . . 7 (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) ∈ V
173171, 76, 172fvmpt 6998 . . . . . 6 (𝑧 ∈ 𝐡 β†’ (πΈβ€˜π‘§) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
174173ad2antll 727 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜π‘§) = (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)))
175169, 174oveq12d 7429 . . . 4 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ ((πΈβ€˜π‘¦)(+gβ€˜π‘‡)(πΈβ€˜π‘§)) = ((𝑇 Ξ£g (𝑦 ∘f Β· 𝐴))(+gβ€˜π‘‡)(𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
17693, 164, 1753eqtr4d 2782 . . 3 ((πœ‘ ∧ (𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦(+gβ€˜πΉ)𝑧)) = ((πΈβ€˜π‘¦)(+gβ€˜π‘‡)(πΈβ€˜π‘§)))
1771, 19, 20, 21, 23, 25, 77, 176isghmd 19139 . 2 (πœ‘ β†’ 𝐸 ∈ (𝐹 GrpHom 𝑇))
1788adantr 481 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝑇 ∈ LMod)
17912adantr 481 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝐼 ∈ 𝑋)
18018fveq2d 6895 . . . . . . . 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 7086 . . . . 5 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯) ∈ 𝐢)
18652feqmptd 6960 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
187186, 73eqbrtrrd 5172 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐡) β†’ (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) finSupp (0gβ€˜π‘‡))
188187adantrl 714 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) finSupp (0gβ€˜π‘‡))
18919, 5, 43, 32, 21, 3, 178, 179, 183, 185, 188gsumvsmul 20680 . . . 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 20632 . . . . . . . . . . . 12 ((𝐹 ∈ LMod ∧ 𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡)
194190, 191, 192, 193syl3anc 1371 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡)
19513, 46, 1frlmbasf 21534 . . . . . . . . . . 11 ((𝐼 ∈ 𝑋 ∧ (𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧):𝐼⟢(Baseβ€˜π‘…))
196179, 194, 195syl2anc 584 . . . . . . . . . 10 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧):𝐼⟢(Baseβ€˜π‘…))
197196ffnd 6718 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦( ·𝑠 β€˜πΉ)𝑧) Fn 𝐼)
198115adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ 𝐴 Fn 𝐼)
199197, 198, 179, 179, 51offn 7685 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) Fn 𝐼)
200 dffn2 6719 . . . . . . . 8 (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) Fn 𝐼 ↔ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴):𝐼⟢V)
201199, 200sylib 217 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴):𝐼⟢V)
202201feqmptd 6960 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯)))
2037fveq2d 6895 . . . . . . . . . . . 12 (πœ‘ β†’ (.rβ€˜π‘…) = (.rβ€˜(Scalarβ€˜π‘‡)))
204203ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (.rβ€˜π‘…) = (.rβ€˜(Scalarβ€˜π‘‡)))
205204oveqd 7428 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) = (𝑦(.rβ€˜(Scalarβ€˜π‘‡))(π‘§β€˜π‘₯)))
206205oveq1d 7426 . . . . . . . . 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 7086 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜π‘…))
21239ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (Baseβ€˜π‘…) = (Baseβ€˜(Scalarβ€˜π‘‡)))
213211, 212eleqtrd 2835 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝐡) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
214213adantlrl 718 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π‘§β€˜π‘₯) ∈ (Baseβ€˜(Scalarβ€˜π‘‡)))
21549ffvelcdmda 7086 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
216215adantlr 713 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (π΄β€˜π‘₯) ∈ 𝐢)
217 eqid 2732 . . . . . . . . . . 11 (.rβ€˜(Scalarβ€˜π‘‡)) = (.rβ€˜(Scalarβ€˜π‘‡))
21819, 5, 3, 43, 217lmodvsass 20641 . . . . . . . . . 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 7689 . . . . . . . . . 10 ((((𝑦( ·𝑠 β€˜πΉ)𝑧) Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐼)) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
226221, 222, 223, 224, 225syl22anc 837 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)))
22717fveq2d 6895 . . . . . . . . . . . . 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 21542 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) = (𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)))
233232oveq1d 7426 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧)β€˜π‘₯) Β· (π΄β€˜π‘₯)) = ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
234226, 233eqtrd 2772 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = ((𝑦(.rβ€˜π‘…)(π‘§β€˜π‘₯)) Β· (π΄β€˜π‘₯)))
23548ffnd 6718 . . . . . . . . . . . 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 7427 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)) = (𝑦 Β· ((π‘§β€˜π‘₯) Β· (π΄β€˜π‘₯))))
240220, 234, 2393eqtr4d 2782 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) ∧ π‘₯ ∈ 𝐼) β†’ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯) = (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
241240mpteq2dva 5248 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (π‘₯ ∈ 𝐼 ↦ (((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)β€˜π‘₯)) = (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
242202, 241eqtrd 2772 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
243242oveq2d 7427 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ (𝑦 Β· ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))))
244184feqmptd 6960 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑧 ∘f Β· 𝐴) = (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))
245244oveq2d 7427 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴)) = (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯))))
246245oveq2d 7427 . . . 4 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))) = (𝑦 Β· (𝑇 Ξ£g (π‘₯ ∈ 𝐼 ↦ ((𝑧 ∘f Β· 𝐴)β€˜π‘₯)))))
247189, 243, 2463eqtr4d 2782 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) = (𝑦 Β· (𝑇 Ξ£g (𝑧 ∘f Β· 𝐴))))
248 oveq1 7418 . . . . . 6 (π‘₯ = (𝑦( ·𝑠 β€˜πΉ)𝑧) β†’ (π‘₯ ∘f Β· 𝐴) = ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴))
249248oveq2d 7427 . . . . 5 (π‘₯ = (𝑦( ·𝑠 β€˜πΉ)𝑧) β†’ (𝑇 Ξ£g (π‘₯ ∘f Β· 𝐴)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
250 ovex 7444 . . . . 5 (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)) ∈ V
251249, 76, 250fvmpt 6998 . . . 4 ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∈ 𝐡 β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
252194, 251syl 17 . . 3 ((πœ‘ ∧ (𝑦 ∈ (Baseβ€˜(Scalarβ€˜πΉ)) ∧ 𝑧 ∈ 𝐡)) β†’ (πΈβ€˜(𝑦( ·𝑠 β€˜πΉ)𝑧)) = (𝑇 Ξ£g ((𝑦( ·𝑠 β€˜πΉ)𝑧) ∘f Β· 𝐴)))
253173oveq2d 7427 . . . 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 20794 1 (πœ‘ β†’ 𝐸 ∈ (𝐹 LMHom 𝑇))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3474   βŠ† wss 3948   class class class wbr 5148   ↦ cmpt 5231  Fun wfun 6537   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411   ∘f cof 7670   supp csupp 8148  Fincfn 8941   finSupp cfsupp 9363  Basecbs 17148  +gcplusg 17201  .rcmulr 17202  Scalarcsca 17204   ·𝑠 cvsca 17205  0gc0g 17389   Ξ£g cgsu 17390  Grpcgrp 18855  CMndccmn 19689  Ringcrg 20127  LModclmod 20614   LMHom clmhm 20774   freeLMod cfrlm 21520
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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-fz 13489  df-fzo 13632  df-seq 13971  df-hash 14295  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-hom 17225  df-cco 17226  df-0g 17391  df-gsum 17392  df-prds 17397  df-pws 17399  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-mhm 18705  df-submnd 18706  df-grp 18858  df-minusg 18859  df-sbg 18860  df-subg 19039  df-ghm 19128  df-cntz 19222  df-cmn 19691  df-abl 19692  df-mgp 20029  df-rng 20047  df-ur 20076  df-ring 20129  df-subrg 20459  df-lmod 20616  df-lss 20687  df-lmhm 20777  df-sra 20930  df-rgmod 20931  df-dsmm 21506  df-frlm 21521
This theorem is referenced by:  frlmup3  21574  frlmup4  21575  islindf5  21613  indlcim  21614  lnrfg  42163
  Copyright terms: Public domain W3C validator