Step |
Hyp |
Ref |
Expression |
1 |
|
mplsubg.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
2 |
|
mplsubg.p |
⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) |
3 |
|
mplsubg.u |
⊢ 𝑈 = ( Base ‘ 𝑃 ) |
4 |
|
mplsubg.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
5 |
|
mpllss.r |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
7 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
8 |
|
eqid |
⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
9 |
|
0fin |
⊢ ∅ ∈ Fin |
10 |
9
|
a1i |
⊢ ( 𝜑 → ∅ ∈ Fin ) |
11 |
|
unfi |
⊢ ( ( 𝑥 ∈ Fin ∧ 𝑦 ∈ Fin ) → ( 𝑥 ∪ 𝑦 ) ∈ Fin ) |
12 |
11
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ 𝑦 ∈ Fin ) ) → ( 𝑥 ∪ 𝑦 ) ∈ Fin ) |
13 |
|
ssfi |
⊢ ( ( 𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ∈ Fin ) |
14 |
13
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ∈ Fin ) |
15 |
1 2 3 4
|
mplsubglem2 |
⊢ ( 𝜑 → 𝑈 = { 𝑔 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝑔 supp ( 0g ‘ 𝑅 ) ) ∈ Fin } ) |
16 |
1 6 7 8 4 10 12 14 15 5
|
mpllsslem |
⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑆 ) ) |