This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tdeglem3

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

Ref Expression
Hypotheses tdeglem.a ⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
tdeglem.h ⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
Assertion tdeglem3 ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑋 ∘f + 𝑌 ) ) = ( ( 𝐻 ‘ 𝑋 ) + ( 𝐻 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 tdeglem.a ⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
2 tdeglem.h ⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
3 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
4 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
5 cnfldadd ⊢ + = ( +g ‘ ℂfld )
6 cnring ⊢ ℂfld ∈ Ring
7 ringcmn ⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
8 6 7 mp1i ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ℂfld ∈ CMnd )
9 simpl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
10 1 psrbagf ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 : 𝐼 ⟶ ℕ0 )
11 nn0sscn ⊢ ℕ0 ⊆ ℂ
12 fss ⊢ ( ( 𝑋 : 𝐼 ⟶ ℕ0 ∧ ℕ0 ⊆ ℂ ) → 𝑋 : 𝐼 ⟶ ℂ )
13 10 11 12 sylancl ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 : 𝐼 ⟶ ℂ )
14 13 adantr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 : 𝐼 ⟶ ℂ )
15 14 ffnd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 Fn 𝐼 )
16 9 15 fndmexd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝐼 ∈ V )
17 1 psrbagf ⊢ ( 𝑌 ∈ 𝐴 → 𝑌 : 𝐼 ⟶ ℕ0 )
18 fss ⊢ ( ( 𝑌 : 𝐼 ⟶ ℕ0 ∧ ℕ0 ⊆ ℂ ) → 𝑌 : 𝐼 ⟶ ℂ )
19 17 11 18 sylancl ⊢ ( 𝑌 ∈ 𝐴 → 𝑌 : 𝐼 ⟶ ℂ )
20 19 adantl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 : 𝐼 ⟶ ℂ )
21 1 psrbagfsupp ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 finSupp 0 )
22 21 adantr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 finSupp 0 )
23 1 psrbagfsupp ⊢ ( 𝑌 ∈ 𝐴 → 𝑌 finSupp 0 )
24 23 adantl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 finSupp 0 )
25 3 4 5 8 16 14 20 22 24 gsumadd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ℂfld Σg ( 𝑋 ∘f + 𝑌 ) ) = ( ( ℂfld Σg 𝑋 ) + ( ℂfld Σg 𝑌 ) ) )
26 1 psrbagaddcl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ∘f + 𝑌 ) ∈ 𝐴 )
27 oveq2 ⊢ ( ℎ = ( 𝑋 ∘f + 𝑌 ) → ( ℂfld Σg ℎ ) = ( ℂfld Σg ( 𝑋 ∘f + 𝑌 ) ) )
28 ovex ⊢ ( ℂfld Σg ( 𝑋 ∘f + 𝑌 ) ) ∈ V
29 27 2 28 fvmpt ⊢ ( ( 𝑋 ∘f + 𝑌 ) ∈ 𝐴 → ( 𝐻 ‘ ( 𝑋 ∘f + 𝑌 ) ) = ( ℂfld Σg ( 𝑋 ∘f + 𝑌 ) ) )
30 26 29 syl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑋 ∘f + 𝑌 ) ) = ( ℂfld Σg ( 𝑋 ∘f + 𝑌 ) ) )
31 oveq2 ⊢ ( ℎ = 𝑋 → ( ℂfld Σg ℎ ) = ( ℂfld Σg 𝑋 ) )
32 ovex ⊢ ( ℂfld Σg 𝑋 ) ∈ V
33 31 2 32 fvmpt ⊢ ( 𝑋 ∈ 𝐴 → ( 𝐻 ‘ 𝑋 ) = ( ℂfld Σg 𝑋 ) )
34 oveq2 ⊢ ( ℎ = 𝑌 → ( ℂfld Σg ℎ ) = ( ℂfld Σg 𝑌 ) )
35 ovex ⊢ ( ℂfld Σg 𝑌 ) ∈ V
36 34 2 35 fvmpt ⊢ ( 𝑌 ∈ 𝐴 → ( 𝐻 ‘ 𝑌 ) = ( ℂfld Σg 𝑌 ) )
37 33 36 oveqan12d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑋 ) + ( 𝐻 ‘ 𝑌 ) ) = ( ( ℂfld Σg 𝑋 ) + ( ℂfld Σg 𝑌 ) ) )
38 25 30 37 3eqtr4d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑋 ∘f + 𝑌 ) ) = ( ( 𝐻 ‘ 𝑋 ) + ( 𝐻 ‘ 𝑌 ) ) )