Database
BASIC LINEAR ALGEBRA
Abstract multivariate polynomials
Definition and basic properties
rhmpsrlem1
Next ⟩
rhmpsrlem2
Metamath Proof Explorer
Ascii
Unicode
Theorem
rhmpsrlem1
Description:
Lemma for
rhmpsr
et al.
(Contributed by
SN
, 8-Feb-2025)
Ref
Expression
Hypotheses
rhmpsrlem1.d
⊢
D
=
f
∈
ℕ
0
I
|
f
-1
ℕ
∈
Fin
rhmpsrlem1.r
⊢
φ
→
R
∈
Ring
rhmpsrlem1.x
⊢
φ
→
X
:
D
⟶
Base
R
rhmpsrlem1.y
⊢
φ
→
Y
:
D
⟶
Base
R
Assertion
rhmpsrlem1
⊢
φ
∧
k
∈
D
→
finSupp
0
R
⁡
x
∈
y
∈
D
|
y
≤
f
k
⟼
X
⁡
x
⋅
R
Y
⁡
k
−
f
x
Proof
Step
Hyp
Ref
Expression
1
rhmpsrlem1.d
⊢
D
=
f
∈
ℕ
0
I
|
f
-1
ℕ
∈
Fin
2
rhmpsrlem1.r
⊢
φ
→
R
∈
Ring
3
rhmpsrlem1.x
⊢
φ
→
X
:
D
⟶
Base
R
4
rhmpsrlem1.y
⊢
φ
→
Y
:
D
⟶
Base
R
5
ovexd
⊢
φ
∧
k
∈
D
∧
x
∈
y
∈
D
|
y
≤
f
k
→
X
⁡
x
⋅
R
Y
⁡
k
−
f
x
∈
V
6
5
fmpttd
⊢
φ
∧
k
∈
D
→
x
∈
y
∈
D
|
y
≤
f
k
⟼
X
⁡
x
⋅
R
Y
⁡
k
−
f
x
:
y
∈
D
|
y
≤
f
k
⟶
V
7
1
psrbaglefi
⊢
k
∈
D
→
y
∈
D
|
y
≤
f
k
∈
Fin
8
7
adantl
⊢
φ
∧
k
∈
D
→
y
∈
D
|
y
≤
f
k
∈
Fin
9
fvexd
⊢
φ
∧
k
∈
D
→
0
R
∈
V
10
6
8
9
fdmfifsupp
⊢
φ
∧
k
∈
D
→
finSupp
0
R
⁡
x
∈
y
∈
D
|
y
≤
f
k
⟼
X
⁡
x
⋅
R
Y
⁡
k
−
f
x