| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | evlslem1.b | . . 3
⊢ 𝐵 = (Base‘𝑃) | 
| 2 |  | eqid 2736 | . . 3
⊢
(1r‘𝑃) = (1r‘𝑃) | 
| 3 |  | eqid 2736 | . . 3
⊢
(1r‘𝑆) = (1r‘𝑆) | 
| 4 |  | eqid 2736 | . . 3
⊢
(.r‘𝑃) = (.r‘𝑃) | 
| 5 |  | evlslem1.m | . . 3
⊢  · =
(.r‘𝑆) | 
| 6 |  | evlslem1.p | . . . 4
⊢ 𝑃 = (𝐼 mPoly 𝑅) | 
| 7 |  | evlslem1.i | . . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑊) | 
| 8 |  | evlslem1.r | . . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 9 | 8 | crngringd 20244 | . . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 10 | 6, 7, 9 | mplringd 22044 | . . 3
⊢ (𝜑 → 𝑃 ∈ Ring) | 
| 11 |  | evlslem1.s | . . . 4
⊢ (𝜑 → 𝑆 ∈ CRing) | 
| 12 | 11 | crngringd 20244 | . . 3
⊢ (𝜑 → 𝑆 ∈ Ring) | 
| 13 |  | 2fveq3 6910 | . . . . . 6
⊢ (𝑥 = (1r‘𝑅) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝐴‘(1r‘𝑅)))) | 
| 14 |  | fveq2 6905 | . . . . . 6
⊢ (𝑥 = (1r‘𝑅) → (𝐹‘𝑥) = (𝐹‘(1r‘𝑅))) | 
| 15 | 13, 14 | eqeq12d 2752 | . . . . 5
⊢ (𝑥 = (1r‘𝑅) → ((𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥) ↔ (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅)))) | 
| 16 |  | evlslem1.d | . . . . . . . . 9
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 17 |  | eqid 2736 | . . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 18 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 19 |  | evlslem1.a | . . . . . . . . 9
⊢ 𝐴 = (algSc‘𝑃) | 
| 20 | 7 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐼 ∈ 𝑊) | 
| 21 | 9 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) | 
| 22 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) | 
| 23 | 6, 16, 17, 18, 19, 20, 21, 22 | mplascl 22089 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐴‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) | 
| 24 | 23 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅))))) | 
| 25 |  | evlslem1.c | . . . . . . . 8
⊢ 𝐶 = (Base‘𝑆) | 
| 26 |  | evlslem1.t | . . . . . . . 8
⊢ 𝑇 = (mulGrp‘𝑆) | 
| 27 |  | evlslem1.x | . . . . . . . 8
⊢  ↑ =
(.g‘𝑇) | 
| 28 |  | evlslem1.v | . . . . . . . 8
⊢ 𝑉 = (𝐼 mVar 𝑅) | 
| 29 |  | evlslem1.e | . . . . . . . 8
⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 30 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing) | 
| 31 | 11 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑆 ∈ CRing) | 
| 32 |  | evlslem1.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 33 | 32 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 34 |  | evlslem1.g | . . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) | 
| 35 | 34 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐺:𝐼⟶𝐶) | 
| 36 | 16 | psrbag0 22087 | . . . . . . . . . 10
⊢ (𝐼 ∈ 𝑊 → (𝐼 × {0}) ∈ 𝐷) | 
| 37 | 7, 36 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷) | 
| 38 | 37 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼 × {0}) ∈ 𝐷) | 
| 39 | 6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 20, 30, 31, 33, 35, 17, 38, 22 | evlslem3 22105 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) = ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺)))) | 
| 40 |  | 0zd 12627 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℤ) | 
| 41 |  | fvexd 6920 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ V) | 
| 42 |  | fconstmpt 5746 | . . . . . . . . . . . . . . 15
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) | 
| 43 | 42 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)) | 
| 44 | 34 | feqmptd 6976 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝐺‘𝑥))) | 
| 45 | 7, 40, 41, 43, 44 | offval2 7718 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐼 × {0}) ∘f ↑ 𝐺) = (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥)))) | 
| 46 | 34 | ffvelcdmda 7103 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ 𝐶) | 
| 47 | 26, 25 | mgpbas 20143 | . . . . . . . . . . . . . . . 16
⊢ 𝐶 = (Base‘𝑇) | 
| 48 | 26, 3 | ringidval 20181 | . . . . . . . . . . . . . . . 16
⊢
(1r‘𝑆) = (0g‘𝑇) | 
| 49 | 47, 48, 27 | mulg0 19093 | . . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑥) ∈ 𝐶 → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆)) | 
| 50 | 46, 49 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆)) | 
| 51 | 50 | mpteq2dva 5241 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) | 
| 52 | 45, 51 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐼 × {0}) ∘f ↑ 𝐺) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) | 
| 53 | 52 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆)))) | 
| 54 | 26 | crngmgp 20239 | . . . . . . . . . . . . . 14
⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd) | 
| 55 | 11, 54 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ CMnd) | 
| 56 | 55 | cmnmndd 19823 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ Mnd) | 
| 57 | 48 | gsumz 18850 | . . . . . . . . . . . 12
⊢ ((𝑇 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆)) | 
| 58 | 56, 7, 57 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆)) | 
| 59 | 53, 58 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺)) = (1r‘𝑆)) | 
| 60 | 59 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺)) = (1r‘𝑆)) | 
| 61 | 60 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺))) = ((𝐹‘𝑥) ·
(1r‘𝑆))) | 
| 62 | 18, 25 | rhmf 20486 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶) | 
| 63 | 32, 62 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶𝐶) | 
| 64 | 63 | ffvelcdmda 7103 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ 𝐶) | 
| 65 | 25, 5, 3 | ringridm 20268 | . . . . . . . . 9
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘𝑥) ∈ 𝐶) → ((𝐹‘𝑥) ·
(1r‘𝑆)) =
(𝐹‘𝑥)) | 
| 66 | 12, 64, 65 | syl2an2r 685 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) ·
(1r‘𝑆)) =
(𝐹‘𝑥)) | 
| 67 | 61, 66 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0})
∘f ↑ 𝐺))) = (𝐹‘𝑥)) | 
| 68 | 24, 39, 67 | 3eqtrd 2780 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥)) | 
| 69 | 68 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥)) | 
| 70 |  | eqid 2736 | . . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 71 | 18, 70 | ringidcl 20263 | . . . . . 6
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) | 
| 72 | 9, 71 | syl 17 | . . . . 5
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 73 | 15, 69, 72 | rspcdva 3622 | . . . 4
⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅))) | 
| 74 | 6 | mplassa 22043 | . . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg) | 
| 75 | 7, 8, 74 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ AssAlg) | 
| 76 |  | eqid 2736 | . . . . . . . . 9
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) | 
| 77 | 19, 76 | asclrhm 21911 | . . . . . . . 8
⊢ (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃)) | 
| 78 | 75, 77 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃)) | 
| 79 | 6, 7, 8 | mplsca 22034 | . . . . . . . 8
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) | 
| 80 | 79 | oveq1d 7447 | . . . . . . 7
⊢ (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃)) | 
| 81 | 78, 80 | eleqtrrd 2843 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝑅 RingHom 𝑃)) | 
| 82 | 70, 2 | rhm1 20490 | . . . . . 6
⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r‘𝑅)) = (1r‘𝑃)) | 
| 83 | 81, 82 | syl 17 | . . . . 5
⊢ (𝜑 → (𝐴‘(1r‘𝑅)) = (1r‘𝑃)) | 
| 84 | 83 | fveq2d 6909 | . . . 4
⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐸‘(1r‘𝑃))) | 
| 85 | 70, 3 | rhm1 20490 | . . . . 5
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) | 
| 86 | 32, 85 | syl 17 | . . . 4
⊢ (𝜑 → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) | 
| 87 | 73, 84, 86 | 3eqtr3d 2784 | . . 3
⊢ (𝜑 → (𝐸‘(1r‘𝑃)) = (1r‘𝑆)) | 
| 88 |  | eqid 2736 | . . . . 5
⊢
(+g‘𝑃) = (+g‘𝑃) | 
| 89 |  | eqid 2736 | . . . . 5
⊢
(+g‘𝑆) = (+g‘𝑆) | 
| 90 | 10 | ringgrpd 20240 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ Grp) | 
| 91 | 12 | ringgrpd 20240 | . . . . 5
⊢ (𝜑 → 𝑆 ∈ Grp) | 
| 92 |  | eqid 2736 | . . . . . . 7
⊢
(0g‘𝑆) = (0g‘𝑆) | 
| 93 |  | ringcmn 20280 | . . . . . . . . 9
⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd) | 
| 94 | 12, 93 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ CMnd) | 
| 95 | 94 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CMnd) | 
| 96 |  | ovex 7465 | . . . . . . . . 9
⊢
(ℕ0 ↑m 𝐼) ∈ V | 
| 97 | 16, 96 | rabex2 5340 | . . . . . . . 8
⊢ 𝐷 ∈ V | 
| 98 | 97 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐷 ∈ V) | 
| 99 | 7 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐼 ∈ 𝑊) | 
| 100 | 8 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑅 ∈ CRing) | 
| 101 | 11 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CRing) | 
| 102 | 32 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 103 | 34 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐺:𝐼⟶𝐶) | 
| 104 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ 𝐵) | 
| 105 | 6, 1, 25, 16, 26, 27, 5, 28, 29, 99, 100, 101, 102, 103, 104 | evlslem6 22106 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆))) | 
| 106 | 105 | simpld 494 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶) | 
| 107 | 105 | simprd 495 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆)) | 
| 108 | 25, 92, 95, 98, 106, 107 | gsumcl 19934 | . . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ 𝐶) | 
| 109 | 108, 29 | fmptd 7133 | . . . . 5
⊢ (𝜑 → 𝐸:𝐵⟶𝐶) | 
| 110 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 111 |  | simplrl 776 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 ∈ 𝐵) | 
| 112 |  | simplrr 777 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 ∈ 𝐵) | 
| 113 | 6, 1, 110, 88, 111, 112 | mpladd 22030 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥(+g‘𝑃)𝑦) = (𝑥 ∘f
(+g‘𝑅)𝑦)) | 
| 114 | 113 | fveq1d 6907 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥 ∘f
(+g‘𝑅)𝑦)‘𝑏)) | 
| 115 |  | simprl 770 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) | 
| 116 | 6, 18, 1, 16, 115 | mplelf 22019 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥:𝐷⟶(Base‘𝑅)) | 
| 117 | 116 | ffnd 6736 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 Fn 𝐷) | 
| 118 | 117 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 Fn 𝐷) | 
| 119 |  | simprr 772 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) | 
| 120 | 6, 18, 1, 16, 119 | mplelf 22019 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦:𝐷⟶(Base‘𝑅)) | 
| 121 | 120 | ffnd 6736 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 Fn 𝐷) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 Fn 𝐷) | 
| 123 | 97 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐷 ∈ V) | 
| 124 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷) | 
| 125 |  | fnfvof 7715 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 Fn 𝐷 ∧ 𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏 ∈ 𝐷)) → ((𝑥 ∘f
(+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) | 
| 126 | 118, 122,
123, 124, 125 | syl22anc 838 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∘f
(+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) | 
| 127 | 114, 126 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) | 
| 128 | 127 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))) | 
| 129 |  | rhmghm 20485 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | 
| 130 | 32, 129 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | 
| 131 | 130 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | 
| 132 | 116 | ffvelcdmda 7103 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥‘𝑏) ∈ (Base‘𝑅)) | 
| 133 | 120 | ffvelcdmda 7103 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑦‘𝑏) ∈ (Base‘𝑅)) | 
| 134 | 18, 110, 89 | ghmlin 19240 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥‘𝑏) ∈ (Base‘𝑅) ∧ (𝑦‘𝑏) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) | 
| 135 | 131, 132,
133, 134 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) | 
| 136 | 128, 135 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏)))) | 
| 137 | 136 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) | 
| 138 | 12 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring) | 
| 139 | 63 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹:(Base‘𝑅)⟶𝐶) | 
| 140 | 139, 132 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑥‘𝑏)) ∈ 𝐶) | 
| 141 | 139, 133 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑦‘𝑏)) ∈ 𝐶) | 
| 142 | 55 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd) | 
| 143 | 34 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶) | 
| 144 | 16, 47, 27, 142, 124, 143 | psrbagev2 22103 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶) | 
| 145 | 25, 89, 5 | ringdir 20260 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥‘𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) | 
| 146 | 138, 140,
141, 144, 145 | syl13anc 1373 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) | 
| 147 | 137, 146 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) | 
| 148 | 147 | mpteq2dva 5241 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 149 | 97 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ V) | 
| 150 |  | ovexd 7467 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ V) | 
| 151 |  | ovexd 7467 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ V) | 
| 152 |  | eqidd 2737 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) | 
| 153 |  | eqidd 2737 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) | 
| 154 | 149, 150,
151, 152, 153 | offval2 7718 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f
(+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 155 | 148, 154 | eqtr4d 2779 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f
(+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 156 | 155 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f
(+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))) | 
| 157 | 94 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CMnd) | 
| 158 | 7 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐼 ∈ 𝑊) | 
| 159 | 8 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ CRing) | 
| 160 | 11 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CRing) | 
| 161 | 32 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 162 | 34 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺:𝐼⟶𝐶) | 
| 163 | 6, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 115 | evlslem6 22106 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆))) | 
| 164 | 163 | simpld 494 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶) | 
| 165 | 6, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 119 | evlslem6 22106 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆))) | 
| 166 | 165 | simpld 494 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶) | 
| 167 | 163 | simprd 495 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆)) | 
| 168 | 165 | simprd 495 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp
(0g‘𝑆)) | 
| 169 | 25, 92, 89, 157, 149, 164, 166, 167, 168 | gsumadd 19942 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f
(+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))) | 
| 170 | 156, 169 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))) | 
| 171 | 90 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Grp) | 
| 172 | 1, 88 | grpcl 18960 | . . . . . . . 8
⊢ ((𝑃 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵) | 
| 173 | 171, 115,
119, 172 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵) | 
| 174 |  | fveq1 6904 | . . . . . . . . . . . 12
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑝‘𝑏) = ((𝑥(+g‘𝑃)𝑦)‘𝑏)) | 
| 175 | 174 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏))) | 
| 176 | 175 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) | 
| 177 | 176 | mpteq2dv 5243 | . . . . . . . . 9
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) | 
| 178 | 177 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 179 |  | ovex 7465 | . . . . . . . 8
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V | 
| 180 | 178, 29, 179 | fvmpt 7015 | . . . . . . 7
⊢ ((𝑥(+g‘𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 181 | 173, 180 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 182 |  | fveq1 6904 | . . . . . . . . . . . . 13
⊢ (𝑝 = 𝑥 → (𝑝‘𝑏) = (𝑥‘𝑏)) | 
| 183 | 182 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑝 = 𝑥 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑥‘𝑏))) | 
| 184 | 183 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑝 = 𝑥 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) | 
| 185 | 184 | mpteq2dv 5243 | . . . . . . . . . 10
⊢ (𝑝 = 𝑥 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) | 
| 186 | 185 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑝 = 𝑥 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 187 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V | 
| 188 | 186, 29, 187 | fvmpt 7015 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 189 | 115, 188 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 190 |  | fveq1 6904 | . . . . . . . . . . . . 13
⊢ (𝑝 = 𝑦 → (𝑝‘𝑏) = (𝑦‘𝑏)) | 
| 191 | 190 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑝 = 𝑦 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑦‘𝑏))) | 
| 192 | 191 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑝 = 𝑦 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) | 
| 193 | 192 | mpteq2dv 5243 | . . . . . . . . . 10
⊢ (𝑝 = 𝑦 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) | 
| 194 | 193 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑝 = 𝑦 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 195 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V | 
| 196 | 194, 29, 195 | fvmpt 7015 | . . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 197 | 196 | ad2antll 729 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 198 | 189, 197 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦)) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))) | 
| 199 | 170, 181,
198 | 3eqtr4d 2786 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦))) | 
| 200 | 1, 25, 88, 89, 90, 91, 109, 199 | isghmd 19244 | . . . 4
⊢ (𝜑 → 𝐸 ∈ (𝑃 GrpHom 𝑆)) | 
| 201 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) | 
| 202 | 201, 26 | rhmmhm 20480 | . . . . . . . . . 10
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) | 
| 203 | 32, 202 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) | 
| 204 | 203 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇)) | 
| 205 |  | simprll 778 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥 ∈ 𝐵) | 
| 206 | 6, 18, 1, 16, 205 | mplelf 22019 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥:𝐷⟶(Base‘𝑅)) | 
| 207 |  | simprrl 780 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑧 ∈ 𝐷) | 
| 208 | 206, 207 | ffvelcdmd 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑥‘𝑧) ∈ (Base‘𝑅)) | 
| 209 |  | simprlr 779 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦 ∈ 𝐵) | 
| 210 | 6, 18, 1, 16, 209 | mplelf 22019 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦:𝐷⟶(Base‘𝑅)) | 
| 211 |  | simprrr 781 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑤 ∈ 𝐷) | 
| 212 | 210, 211 | ffvelcdmd 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑦‘𝑤) ∈ (Base‘𝑅)) | 
| 213 | 201, 18 | mgpbas 20143 | . . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) | 
| 214 |  | eqid 2736 | . . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 215 | 201, 214 | mgpplusg 20142 | . . . . . . . . 9
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) | 
| 216 | 26, 5 | mgpplusg 20142 | . . . . . . . . 9
⊢  · =
(+g‘𝑇) | 
| 217 | 213, 215,
216 | mhmlin 18807 | . . . . . . . 8
⊢ ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤)))) | 
| 218 | 204, 208,
212, 217 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤)))) | 
| 219 | 56 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → 𝑇 ∈ Mnd) | 
| 220 |  | simprl 770 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 ∈ 𝐷) | 
| 221 | 16 | psrbagf 21939 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝐷 → 𝑧:𝐼⟶ℕ0) | 
| 222 | 220, 221 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧:𝐼⟶ℕ0) | 
| 223 | 222 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) ∈
ℕ0) | 
| 224 | 16 | psrbagf 21939 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ 𝐷 → 𝑤:𝐼⟶ℕ0) | 
| 225 | 224 | ad2antll 729 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤:𝐼⟶ℕ0) | 
| 226 | 225 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) ∈
ℕ0) | 
| 227 | 34 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺:𝐼⟶𝐶) | 
| 228 | 227 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ 𝐶) | 
| 229 | 47, 27, 216 | mulgnn0dir 19123 | . . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Mnd ∧ ((𝑧‘𝑣) ∈ ℕ0 ∧ (𝑤‘𝑣) ∈ ℕ0 ∧ (𝐺‘𝑣) ∈ 𝐶)) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) | 
| 230 | 219, 223,
226, 228, 229 | syl13anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) | 
| 231 | 230 | mpteq2dva 5241 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣))) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))) | 
| 232 | 7 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐼 ∈ 𝑊) | 
| 233 |  | ovexd 7467 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) + (𝑤‘𝑣)) ∈ V) | 
| 234 |  | fvexd 6920 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ V) | 
| 235 | 222 | ffnd 6736 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 Fn 𝐼) | 
| 236 | 225 | ffnd 6736 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 Fn 𝐼) | 
| 237 |  | inidm 4226 | . . . . . . . . . . . . 13
⊢ (𝐼 ∩ 𝐼) = 𝐼 | 
| 238 |  | eqidd 2737 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) = (𝑧‘𝑣)) | 
| 239 |  | eqidd 2737 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) = (𝑤‘𝑣)) | 
| 240 | 235, 236,
232, 232, 237, 238, 239 | offval 7707 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f + 𝑤) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) + (𝑤‘𝑣)))) | 
| 241 | 34 | feqmptd 6976 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣))) | 
| 242 | 241 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣))) | 
| 243 | 232, 233,
234, 240, 242 | offval2 7718 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)))) | 
| 244 |  | ovexd 7467 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) ↑ (𝐺‘𝑣)) ∈ V) | 
| 245 |  | ovexd 7467 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑤‘𝑣) ↑ (𝐺‘𝑣)) ∈ V) | 
| 246 | 34 | ffnd 6736 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 Fn 𝐼) | 
| 247 | 246 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 Fn 𝐼) | 
| 248 |  | eqidd 2737 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) = (𝐺‘𝑣)) | 
| 249 | 235, 247,
232, 232, 237, 238, 248 | offval 7707 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) ↑ (𝐺‘𝑣)))) | 
| 250 | 236, 247,
232, 232, 237, 239, 248 | offval 7707 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))) | 
| 251 | 232, 244,
245, 249, 250 | offval2 7718 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺)) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))) | 
| 252 | 231, 243,
251 | 3eqtr4d 2786 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺) = ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺))) | 
| 253 | 252 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = (𝑇 Σg ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺)))) | 
| 254 | 55 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑇 ∈ CMnd) | 
| 255 | 16, 47, 27, 48, 254, 220, 227 | psrbagev1 22102 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑧 ∘f ↑ 𝐺) finSupp (1r‘𝑆))) | 
| 256 | 255 | simpld 494 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺):𝐼⟶𝐶) | 
| 257 |  | simprr 772 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 ∈ 𝐷) | 
| 258 | 16, 47, 27, 48, 254, 257, 227 | psrbagev1 22102 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑤 ∘f ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑤 ∘f ↑ 𝐺) finSupp (1r‘𝑆))) | 
| 259 | 258 | simpld 494 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺):𝐼⟶𝐶) | 
| 260 | 255 | simprd 495 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺) finSupp (1r‘𝑆)) | 
| 261 | 258 | simprd 495 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺) finSupp (1r‘𝑆)) | 
| 262 | 47, 48, 216, 254, 232, 256, 259, 260, 261 | gsumadd 19942 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺))) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) | 
| 263 | 253, 262 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) | 
| 264 | 263 | adantrl 716 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) | 
| 265 | 218, 264 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))) | 
| 266 | 55 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑇 ∈ CMnd) | 
| 267 | 63 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹:(Base‘𝑅)⟶𝐶) | 
| 268 | 267, 208 | ffvelcdmd 7104 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑥‘𝑧)) ∈ 𝐶) | 
| 269 | 267, 212 | ffvelcdmd 7104 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) | 
| 270 | 16, 47, 27, 254, 220, 227 | psrbagev2 22103 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶) | 
| 271 | 270 | adantrl 716 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶) | 
| 272 | 16, 47, 27, 254, 257, 227 | psrbagev2 22103 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶) | 
| 273 | 272 | adantrl 716 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶) | 
| 274 | 47, 216 | cmn4 19820 | . . . . . . 7
⊢ ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥‘𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))) | 
| 275 | 266, 268,
269, 271, 273, 274 | syl122anc 1380 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))) | 
| 276 | 265, 275 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))) | 
| 277 | 7 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐼 ∈ 𝑊) | 
| 278 | 8 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ CRing) | 
| 279 | 11 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑆 ∈ CRing) | 
| 280 | 32 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 281 | 34 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐺:𝐼⟶𝐶) | 
| 282 | 16 | psrbagaddcl 21945 | . . . . . . 7
⊢ ((𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → (𝑧 ∘f + 𝑤) ∈ 𝐷) | 
| 283 | 282 | ad2antll 729 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑧 ∘f + 𝑤) ∈ 𝐷) | 
| 284 | 9 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ Ring) | 
| 285 | 18, 214 | ringcl 20248 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅)) | 
| 286 | 284, 208,
212, 285 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅)) | 
| 287 | 6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 283, 286 | evlslem3 22105 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘f + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)))) | 
| 288 | 6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 207, 208 | evlslem3 22105 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) = ((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺)))) | 
| 289 | 6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 211, 212 | evlslem3 22105 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))) = ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) | 
| 290 | 288, 289 | oveq12d 7450 | . . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅))))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))) | 
| 291 | 276, 287,
290 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘f + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))))) | 
| 292 | 6, 1, 5, 17, 16, 7, 8, 11, 200, 291 | evlslem2 22104 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(.r‘𝑃)𝑦)) = ((𝐸‘𝑥) · (𝐸‘𝑦))) | 
| 293 | 1, 2, 3, 4, 5, 10,
12, 87, 292, 25, 88, 89, 109, 199 | isrhmd 20489 | . 2
⊢ (𝜑 → 𝐸 ∈ (𝑃 RingHom 𝑆)) | 
| 294 |  | ovex 7465 | . . . . . 6
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V | 
| 295 | 294, 29 | fnmpti 6710 | . . . . 5
⊢ 𝐸 Fn 𝐵 | 
| 296 | 295 | a1i 11 | . . . 4
⊢ (𝜑 → 𝐸 Fn 𝐵) | 
| 297 | 18, 1 | rhmf 20486 | . . . . . 6
⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:(Base‘𝑅)⟶𝐵) | 
| 298 | 81, 297 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐴:(Base‘𝑅)⟶𝐵) | 
| 299 | 298 | ffnd 6736 | . . . 4
⊢ (𝜑 → 𝐴 Fn (Base‘𝑅)) | 
| 300 | 298 | frnd 6743 | . . . 4
⊢ (𝜑 → ran 𝐴 ⊆ 𝐵) | 
| 301 |  | fnco 6685 | . . . 4
⊢ ((𝐸 Fn 𝐵 ∧ 𝐴 Fn (Base‘𝑅) ∧ ran 𝐴 ⊆ 𝐵) → (𝐸 ∘ 𝐴) Fn (Base‘𝑅)) | 
| 302 | 296, 299,
300, 301 | syl3anc 1372 | . . 3
⊢ (𝜑 → (𝐸 ∘ 𝐴) Fn (Base‘𝑅)) | 
| 303 | 63 | ffnd 6736 | . . 3
⊢ (𝜑 → 𝐹 Fn (Base‘𝑅)) | 
| 304 |  | fvco2 7005 | . . . . 5
⊢ ((𝐴 Fn (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥))) | 
| 305 | 299, 304 | sylan 580 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥))) | 
| 306 | 305, 68 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐹‘𝑥)) | 
| 307 | 302, 303,
306 | eqfnfvd 7053 | . 2
⊢ (𝜑 → (𝐸 ∘ 𝐴) = 𝐹) | 
| 308 | 6, 28, 1, 7, 9 | mvrf2 22014 | . . . . 5
⊢ (𝜑 → 𝑉:𝐼⟶𝐵) | 
| 309 | 308 | ffnd 6736 | . . . 4
⊢ (𝜑 → 𝑉 Fn 𝐼) | 
| 310 | 308 | frnd 6743 | . . . 4
⊢ (𝜑 → ran 𝑉 ⊆ 𝐵) | 
| 311 |  | fnco 6685 | . . . 4
⊢ ((𝐸 Fn 𝐵 ∧ 𝑉 Fn 𝐼 ∧ ran 𝑉 ⊆ 𝐵) → (𝐸 ∘ 𝑉) Fn 𝐼) | 
| 312 | 296, 309,
310, 311 | syl3anc 1372 | . . 3
⊢ (𝜑 → (𝐸 ∘ 𝑉) Fn 𝐼) | 
| 313 |  | fvco2 7005 | . . . . 5
⊢ ((𝑉 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥))) | 
| 314 | 309, 313 | sylan 580 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥))) | 
| 315 | 7 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊) | 
| 316 | 8 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing) | 
| 317 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) | 
| 318 | 28, 16, 17, 70, 315, 316, 317 | mvrval 22003 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) | 
| 319 | 318 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅))))) | 
| 320 | 11 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing) | 
| 321 | 32 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 322 | 34 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺:𝐼⟶𝐶) | 
| 323 | 16 | psrbagsn 22088 | . . . . . . . 8
⊢ (𝐼 ∈ 𝑊 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) | 
| 324 | 7, 323 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) | 
| 325 | 324 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷) | 
| 326 | 72 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 327 | 6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 315, 316, 320, 321, 322, 17, 325, 326 | evlslem3 22105 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) = ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)))) | 
| 328 | 86 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) | 
| 329 |  | 1nn0 12544 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 | 
| 330 |  | 0nn0 12543 | . . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 | 
| 331 | 329, 330 | ifcli 4572 | . . . . . . . . . . . . 13
⊢ if(𝑧 = 𝑥, 1, 0) ∈
ℕ0 | 
| 332 | 331 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, 1, 0) ∈
ℕ0) | 
| 333 | 34 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶) | 
| 334 |  | eqidd 2737 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0))) | 
| 335 | 34 | feqmptd 6976 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐼 ↦ (𝐺‘𝑧))) | 
| 336 | 7, 332, 333, 334, 335 | offval2 7718 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)))) | 
| 337 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (1 =
if(𝑧 = 𝑥, 1, 0) → (1 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) | 
| 338 | 337 | eqeq1d 2738 | . . . . . . . . . . . . 13
⊢ (1 =
if(𝑧 = 𝑥, 1, 0) → ((1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) | 
| 339 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (0 =
if(𝑧 = 𝑥, 1, 0) → (0 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) | 
| 340 | 339 | eqeq1d 2738 | . . . . . . . . . . . . 13
⊢ (0 =
if(𝑧 = 𝑥, 1, 0) → ((0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) | 
| 341 | 333 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (𝐺‘𝑧) ∈ 𝐶) | 
| 342 | 47, 27 | mulg1 19100 | . . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑧) ∈ 𝐶 → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧)) | 
| 343 | 341, 342 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧)) | 
| 344 |  | iftrue 4530 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧)) | 
| 345 | 344 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧)) | 
| 346 | 343, 345 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) | 
| 347 | 47, 48, 27 | mulg0 19093 | . . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑧) ∈ 𝐶 → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) | 
| 348 | 333, 347 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) | 
| 349 | 348 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆)) | 
| 350 |  | iffalse 4533 | . . . . . . . . . . . . . . 15
⊢ (¬
𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) | 
| 351 | 350 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) | 
| 352 | 349, 351 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) | 
| 353 | 338, 340,
346, 352 | ifbothda 4563 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) | 
| 354 | 353 | mpteq2dva 5241 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) | 
| 355 | 336, 354 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) | 
| 356 | 355 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) | 
| 357 | 356 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)) = (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))) | 
| 358 | 56 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ Mnd) | 
| 359 | 333 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶) | 
| 360 | 25, 3 | ringidcl 20263 | . . . . . . . . . . . . 13
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ 𝐶) | 
| 361 | 12, 360 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (1r‘𝑆) ∈ 𝐶) | 
| 362 | 361 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (1r‘𝑆) ∈ 𝐶) | 
| 363 | 359, 362 | ifcld 4571 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ∈ 𝐶) | 
| 364 | 363 | fmpttd 7134 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))):𝐼⟶𝐶) | 
| 365 |  | eldifsnneq 4790 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥) | 
| 366 | 365, 350 | syl 17 | . . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) | 
| 367 | 366 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆)) | 
| 368 | 367, 315 | suppss2 8226 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) supp (1r‘𝑆)) ⊆ {𝑥}) | 
| 369 | 47, 48, 358, 315, 317, 364, 368 | gsumpt 19981 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) = ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥)) | 
| 370 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥)) | 
| 371 | 344, 370 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑥)) | 
| 372 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) | 
| 373 |  | fvex 6918 | . . . . . . . . . 10
⊢ (𝐺‘𝑥) ∈ V | 
| 374 | 371, 372,
373 | fvmpt 7015 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥)) | 
| 375 | 374 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥)) | 
| 376 | 357, 369,
375 | 3eqtrd 2780 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)) = (𝐺‘𝑥)) | 
| 377 | 328, 376 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))) =
((1r‘𝑆)
·
(𝐺‘𝑥))) | 
| 378 | 25, 5, 3 | ringlidm 20267 | . . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐶) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥)) | 
| 379 | 12, 46, 378 | syl2an2r 685 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥)) | 
| 380 | 377, 379 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))) = (𝐺‘𝑥)) | 
| 381 | 319, 327,
380 | 3eqtrd 2780 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐺‘𝑥)) | 
| 382 | 314, 381 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐺‘𝑥)) | 
| 383 | 312, 246,
382 | eqfnfvd 7053 | . 2
⊢ (𝜑 → (𝐸 ∘ 𝑉) = 𝐺) | 
| 384 | 293, 307,
383 | 3jca 1128 | 1
⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺)) |