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)

	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		simpl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ℎ ∈ 𝐴 ) → 𝐼 ∈ 𝑉 )
8		nn0subm	⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
9	8	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ℎ ∈ 𝐴 ) → ℕ0 ∈ ( SubMnd ‘ ℂfld ) )
10	1	psrbagf	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ℎ ∈ 𝐴 ) → ℎ : 𝐼 ⟶ ℕ0 )
11	1	psrbagfsupp	⊢ ( ( ℎ ∈ 𝐴 ∧ 𝐼 ∈ 𝑉 ) → ℎ finSupp 0 )
12	11	ancoms	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ℎ ∈ 𝐴 ) → ℎ finSupp 0 )
13	3 6 7 9 10 12	gsumsubmcl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ℎ ∈ 𝐴 ) → ( ℂfld Σg ℎ ) ∈ ℕ0 )
14	13 2	fmptd	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 : 𝐴 ⟶ ℕ0 )