| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frlmup.b | . 2
⊢ 𝐵 = (Base‘𝐹) | 
| 2 |  | eqid 2736 | . 2
⊢ (
·𝑠 ‘𝐹) = ( ·𝑠
‘𝐹) | 
| 3 |  | frlmup.v | . 2
⊢  · = (
·𝑠 ‘𝑇) | 
| 4 |  | eqid 2736 | . 2
⊢
(Scalar‘𝐹) =
(Scalar‘𝐹) | 
| 5 |  | eqid 2736 | . 2
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) | 
| 6 |  | eqid 2736 | . 2
⊢
(Base‘(Scalar‘𝐹)) = (Base‘(Scalar‘𝐹)) | 
| 7 |  | frlmup.r | . . . 4
⊢ (𝜑 → 𝑅 = (Scalar‘𝑇)) | 
| 8 |  | frlmup.t | . . . . 5
⊢ (𝜑 → 𝑇 ∈ LMod) | 
| 9 | 5 | lmodring 20867 | . . . . 5
⊢ (𝑇 ∈ LMod →
(Scalar‘𝑇) ∈
Ring) | 
| 10 | 8, 9 | syl 17 | . . . 4
⊢ (𝜑 → (Scalar‘𝑇) ∈ Ring) | 
| 11 | 7, 10 | eqeltrd 2840 | . . 3
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 12 |  | frlmup.i | . . 3
⊢ (𝜑 → 𝐼 ∈ 𝑋) | 
| 13 |  | frlmup.f | . . . 4
⊢ 𝐹 = (𝑅 freeLMod 𝐼) | 
| 14 | 13 | frlmlmod 21770 | . . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) → 𝐹 ∈ LMod) | 
| 15 | 11, 12, 14 | syl2anc 584 | . 2
⊢ (𝜑 → 𝐹 ∈ LMod) | 
| 16 | 13 | frlmsca 21774 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋) → 𝑅 = (Scalar‘𝐹)) | 
| 17 | 11, 12, 16 | syl2anc 584 | . . 3
⊢ (𝜑 → 𝑅 = (Scalar‘𝐹)) | 
| 18 | 7, 17 | eqtr3d 2778 | . 2
⊢ (𝜑 → (Scalar‘𝑇) = (Scalar‘𝐹)) | 
| 19 |  | frlmup.c | . . 3
⊢ 𝐶 = (Base‘𝑇) | 
| 20 |  | eqid 2736 | . . 3
⊢
(+g‘𝐹) = (+g‘𝐹) | 
| 21 |  | eqid 2736 | . . 3
⊢
(+g‘𝑇) = (+g‘𝑇) | 
| 22 |  | lmodgrp 20866 | . . . 4
⊢ (𝐹 ∈ LMod → 𝐹 ∈ Grp) | 
| 23 | 15, 22 | syl 17 | . . 3
⊢ (𝜑 → 𝐹 ∈ Grp) | 
| 24 |  | lmodgrp 20866 | . . . 4
⊢ (𝑇 ∈ LMod → 𝑇 ∈ Grp) | 
| 25 | 8, 24 | syl 17 | . . 3
⊢ (𝜑 → 𝑇 ∈ Grp) | 
| 26 |  | eleq1w 2823 | . . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵)) | 
| 27 | 26 | anbi2d 630 | . . . . . 6
⊢ (𝑧 = 𝑥 → ((𝜑 ∧ 𝑧 ∈ 𝐵) ↔ (𝜑 ∧ 𝑥 ∈ 𝐵))) | 
| 28 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 ∘f · 𝐴) = (𝑥 ∘f · 𝐴)) | 
| 29 | 28 | oveq2d 7448 | . . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑇 Σg (𝑧 ∘f · 𝐴)) = (𝑇 Σg (𝑥 ∘f · 𝐴))) | 
| 30 | 29 | eleq1d 2825 | . . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑇 Σg (𝑧 ∘f · 𝐴)) ∈ 𝐶 ↔ (𝑇 Σg (𝑥 ∘f · 𝐴)) ∈ 𝐶)) | 
| 31 | 27, 30 | imbi12d 344 | . . . . 5
⊢ (𝑧 = 𝑥 → (((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑇 Σg (𝑧 ∘f · 𝐴)) ∈ 𝐶) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑇 Σg (𝑥 ∘f · 𝐴)) ∈ 𝐶))) | 
| 32 |  | eqid 2736 | . . . . . 6
⊢
(0g‘𝑇) = (0g‘𝑇) | 
| 33 |  | lmodcmn 20909 | . . . . . . . 8
⊢ (𝑇 ∈ LMod → 𝑇 ∈ CMnd) | 
| 34 | 8, 33 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑇 ∈ CMnd) | 
| 35 | 34 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑇 ∈ CMnd) | 
| 36 | 12 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐼 ∈ 𝑋) | 
| 37 | 8 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → 𝑇 ∈ LMod) | 
| 38 |  | simprl 770 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (Base‘𝑅)) | 
| 39 | 7 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑇))) | 
| 40 | 39 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → (Base‘𝑅) = (Base‘(Scalar‘𝑇))) | 
| 41 | 38, 40 | eleqtrd 2842 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (Base‘(Scalar‘𝑇))) | 
| 42 |  | simprr 772 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶) | 
| 43 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇)) | 
| 44 | 19, 5, 3, 43 | lmodvscl 20877 | . . . . . . . 8
⊢ ((𝑇 ∈ LMod ∧ 𝑥 ∈
(Base‘(Scalar‘𝑇)) ∧ 𝑦 ∈ 𝐶) → (𝑥 · 𝑦) ∈ 𝐶) | 
| 45 | 37, 41, 42, 44 | syl3anc 1372 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ 𝐶)) → (𝑥 · 𝑦) ∈ 𝐶) | 
| 46 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 47 | 13, 46, 1 | frlmbasf 21781 | . . . . . . . 8
⊢ ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐵) → 𝑧:𝐼⟶(Base‘𝑅)) | 
| 48 | 12, 47 | sylan 580 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧:𝐼⟶(Base‘𝑅)) | 
| 49 |  | frlmup.a | . . . . . . . 8
⊢ (𝜑 → 𝐴:𝐼⟶𝐶) | 
| 50 | 49 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐴:𝐼⟶𝐶) | 
| 51 |  | inidm 4226 | . . . . . . 7
⊢ (𝐼 ∩ 𝐼) = 𝐼 | 
| 52 | 45, 48, 50, 36, 36, 51 | off 7716 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘f · 𝐴):𝐼⟶𝐶) | 
| 53 |  | ovexd 7467 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘f · 𝐴) ∈ V) | 
| 54 | 52 | ffund 6739 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → Fun (𝑧 ∘f · 𝐴)) | 
| 55 |  | fvexd 6920 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (0g‘𝑇) ∈ V) | 
| 56 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 57 | 13, 56, 1 | frlmbasfsupp 21779 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑋 ∧ 𝑧 ∈ 𝐵) → 𝑧 finSupp (0g‘𝑅)) | 
| 58 | 12, 57 | sylan 580 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 finSupp (0g‘𝑅)) | 
| 59 | 7 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝜑 → (0g‘𝑅) =
(0g‘(Scalar‘𝑇))) | 
| 60 | 59 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (𝜑 →
(0g‘(Scalar‘𝑇)) = (0g‘𝑅)) | 
| 61 | 60 | breq2d 5154 | . . . . . . . . . 10
⊢ (𝜑 → (𝑧 finSupp
(0g‘(Scalar‘𝑇)) ↔ 𝑧 finSupp (0g‘𝑅))) | 
| 62 | 61 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 finSupp
(0g‘(Scalar‘𝑇)) ↔ 𝑧 finSupp (0g‘𝑅))) | 
| 63 | 58, 62 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 finSupp
(0g‘(Scalar‘𝑇))) | 
| 64 | 63 | fsuppimpd 9410 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 supp
(0g‘(Scalar‘𝑇))) ∈ Fin) | 
| 65 |  | ssidd 4006 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 supp
(0g‘(Scalar‘𝑇))) ⊆ (𝑧 supp
(0g‘(Scalar‘𝑇)))) | 
| 66 | 8 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑤 ∈ 𝐶) → 𝑇 ∈ LMod) | 
| 67 |  | eqid 2736 | . . . . . . . . . 10
⊢
(0g‘(Scalar‘𝑇)) =
(0g‘(Scalar‘𝑇)) | 
| 68 | 19, 5, 3, 67, 32 | lmod0vs 20894 | . . . . . . . . 9
⊢ ((𝑇 ∈ LMod ∧ 𝑤 ∈ 𝐶) →
((0g‘(Scalar‘𝑇)) · 𝑤) = (0g‘𝑇)) | 
| 69 | 66, 68 | sylancom 588 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑤 ∈ 𝐶) →
((0g‘(Scalar‘𝑇)) · 𝑤) = (0g‘𝑇)) | 
| 70 |  | fvexd 6920 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) →
(0g‘(Scalar‘𝑇)) ∈ V) | 
| 71 | 65, 69, 48, 50, 36, 70 | suppssof1 8225 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((𝑧 ∘f · 𝐴) supp (0g‘𝑇)) ⊆ (𝑧 supp
(0g‘(Scalar‘𝑇)))) | 
| 72 |  | suppssfifsupp 9421 | . . . . . . 7
⊢ ((((𝑧 ∘f · 𝐴) ∈ V ∧ Fun (𝑧 ∘f · 𝐴) ∧
(0g‘𝑇)
∈ V) ∧ ((𝑧 supp
(0g‘(Scalar‘𝑇))) ∈ Fin ∧ ((𝑧 ∘f · 𝐴) supp (0g‘𝑇)) ⊆ (𝑧 supp
(0g‘(Scalar‘𝑇))))) → (𝑧 ∘f · 𝐴) finSupp (0g‘𝑇)) | 
| 73 | 53, 54, 55, 64, 71, 72 | syl32anc 1379 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘f · 𝐴) finSupp (0g‘𝑇)) | 
| 74 | 19, 32, 35, 36, 52, 73 | gsumcl 19934 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑇 Σg (𝑧 ∘f · 𝐴)) ∈ 𝐶) | 
| 75 | 31, 74 | chvarvv 1997 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑇 Σg (𝑥 ∘f · 𝐴)) ∈ 𝐶) | 
| 76 |  | frlmup.e | . . . 4
⊢ 𝐸 = (𝑥 ∈ 𝐵 ↦ (𝑇 Σg (𝑥 ∘f · 𝐴))) | 
| 77 | 75, 76 | fmptd 7133 | . . 3
⊢ (𝜑 → 𝐸:𝐵⟶𝐶) | 
| 78 | 34 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑇 ∈ CMnd) | 
| 79 | 12 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐼 ∈ 𝑋) | 
| 80 |  | eleq1w 2823 | . . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) | 
| 81 | 80 | anbi2d 630 | . . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝜑 ∧ 𝑧 ∈ 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐵))) | 
| 82 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑧 ∘f · 𝐴) = (𝑦 ∘f · 𝐴)) | 
| 83 | 82 | feq1d 6719 | . . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝑧 ∘f · 𝐴):𝐼⟶𝐶 ↔ (𝑦 ∘f · 𝐴):𝐼⟶𝐶)) | 
| 84 | 81, 83 | imbi12d 344 | . . . . . . 7
⊢ (𝑧 = 𝑦 → (((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘f · 𝐴):𝐼⟶𝐶) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∘f · 𝐴):𝐼⟶𝐶))) | 
| 85 | 84, 52 | chvarvv 1997 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∘f · 𝐴):𝐼⟶𝐶) | 
| 86 | 85 | adantrr 717 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 ∘f · 𝐴):𝐼⟶𝐶) | 
| 87 | 52 | adantrl 716 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑧 ∘f · 𝐴):𝐼⟶𝐶) | 
| 88 | 82 | breq1d 5152 | . . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝑧 ∘f · 𝐴) finSupp (0g‘𝑇) ↔ (𝑦 ∘f · 𝐴) finSupp (0g‘𝑇))) | 
| 89 | 81, 88 | imbi12d 344 | . . . . . . 7
⊢ (𝑧 = 𝑦 → (((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘f · 𝐴) finSupp (0g‘𝑇)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∘f · 𝐴) finSupp (0g‘𝑇)))) | 
| 90 | 89, 73 | chvarvv 1997 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∘f · 𝐴) finSupp (0g‘𝑇)) | 
| 91 | 90 | adantrr 717 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 ∘f · 𝐴) finSupp (0g‘𝑇)) | 
| 92 | 73 | adantrl 716 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑧 ∘f · 𝐴) finSupp (0g‘𝑇)) | 
| 93 | 19, 32, 21, 78, 79, 86, 87, 91, 92 | gsumadd 19942 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg ((𝑦 ∘f · 𝐴) ∘f
(+g‘𝑇)(𝑧 ∘f · 𝐴))) = ((𝑇 Σg (𝑦 ∘f · 𝐴))(+g‘𝑇)(𝑇 Σg (𝑧 ∘f · 𝐴)))) | 
| 94 | 1, 20 | lmodvacl 20874 | . . . . . . . 8
⊢ ((𝐹 ∈ LMod ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝐹)𝑧) ∈ 𝐵) | 
| 95 | 94 | 3expb 1120 | . . . . . . 7
⊢ ((𝐹 ∈ LMod ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝐹)𝑧) ∈ 𝐵) | 
| 96 | 15, 95 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝐹)𝑧) ∈ 𝐵) | 
| 97 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = (𝑦(+g‘𝐹)𝑧) → (𝑥 ∘f · 𝐴) = ((𝑦(+g‘𝐹)𝑧) ∘f · 𝐴)) | 
| 98 | 97 | oveq2d 7448 | . . . . . . 7
⊢ (𝑥 = (𝑦(+g‘𝐹)𝑧) → (𝑇 Σg (𝑥 ∘f · 𝐴)) = (𝑇 Σg ((𝑦(+g‘𝐹)𝑧) ∘f · 𝐴))) | 
| 99 |  | ovex 7465 | . . . . . . 7
⊢ (𝑇 Σg
((𝑦(+g‘𝐹)𝑧) ∘f · 𝐴)) ∈ V | 
| 100 | 98, 76, 99 | fvmpt 7015 | . . . . . 6
⊢ ((𝑦(+g‘𝐹)𝑧) ∈ 𝐵 → (𝐸‘(𝑦(+g‘𝐹)𝑧)) = (𝑇 Σg ((𝑦(+g‘𝐹)𝑧) ∘f · 𝐴))) | 
| 101 | 96, 100 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝐸‘(𝑦(+g‘𝐹)𝑧)) = (𝑇 Σg ((𝑦(+g‘𝐹)𝑧) ∘f · 𝐴))) | 
| 102 | 11 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑅 ∈ Ring) | 
| 103 |  | simprl 770 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑦 ∈ 𝐵) | 
| 104 |  | simprr 772 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧 ∈ 𝐵) | 
| 105 |  | eqid 2736 | . . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 106 | 13, 1, 102, 79, 103, 104, 105, 20 | frlmplusgval 21785 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝐹)𝑧) = (𝑦 ∘f
(+g‘𝑅)𝑧)) | 
| 107 | 106 | oveq1d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦(+g‘𝐹)𝑧) ∘f · 𝐴) = ((𝑦 ∘f
(+g‘𝑅)𝑧) ∘f · 𝐴)) | 
| 108 | 13, 46, 1 | frlmbasf 21781 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑋 ∧ 𝑦 ∈ 𝐵) → 𝑦:𝐼⟶(Base‘𝑅)) | 
| 109 | 12, 108 | sylan 580 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦:𝐼⟶(Base‘𝑅)) | 
| 110 | 109 | adantrr 717 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑦:𝐼⟶(Base‘𝑅)) | 
| 111 | 110 | ffnd 6736 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑦 Fn 𝐼) | 
| 112 | 48 | adantrl 716 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧:𝐼⟶(Base‘𝑅)) | 
| 113 | 112 | ffnd 6736 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧 Fn 𝐼) | 
| 114 | 111, 113,
79, 79, 51 | offn 7711 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 ∘f
(+g‘𝑅)𝑧) Fn 𝐼) | 
| 115 | 49 | ffnd 6736 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 Fn 𝐼) | 
| 116 | 115 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐴 Fn 𝐼) | 
| 117 | 114, 116,
79, 79, 51 | offn 7711 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦 ∘f
(+g‘𝑅)𝑧) ∘f · 𝐴) Fn 𝐼) | 
| 118 | 85 | ffnd 6736 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∘f · 𝐴) Fn 𝐼) | 
| 119 | 118 | adantrr 717 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 ∘f · 𝐴) Fn 𝐼) | 
| 120 | 52 | ffnd 6736 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘f · 𝐴) Fn 𝐼) | 
| 121 | 120 | adantrl 716 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑧 ∘f · 𝐴) Fn 𝐼) | 
| 122 | 119, 121,
79, 79, 51 | offn 7711 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦 ∘f · 𝐴) ∘f
(+g‘𝑇)(𝑧 ∘f · 𝐴)) Fn 𝐼) | 
| 123 | 7 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (+g‘𝑅) =
(+g‘(Scalar‘𝑇))) | 
| 124 | 123 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (+g‘𝑅) =
(+g‘(Scalar‘𝑇))) | 
| 125 | 124 | oveqd 7449 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥)) = ((𝑦‘𝑥)(+g‘(Scalar‘𝑇))(𝑧‘𝑥))) | 
| 126 | 125 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)) = (((𝑦‘𝑥)(+g‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥))) | 
| 127 | 8 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ LMod) | 
| 128 | 110 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) ∈ (Base‘𝑅)) | 
| 129 | 39 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑇))) | 
| 130 | 128, 129 | eleqtrd 2842 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦‘𝑥) ∈ (Base‘(Scalar‘𝑇))) | 
| 131 | 112 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑧‘𝑥) ∈ (Base‘𝑅)) | 
| 132 | 131, 129 | eleqtrd 2842 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑧‘𝑥) ∈ (Base‘(Scalar‘𝑇))) | 
| 133 | 49 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐴:𝐼⟶𝐶) | 
| 134 | 133 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝐴‘𝑥) ∈ 𝐶) | 
| 135 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(+g‘(Scalar‘𝑇)) =
(+g‘(Scalar‘𝑇)) | 
| 136 | 19, 21, 5, 3, 43, 135 | lmodvsdir 20885 | . . . . . . . . . . . 12
⊢ ((𝑇 ∈ LMod ∧ ((𝑦‘𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝑧‘𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐴‘𝑥) ∈ 𝐶)) → (((𝑦‘𝑥)(+g‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥)) = (((𝑦‘𝑥) · (𝐴‘𝑥))(+g‘𝑇)((𝑧‘𝑥) · (𝐴‘𝑥)))) | 
| 137 | 127, 130,
132, 134, 136 | syl13anc 1373 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦‘𝑥)(+g‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥)) = (((𝑦‘𝑥) · (𝐴‘𝑥))(+g‘𝑇)((𝑧‘𝑥) · (𝐴‘𝑥)))) | 
| 138 | 126, 137 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)) = (((𝑦‘𝑥) · (𝐴‘𝑥))(+g‘𝑇)((𝑧‘𝑥) · (𝐴‘𝑥)))) | 
| 139 | 111 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑦 Fn 𝐼) | 
| 140 | 113 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑧 Fn 𝐼) | 
| 141 | 12 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑋) | 
| 142 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) | 
| 143 |  | fnfvof 7715 | . . . . . . . . . . . 12
⊢ (((𝑦 Fn 𝐼 ∧ 𝑧 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → ((𝑦 ∘f
(+g‘𝑅)𝑧)‘𝑥) = ((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥))) | 
| 144 | 139, 140,
141, 142, 143 | syl22anc 838 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∘f
(+g‘𝑅)𝑧)‘𝑥) = ((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥))) | 
| 145 | 144 | oveq1d 7447 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘f
(+g‘𝑅)𝑧)‘𝑥) · (𝐴‘𝑥)) = (((𝑦‘𝑥)(+g‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥))) | 
| 146 | 115 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝐴 Fn 𝐼) | 
| 147 |  | fnfvof 7715 | . . . . . . . . . . . 12
⊢ (((𝑦 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → ((𝑦 ∘f · 𝐴)‘𝑥) = ((𝑦‘𝑥) · (𝐴‘𝑥))) | 
| 148 | 139, 146,
141, 142, 147 | syl22anc 838 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∘f · 𝐴)‘𝑥) = ((𝑦‘𝑥) · (𝐴‘𝑥))) | 
| 149 |  | fnfvof 7715 | . . . . . . . . . . . 12
⊢ (((𝑧 Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → ((𝑧 ∘f · 𝐴)‘𝑥) = ((𝑧‘𝑥) · (𝐴‘𝑥))) | 
| 150 | 140, 146,
141, 142, 149 | syl22anc 838 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∘f · 𝐴)‘𝑥) = ((𝑧‘𝑥) · (𝐴‘𝑥))) | 
| 151 | 148, 150 | oveq12d 7450 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘f · 𝐴)‘𝑥)(+g‘𝑇)((𝑧 ∘f · 𝐴)‘𝑥)) = (((𝑦‘𝑥) · (𝐴‘𝑥))(+g‘𝑇)((𝑧‘𝑥) · (𝐴‘𝑥)))) | 
| 152 | 138, 145,
151 | 3eqtr4d 2786 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘f
(+g‘𝑅)𝑧)‘𝑥) · (𝐴‘𝑥)) = (((𝑦 ∘f · 𝐴)‘𝑥)(+g‘𝑇)((𝑧 ∘f · 𝐴)‘𝑥))) | 
| 153 | 114 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∘f
(+g‘𝑅)𝑧) Fn 𝐼) | 
| 154 |  | fnfvof 7715 | . . . . . . . . . 10
⊢ ((((𝑦 ∘f
(+g‘𝑅)𝑧) Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → (((𝑦 ∘f
(+g‘𝑅)𝑧) ∘f · 𝐴)‘𝑥) = (((𝑦 ∘f
(+g‘𝑅)𝑧)‘𝑥) · (𝐴‘𝑥))) | 
| 155 | 153, 146,
141, 142, 154 | syl22anc 838 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘f
(+g‘𝑅)𝑧) ∘f · 𝐴)‘𝑥) = (((𝑦 ∘f
(+g‘𝑅)𝑧)‘𝑥) · (𝐴‘𝑥))) | 
| 156 | 119 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∘f · 𝐴) Fn 𝐼) | 
| 157 | 121 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑧 ∘f · 𝐴) Fn 𝐼) | 
| 158 |  | fnfvof 7715 | . . . . . . . . . 10
⊢ ((((𝑦 ∘f · 𝐴) Fn 𝐼 ∧ (𝑧 ∘f · 𝐴) Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → (((𝑦 ∘f · 𝐴) ∘f
(+g‘𝑇)(𝑧 ∘f · 𝐴))‘𝑥) = (((𝑦 ∘f · 𝐴)‘𝑥)(+g‘𝑇)((𝑧 ∘f · 𝐴)‘𝑥))) | 
| 159 | 156, 157,
141, 142, 158 | syl22anc 838 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘f · 𝐴) ∘f
(+g‘𝑇)(𝑧 ∘f · 𝐴))‘𝑥) = (((𝑦 ∘f · 𝐴)‘𝑥)(+g‘𝑇)((𝑧 ∘f · 𝐴)‘𝑥))) | 
| 160 | 152, 155,
159 | 3eqtr4d 2786 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦 ∘f
(+g‘𝑅)𝑧) ∘f · 𝐴)‘𝑥) = (((𝑦 ∘f · 𝐴) ∘f
(+g‘𝑇)(𝑧 ∘f · 𝐴))‘𝑥)) | 
| 161 | 117, 122,
160 | eqfnfvd 7053 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦 ∘f
(+g‘𝑅)𝑧) ∘f · 𝐴) = ((𝑦 ∘f · 𝐴) ∘f
(+g‘𝑇)(𝑧 ∘f · 𝐴))) | 
| 162 | 107, 161 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦(+g‘𝐹)𝑧) ∘f · 𝐴) = ((𝑦 ∘f · 𝐴) ∘f
(+g‘𝑇)(𝑧 ∘f · 𝐴))) | 
| 163 | 162 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg ((𝑦(+g‘𝐹)𝑧) ∘f · 𝐴)) = (𝑇 Σg ((𝑦 ∘f · 𝐴) ∘f
(+g‘𝑇)(𝑧 ∘f · 𝐴)))) | 
| 164 | 101, 163 | eqtrd 2776 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝐸‘(𝑦(+g‘𝐹)𝑧)) = (𝑇 Σg ((𝑦 ∘f · 𝐴) ∘f
(+g‘𝑇)(𝑧 ∘f · 𝐴)))) | 
| 165 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ∘f · 𝐴) = (𝑦 ∘f · 𝐴)) | 
| 166 | 165 | oveq2d 7448 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑇 Σg (𝑥 ∘f · 𝐴)) = (𝑇 Σg (𝑦 ∘f · 𝐴))) | 
| 167 |  | ovex 7465 | . . . . . . 7
⊢ (𝑇 Σg
(𝑦 ∘f
·
𝐴)) ∈
V | 
| 168 | 166, 76, 167 | fvmpt 7015 | . . . . . 6
⊢ (𝑦 ∈ 𝐵 → (𝐸‘𝑦) = (𝑇 Σg (𝑦 ∘f · 𝐴))) | 
| 169 | 168 | ad2antrl 728 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝐸‘𝑦) = (𝑇 Σg (𝑦 ∘f · 𝐴))) | 
| 170 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ∘f · 𝐴) = (𝑧 ∘f · 𝐴)) | 
| 171 | 170 | oveq2d 7448 | . . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑇 Σg (𝑥 ∘f · 𝐴)) = (𝑇 Σg (𝑧 ∘f · 𝐴))) | 
| 172 |  | ovex 7465 | . . . . . . 7
⊢ (𝑇 Σg
(𝑧 ∘f
·
𝐴)) ∈
V | 
| 173 | 171, 76, 172 | fvmpt 7015 | . . . . . 6
⊢ (𝑧 ∈ 𝐵 → (𝐸‘𝑧) = (𝑇 Σg (𝑧 ∘f · 𝐴))) | 
| 174 | 173 | ad2antll 729 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝐸‘𝑧) = (𝑇 Σg (𝑧 ∘f · 𝐴))) | 
| 175 | 169, 174 | oveq12d 7450 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝐸‘𝑦)(+g‘𝑇)(𝐸‘𝑧)) = ((𝑇 Σg (𝑦 ∘f · 𝐴))(+g‘𝑇)(𝑇 Σg (𝑧 ∘f · 𝐴)))) | 
| 176 | 93, 164, 175 | 3eqtr4d 2786 | . . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝐸‘(𝑦(+g‘𝐹)𝑧)) = ((𝐸‘𝑦)(+g‘𝑇)(𝐸‘𝑧))) | 
| 177 | 1, 19, 20, 21, 23, 25, 77, 176 | isghmd 19244 | . 2
⊢ (𝜑 → 𝐸 ∈ (𝐹 GrpHom 𝑇)) | 
| 178 | 8 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝑇 ∈ LMod) | 
| 179 | 12 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝐼 ∈ 𝑋) | 
| 180 | 18 | fveq2d 6909 | . . . . . . . 8
⊢ (𝜑 →
(Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝐹))) | 
| 181 | 180 | eleq2d 2826 | . . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (Base‘(Scalar‘𝑇)) ↔ 𝑦 ∈ (Base‘(Scalar‘𝐹)))) | 
| 182 | 181 | biimpar 477 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(Scalar‘𝐹))) → 𝑦 ∈ (Base‘(Scalar‘𝑇))) | 
| 183 | 182 | adantrr 717 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝑦 ∈ (Base‘(Scalar‘𝑇))) | 
| 184 | 52 | adantrl 716 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑧 ∘f · 𝐴):𝐼⟶𝐶) | 
| 185 | 184 | ffvelcdmda 7103 | . . . . 5
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∘f · 𝐴)‘𝑥) ∈ 𝐶) | 
| 186 | 52 | feqmptd 6976 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∘f · 𝐴) = (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘f · 𝐴)‘𝑥))) | 
| 187 | 186, 73 | eqbrtrrd 5166 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘f · 𝐴)‘𝑥)) finSupp (0g‘𝑇)) | 
| 188 | 187 | adantrl 716 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘f · 𝐴)‘𝑥)) finSupp (0g‘𝑇)) | 
| 189 | 19, 5, 43, 32, 21, 3, 178, 179, 183, 185, 188 | gsumvsmul 20925 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (𝑦 · ((𝑧 ∘f · 𝐴)‘𝑥)))) = (𝑦 · (𝑇 Σg (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘f · 𝐴)‘𝑥))))) | 
| 190 | 15 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝐹 ∈ LMod) | 
| 191 |  | simprl 770 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝑦 ∈ (Base‘(Scalar‘𝐹))) | 
| 192 |  | simprr 772 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝑧 ∈ 𝐵) | 
| 193 | 1, 4, 2, 6 | lmodvscl 20877 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ LMod ∧ 𝑦 ∈
(Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵) → (𝑦( ·𝑠
‘𝐹)𝑧) ∈ 𝐵) | 
| 194 | 190, 191,
192, 193 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑦( ·𝑠
‘𝐹)𝑧) ∈ 𝐵) | 
| 195 | 13, 46, 1 | frlmbasf 21781 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑋 ∧ (𝑦( ·𝑠
‘𝐹)𝑧) ∈ 𝐵) → (𝑦( ·𝑠
‘𝐹)𝑧):𝐼⟶(Base‘𝑅)) | 
| 196 | 179, 194,
195 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑦( ·𝑠
‘𝐹)𝑧):𝐼⟶(Base‘𝑅)) | 
| 197 | 196 | ffnd 6736 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑦( ·𝑠
‘𝐹)𝑧) Fn 𝐼) | 
| 198 | 115 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝐴 Fn 𝐼) | 
| 199 | 197, 198,
179, 179, 51 | offn 7711 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → ((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴) Fn 𝐼) | 
| 200 |  | dffn2 6737 | . . . . . . . 8
⊢ (((𝑦(
·𝑠 ‘𝐹)𝑧) ∘f · 𝐴) Fn 𝐼 ↔ ((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴):𝐼⟶V) | 
| 201 | 199, 200 | sylib 218 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → ((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴):𝐼⟶V) | 
| 202 | 201 | feqmptd 6976 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → ((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴) = (𝑥 ∈ 𝐼 ↦ (((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴)‘𝑥))) | 
| 203 | 7 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝜑 → (.r‘𝑅) =
(.r‘(Scalar‘𝑇))) | 
| 204 | 203 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (.r‘𝑅) =
(.r‘(Scalar‘𝑇))) | 
| 205 | 204 | oveqd 7449 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦(.r‘𝑅)(𝑧‘𝑥)) = (𝑦(.r‘(Scalar‘𝑇))(𝑧‘𝑥))) | 
| 206 | 205 | oveq1d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦(.r‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)) = ((𝑦(.r‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥))) | 
| 207 | 8 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ LMod) | 
| 208 |  | simplrl 776 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑦 ∈ (Base‘(Scalar‘𝐹))) | 
| 209 | 180 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (Base‘(Scalar‘𝑇)) =
(Base‘(Scalar‘𝐹))) | 
| 210 | 208, 209 | eleqtrrd 2843 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑦 ∈ (Base‘(Scalar‘𝑇))) | 
| 211 | 48 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑧‘𝑥) ∈ (Base‘𝑅)) | 
| 212 | 39 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑇))) | 
| 213 | 211, 212 | eleqtrd 2842 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑥 ∈ 𝐼) → (𝑧‘𝑥) ∈ (Base‘(Scalar‘𝑇))) | 
| 214 | 213 | adantlrl 720 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑧‘𝑥) ∈ (Base‘(Scalar‘𝑇))) | 
| 215 | 49 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐴‘𝑥) ∈ 𝐶) | 
| 216 | 215 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝐴‘𝑥) ∈ 𝐶) | 
| 217 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(.r‘(Scalar‘𝑇)) =
(.r‘(Scalar‘𝑇)) | 
| 218 | 19, 5, 3, 43, 217 | lmodvsass 20886 | . . . . . . . . . 10
⊢ ((𝑇 ∈ LMod ∧ (𝑦 ∈
(Base‘(Scalar‘𝑇)) ∧ (𝑧‘𝑥) ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐴‘𝑥) ∈ 𝐶)) → ((𝑦(.r‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥)) = (𝑦 · ((𝑧‘𝑥) · (𝐴‘𝑥)))) | 
| 219 | 207, 210,
214, 216, 218 | syl13anc 1373 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦(.r‘(Scalar‘𝑇))(𝑧‘𝑥)) · (𝐴‘𝑥)) = (𝑦 · ((𝑧‘𝑥) · (𝐴‘𝑥)))) | 
| 220 | 206, 219 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦(.r‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥)) = (𝑦 · ((𝑧‘𝑥) · (𝐴‘𝑥)))) | 
| 221 | 197 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦( ·𝑠
‘𝐹)𝑧) Fn 𝐼) | 
| 222 | 115 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝐴 Fn 𝐼) | 
| 223 | 12 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑋) | 
| 224 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) | 
| 225 |  | fnfvof 7715 | . . . . . . . . . 10
⊢ ((((𝑦(
·𝑠 ‘𝐹)𝑧) Fn 𝐼 ∧ 𝐴 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼)) → (((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴)‘𝑥) = (((𝑦( ·𝑠
‘𝐹)𝑧)‘𝑥) · (𝐴‘𝑥))) | 
| 226 | 221, 222,
223, 224, 225 | syl22anc 838 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴)‘𝑥) = (((𝑦( ·𝑠
‘𝐹)𝑧)‘𝑥) · (𝐴‘𝑥))) | 
| 227 | 17 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝐹))) | 
| 228 | 227 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝐹))) | 
| 229 | 208, 228 | eleqtrrd 2843 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑦 ∈ (Base‘𝑅)) | 
| 230 |  | simplrr 777 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑧 ∈ 𝐵) | 
| 231 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 232 | 13, 1, 46, 223, 229, 230, 224, 2, 231 | frlmvscaval 21789 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑦( ·𝑠
‘𝐹)𝑧)‘𝑥) = (𝑦(.r‘𝑅)(𝑧‘𝑥))) | 
| 233 | 232 | oveq1d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦( ·𝑠
‘𝐹)𝑧)‘𝑥) · (𝐴‘𝑥)) = ((𝑦(.r‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥))) | 
| 234 | 226, 233 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴)‘𝑥) = ((𝑦(.r‘𝑅)(𝑧‘𝑥)) · (𝐴‘𝑥))) | 
| 235 | 48 | ffnd 6736 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 Fn 𝐼) | 
| 236 | 235 | adantrl 716 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → 𝑧 Fn 𝐼) | 
| 237 | 236 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → 𝑧 Fn 𝐼) | 
| 238 | 237, 222,
223, 224, 149 | syl22anc 838 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∘f · 𝐴)‘𝑥) = ((𝑧‘𝑥) · (𝐴‘𝑥))) | 
| 239 | 238 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑦 · ((𝑧 ∘f · 𝐴)‘𝑥)) = (𝑦 · ((𝑧‘𝑥) · (𝐴‘𝑥)))) | 
| 240 | 220, 234,
239 | 3eqtr4d 2786 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴)‘𝑥) = (𝑦 · ((𝑧 ∘f · 𝐴)‘𝑥))) | 
| 241 | 240 | mpteq2dva 5241 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ (((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴)‘𝑥)) = (𝑥 ∈ 𝐼 ↦ (𝑦 · ((𝑧 ∘f · 𝐴)‘𝑥)))) | 
| 242 | 202, 241 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → ((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴) = (𝑥 ∈ 𝐼 ↦ (𝑦 · ((𝑧 ∘f · 𝐴)‘𝑥)))) | 
| 243 | 242 | oveq2d 7448 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg ((𝑦(
·𝑠 ‘𝐹)𝑧) ∘f · 𝐴)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (𝑦 · ((𝑧 ∘f · 𝐴)‘𝑥))))) | 
| 244 | 184 | feqmptd 6976 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑧 ∘f · 𝐴) = (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘f · 𝐴)‘𝑥))) | 
| 245 | 244 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg (𝑧 ∘f · 𝐴)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘f · 𝐴)‘𝑥)))) | 
| 246 | 245 | oveq2d 7448 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑦 · (𝑇 Σg (𝑧 ∘f · 𝐴))) = (𝑦 · (𝑇 Σg (𝑥 ∈ 𝐼 ↦ ((𝑧 ∘f · 𝐴)‘𝑥))))) | 
| 247 | 189, 243,
246 | 3eqtr4d 2786 | . . 3
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑇 Σg ((𝑦(
·𝑠 ‘𝐹)𝑧) ∘f · 𝐴)) = (𝑦 · (𝑇 Σg (𝑧 ∘f · 𝐴)))) | 
| 248 |  | oveq1 7439 | . . . . . 6
⊢ (𝑥 = (𝑦( ·𝑠
‘𝐹)𝑧) → (𝑥 ∘f · 𝐴) = ((𝑦( ·𝑠
‘𝐹)𝑧) ∘f · 𝐴)) | 
| 249 | 248 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = (𝑦( ·𝑠
‘𝐹)𝑧) → (𝑇 Σg (𝑥 ∘f · 𝐴)) = (𝑇 Σg ((𝑦(
·𝑠 ‘𝐹)𝑧) ∘f · 𝐴))) | 
| 250 |  | ovex 7465 | . . . . 5
⊢ (𝑇 Σg
((𝑦(
·𝑠 ‘𝐹)𝑧) ∘f · 𝐴)) ∈ V | 
| 251 | 249, 76, 250 | fvmpt 7015 | . . . 4
⊢ ((𝑦(
·𝑠 ‘𝐹)𝑧) ∈ 𝐵 → (𝐸‘(𝑦( ·𝑠
‘𝐹)𝑧)) = (𝑇 Σg ((𝑦(
·𝑠 ‘𝐹)𝑧) ∘f · 𝐴))) | 
| 252 | 194, 251 | syl 17 | . . 3
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝐸‘(𝑦( ·𝑠
‘𝐹)𝑧)) = (𝑇 Σg ((𝑦(
·𝑠 ‘𝐹)𝑧) ∘f · 𝐴))) | 
| 253 | 173 | oveq2d 7448 | . . . 4
⊢ (𝑧 ∈ 𝐵 → (𝑦 · (𝐸‘𝑧)) = (𝑦 · (𝑇 Σg (𝑧 ∘f · 𝐴)))) | 
| 254 | 253 | ad2antll 729 | . . 3
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝑦 · (𝐸‘𝑧)) = (𝑦 · (𝑇 Σg (𝑧 ∘f · 𝐴)))) | 
| 255 | 247, 252,
254 | 3eqtr4d 2786 | . 2
⊢ ((𝜑 ∧ (𝑦 ∈ (Base‘(Scalar‘𝐹)) ∧ 𝑧 ∈ 𝐵)) → (𝐸‘(𝑦( ·𝑠
‘𝐹)𝑧)) = (𝑦 · (𝐸‘𝑧))) | 
| 256 | 1, 2, 3, 4, 5, 6, 15, 8, 18, 177, 255 | islmhmd 21039 | 1
⊢ (𝜑 → 𝐸 ∈ (𝐹 LMHom 𝑇)) |