Database
BASIC LINEAR ALGEBRA
Abstract multivariate polynomials
Definition and basic properties
mplsubglem2
Next ⟩
mplsubg
Metamath Proof Explorer
Ascii
Unicode
Theorem
mplsubglem2
Description:
Lemma for
mplsubg
and
mpllss
.
(Contributed by
AV
, 16-Jul-2019)
Ref
Expression
Hypotheses
mplsubg.s
⊢
S
=
I
mPwSer
R
mplsubg.p
⊢
P
=
I
mPoly
R
mplsubg.u
⊢
U
=
Base
P
mplsubg.i
⊢
φ
→
I
∈
W
Assertion
mplsubglem2
⊢
φ
→
U
=
g
∈
Base
S
|
g
supp
0
R
∈
Fin
Proof
Step
Hyp
Ref
Expression
1
mplsubg.s
⊢
S
=
I
mPwSer
R
2
mplsubg.p
⊢
P
=
I
mPoly
R
3
mplsubg.u
⊢
U
=
Base
P
4
mplsubg.i
⊢
φ
→
I
∈
W
5
eqid
⊢
Base
S
=
Base
S
6
eqid
⊢
0
R
=
0
R
7
2
1
5
6
3
mplbas
⊢
U
=
g
∈
Base
S
|
finSupp
0
R
⁡
g
8
1
5
psrelbasfun
⊢
g
∈
Base
S
→
Fun
⁡
g
9
8
adantl
⊢
φ
∧
g
∈
Base
S
→
Fun
⁡
g
10
simpr
⊢
φ
∧
g
∈
Base
S
→
g
∈
Base
S
11
fvexd
⊢
φ
∧
g
∈
Base
S
→
0
R
∈
V
12
funisfsupp
⊢
Fun
⁡
g
∧
g
∈
Base
S
∧
0
R
∈
V
→
finSupp
0
R
⁡
g
↔
g
supp
0
R
∈
Fin
13
9
10
11
12
syl3anc
⊢
φ
∧
g
∈
Base
S
→
finSupp
0
R
⁡
g
↔
g
supp
0
R
∈
Fin
14
13
rabbidva
⊢
φ
→
g
∈
Base
S
|
finSupp
0
R
⁡
g
=
g
∈
Base
S
|
g
supp
0
R
∈
Fin
15
7
14
syl5eq
⊢
φ
→
U
=
g
∈
Base
S
|
g
supp
0
R
∈
Fin