Description: A homogeneous polynomial defines a homogeneous function; this is mhphf with simpler notation in the conclusion in exchange for a complex definition of .xb , which is based on frlmvscafval but without the finite support restriction ( frlmpws , frlmbas ) on the assignments A from variables to values.
TODO?: Polynomials ( df-mpl ) are defined to have a finite amount of terms (of finite degree). As such, any assignment may be replaced by an assignment with finite support (as only a finite amount of variables matter in a given polynomial, even if the set of variables is infinite). So the finite support restriction can be assumed without loss of generality. (Contributed by SN, 11-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mhphf2.q | ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) | |
| mhphf2.h | ⊢ 𝐻 = ( 𝐼 mHomP 𝑈 ) | ||
| mhphf2.u | ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 ) | ||
| mhphf2.k | ⊢ 𝐾 = ( Base ‘ 𝑆 ) | ||
| mhphf2.b | ⊢ ∙ = ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) | ||
| mhphf2.m | ⊢ · = ( .r ‘ 𝑆 ) | ||
| mhphf2.e | ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) ) | ||
| mhphf2.s | ⊢ ( 𝜑 → 𝑆 ∈ CRing ) | ||
| mhphf2.r | ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) | ||
| mhphf2.l | ⊢ ( 𝜑 → 𝐿 ∈ 𝑅 ) | ||
| mhphf2.x | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ) | ||
| mhphf2.a | ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) ) | ||
| Assertion | mhphf2 | ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( 𝐿 ∙ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mhphf2.q | ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) | |
| 2 | mhphf2.h | ⊢ 𝐻 = ( 𝐼 mHomP 𝑈 ) | |
| 3 | mhphf2.u | ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 ) | |
| 4 | mhphf2.k | ⊢ 𝐾 = ( Base ‘ 𝑆 ) | |
| 5 | mhphf2.b | ⊢ ∙ = ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) | |
| 6 | mhphf2.m | ⊢ · = ( .r ‘ 𝑆 ) | |
| 7 | mhphf2.e | ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) ) | |
| 8 | mhphf2.s | ⊢ ( 𝜑 → 𝑆 ∈ CRing ) | |
| 9 | mhphf2.r | ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) | |
| 10 | mhphf2.l | ⊢ ( 𝜑 → 𝐿 ∈ 𝑅 ) | |
| 11 | mhphf2.x | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ) | |
| 12 | mhphf2.a | ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) ) | |
| 13 | eqid | ⊢ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) | |
| 14 | eqid | ⊢ ( Base ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) = ( Base ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) | |
| 15 | rlmvsca | ⊢ ( .r ‘ 𝑆 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑆 ) ) | |
| 16 | eqid | ⊢ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) | |
| 17 | eqid | ⊢ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) | |
| 18 | fvexd | ⊢ ( 𝜑 → ( ringLMod ‘ 𝑆 ) ∈ V ) | |
| 19 | reldmmhp | ⊢ Rel dom mHomP | |
| 20 | 19 2 11 | elfvov1 | ⊢ ( 𝜑 → 𝐼 ∈ V ) |
| 21 | 4 | subrgss | ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 ) |
| 22 | 9 21 | syl | ⊢ ( 𝜑 → 𝑅 ⊆ 𝐾 ) |
| 23 | 22 10 | sseldd | ⊢ ( 𝜑 → 𝐿 ∈ 𝐾 ) |
| 24 | rlmsca | ⊢ ( 𝑆 ∈ CRing → 𝑆 = ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) | |
| 25 | 8 24 | syl | ⊢ ( 𝜑 → 𝑆 = ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) |
| 26 | 25 | fveq2d | ⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) ) |
| 27 | 4 26 | eqtrid | ⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) ) |
| 28 | 23 27 | eleqtrd | ⊢ ( 𝜑 → 𝐿 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑆 ) ) ) ) |
| 29 | 4 | oveq1i | ⊢ ( 𝐾 ↑m 𝐼 ) = ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) |
| 30 | 12 29 | eleqtrdi | ⊢ ( 𝜑 → 𝐴 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) |
| 31 | rlmbas | ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( ringLMod ‘ 𝑆 ) ) | |
| 32 | 13 31 | pwsbas | ⊢ ( ( ( ringLMod ‘ 𝑆 ) ∈ V ∧ 𝐼 ∈ V ) → ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) = ( Base ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) ) |
| 33 | 18 20 32 | syl2anc | ⊢ ( 𝜑 → ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) = ( Base ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) ) |
| 34 | 30 33 | eleqtrd | ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑆 ) ↑s 𝐼 ) ) ) |
| 35 | 13 14 15 5 16 17 18 20 28 34 | pwsvscafval | ⊢ ( 𝜑 → ( 𝐿 ∙ 𝐴 ) = ( ( 𝐼 × { 𝐿 } ) ∘f ( .r ‘ 𝑆 ) 𝐴 ) ) |
| 36 | 6 | eqcomi | ⊢ ( .r ‘ 𝑆 ) = · |
| 37 | ofeq | ⊢ ( ( .r ‘ 𝑆 ) = · → ∘f ( .r ‘ 𝑆 ) = ∘f · ) | |
| 38 | 36 37 | mp1i | ⊢ ( 𝜑 → ∘f ( .r ‘ 𝑆 ) = ∘f · ) |
| 39 | 38 | oveqd | ⊢ ( 𝜑 → ( ( 𝐼 × { 𝐿 } ) ∘f ( .r ‘ 𝑆 ) 𝐴 ) = ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) |
| 40 | 35 39 | eqtrd | ⊢ ( 𝜑 → ( 𝐿 ∙ 𝐴 ) = ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) |
| 41 | 40 | fveq2d | ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( 𝐿 ∙ 𝐴 ) ) = ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) ) |
| 42 | 1 2 3 4 6 7 8 9 10 11 12 | mhphf | ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) ) |
| 43 | 41 42 | eqtrd | ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( 𝐿 ∙ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) ) |