This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mhphf3

Description: A homogeneous polynomial defines a homogeneous function; this is mhphf2 with the finite support restriction ( frlmpws , frlmbas ) on the assignments A from variables to values. See comment of mhphf2 . (Contributed by SN, 23-Nov-2024)

Ref Expression
Hypotheses mhphf3.q ⊢ Q = I evalSub S ⁡ R
mhphf3.h ⊢ H = I mHomP U
mhphf3.u ⊢ U = S ↾ 𝑠 R
mhphf3.k ⊢ K = Base S
mhphf3.f ⊢ F = S freeLMod I
mhphf3.m ⊢ M = Base F
mhphf3.b ⊢ ∙ ˙ = ⋅ F
mhphf3.x ⊢ · ˙ = ⋅ S
mhphf3.e ⊢ × ˙ = ⋅ mulGrp S
mhphf3.s ⊢ φ → S ∈ CRing
mhphf3.r ⊢ φ → R ∈ SubRing ⁡ S
mhphf3.l ⊢ φ → L ∈ R
mhphf3.p ⊢ φ → X ∈ H ⁡ N
mhphf3.a ⊢ φ → A ∈ M
Assertion mhphf3 ⊢ φ → Q ⁡ X ⁡ L ∙ ˙ A = N × ˙ L · ˙ Q ⁡ X ⁡ A

Proof

Step Hyp Ref Expression
1 mhphf3.q ⊢ Q = I evalSub S ⁡ R
2 mhphf3.h ⊢ H = I mHomP U
3 mhphf3.u ⊢ U = S ↾ 𝑠 R
4 mhphf3.k ⊢ K = Base S
5 mhphf3.f ⊢ F = S freeLMod I
6 mhphf3.m ⊢ M = Base F
7 mhphf3.b ⊢ ∙ ˙ = ⋅ F
8 mhphf3.x ⊢ · ˙ = ⋅ S
9 mhphf3.e ⊢ × ˙ = ⋅ mulGrp S
10 mhphf3.s ⊢ φ → S ∈ CRing
11 mhphf3.r ⊢ φ → R ∈ SubRing ⁡ S
12 mhphf3.l ⊢ φ → L ∈ R
13 mhphf3.p ⊢ φ → X ∈ H ⁡ N
14 mhphf3.a ⊢ φ → A ∈ M
15 reldmmhp ⊢ Rel ⁡ dom ⁡ mHomP
16 15 2 13 elfvov1 ⊢ φ → I ∈ V
17 4 subrgss ⊢ R ∈ SubRing ⁡ S → R ⊆ K
18 11 17 syl ⊢ φ → R ⊆ K
19 18 12 sseldd ⊢ φ → L ∈ K
20 5 6 4 16 19 14 7 8 frlmvscafval ⊢ φ → L ∙ ˙ A = I × L · ˙ f A
21 20 fveq2d ⊢ φ → Q ⁡ X ⁡ L ∙ ˙ A = Q ⁡ X ⁡ I × L · ˙ f A
22 5 4 6 frlmbasmap ⊢ I ∈ V ∧ A ∈ M → A ∈ K I
23 16 14 22 syl2anc ⊢ φ → A ∈ K I
24 1 2 3 4 8 9 10 11 12 13 23 mhphf ⊢ φ → Q ⁡ X ⁡ I × L · ˙ f A = N × ˙ L · ˙ Q ⁡ X ⁡ A
25 21 24 eqtrd ⊢ φ → Q ⁡ X ⁡ L ∙ ˙ A = N × ˙ L · ˙ Q ⁡ X ⁡ A