Theorem tdeglem1

Description: Functionality of the total degree helper function. (Contributed by Stefan O'Rear, 19-Mar-2015) (Proof shortened by AV, 27-Jul-2019) Remove sethood antecedent. (Revised by SN, 7-Aug-2024)

	Ref	Expression
Hypotheses	tdeglem.a	⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
	tdeglem.h	⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
Assertion	tdeglem1	⊢ 𝐻 : 𝐴 ⟶ ℕ0

Proof

Step	Hyp	Ref	Expression
1		tdeglem.a	⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
2		tdeglem.h	⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
3		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
4		cnring	⊢ ℂfld ∈ Ring
5		ringcmn	⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
6	4 5	mp1i	⊢ ( ℎ ∈ 𝐴 → ℂfld ∈ CMnd )
7		id	⊢ ( ℎ ∈ 𝐴 → ℎ ∈ 𝐴 )
8	1	psrbagf	⊢ ( ℎ ∈ 𝐴 → ℎ : 𝐼 ⟶ ℕ0 )
9	8	ffnd	⊢ ( ℎ ∈ 𝐴 → ℎ Fn 𝐼 )
10	7 9	fndmexd	⊢ ( ℎ ∈ 𝐴 → 𝐼 ∈ V )
11		nn0subm	⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
12	11	a1i	⊢ ( ℎ ∈ 𝐴 → ℕ0 ∈ ( SubMnd ‘ ℂfld ) )
13	1	psrbagfsupp	⊢ ( ℎ ∈ 𝐴 → ℎ finSupp 0 )
14	3 6 10 12 8 13	gsumsubmcl	⊢ ( ℎ ∈ 𝐴 → ( ℂfld Σg ℎ ) ∈ ℕ0 )
15	2 14	fmpti	⊢ 𝐻 : 𝐴 ⟶ ℕ0