Metamath Proof Explorer


Theorem tdeglem3OLD

Description: Obsolete version of tdeglem3 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 26-Mar-2015) (Proof shortened by AV, 27-Jul-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses tdeglem.a 𝐴 = { 𝑚 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑚 “ ℕ ) ∈ Fin }
tdeglem.h 𝐻 = ( 𝐴 ↦ ( ℂfld Σg ) )
Assertion tdeglem3OLD ( ( 𝐼𝑉𝑋𝐴𝑌𝐴 ) → ( 𝐻 ‘ ( 𝑋f + 𝑌 ) ) = ( ( 𝐻𝑋 ) + ( 𝐻𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 tdeglem.a 𝐴 = { 𝑚 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑚 “ ℕ ) ∈ 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 simp1 ( ( 𝐼𝑉𝑋𝐴𝑌𝐴 ) → 𝐼𝑉 )
10 1 psrbagfOLD ( ( 𝐼𝑉𝑋𝐴 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
11 nn0sscn 0 ⊆ ℂ
12 fss ( ( 𝑋 : 𝐼 ⟶ ℕ0 ∧ ℕ0 ⊆ ℂ ) → 𝑋 : 𝐼 ⟶ ℂ )
13 10 11 12 sylancl ( ( 𝐼𝑉𝑋𝐴 ) → 𝑋 : 𝐼 ⟶ ℂ )
14 13 3adant3 ( ( 𝐼𝑉𝑋𝐴𝑌𝐴 ) → 𝑋 : 𝐼 ⟶ ℂ )
15 1 psrbagfOLD ( ( 𝐼𝑉𝑌𝐴 ) → 𝑌 : 𝐼 ⟶ ℕ0 )
16 fss ( ( 𝑌 : 𝐼 ⟶ ℕ0 ∧ ℕ0 ⊆ ℂ ) → 𝑌 : 𝐼 ⟶ ℂ )
17 15 11 16 sylancl ( ( 𝐼𝑉𝑌𝐴 ) → 𝑌 : 𝐼 ⟶ ℂ )
18 17 3adant2 ( ( 𝐼𝑉𝑋𝐴𝑌𝐴 ) → 𝑌 : 𝐼 ⟶ ℂ )
19 1 psrbagfsuppOLD ( ( 𝑋𝐴𝐼𝑉 ) → 𝑋 finSupp 0 )
20 19 ancoms ( ( 𝐼𝑉𝑋𝐴 ) → 𝑋 finSupp 0 )
21 20 3adant3 ( ( 𝐼𝑉𝑋𝐴𝑌𝐴 ) → 𝑋 finSupp 0 )
22 1 psrbagfsuppOLD ( ( 𝑌𝐴𝐼𝑉 ) → 𝑌 finSupp 0 )
23 22 ancoms ( ( 𝐼𝑉𝑌𝐴 ) → 𝑌 finSupp 0 )
24 23 3adant2 ( ( 𝐼𝑉𝑋𝐴𝑌𝐴 ) → 𝑌 finSupp 0 )
25 3 4 5 8 9 14 18 21 24 gsumadd ( ( 𝐼𝑉𝑋𝐴𝑌𝐴 ) → ( ℂfld Σg ( 𝑋f + 𝑌 ) ) = ( ( ℂfld Σg 𝑋 ) + ( ℂfld Σg 𝑌 ) ) )
26 1 psrbagaddclOLD ( ( 𝐼𝑉𝑋𝐴𝑌𝐴 ) → ( 𝑋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 37 3adant1 ( ( 𝐼𝑉𝑋𝐴𝑌𝐴 ) → ( ( 𝐻𝑋 ) + ( 𝐻𝑌 ) ) = ( ( ℂfld Σg 𝑋 ) + ( ℂfld Σg 𝑌 ) ) )
39 25 30 38 3eqtr4d ( ( 𝐼𝑉𝑋𝐴𝑌𝐴 ) → ( 𝐻 ‘ ( 𝑋f + 𝑌 ) ) = ( ( 𝐻𝑋 ) + ( 𝐻𝑌 ) ) )