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
|- A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
tdeglem.h
|- H = ( h e. A |-> ( CCfld gsum h ) )
Assertion tdeglem3
|- ( ( X e. A /\ Y e. A ) -> ( H ` ( X oF + Y ) ) = ( ( H ` X ) + ( H ` Y ) ) )

Proof

Step Hyp Ref Expression
1 tdeglem.a
 |-  A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
2 tdeglem.h
 |-  H = ( h e. A |-> ( CCfld gsum h ) )
3 cnfldbas
 |-  CC = ( Base ` CCfld )
4 cnfld0
 |-  0 = ( 0g ` CCfld )
5 cnfldadd
 |-  + = ( +g ` CCfld )
6 cnring
 |-  CCfld e. Ring
7 ringcmn
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
8 6 7 mp1i
 |-  ( ( X e. A /\ Y e. A ) -> CCfld e. CMnd )
9 simpl
 |-  ( ( X e. A /\ Y e. A ) -> X e. A )
10 1 psrbagf
 |-  ( X e. A -> X : I --> NN0 )
11 nn0sscn
 |-  NN0 C_ CC
12 fss
 |-  ( ( X : I --> NN0 /\ NN0 C_ CC ) -> X : I --> CC )
13 10 11 12 sylancl
 |-  ( X e. A -> X : I --> CC )
14 13 adantr
 |-  ( ( X e. A /\ Y e. A ) -> X : I --> CC )
15 14 ffnd
 |-  ( ( X e. A /\ Y e. A ) -> X Fn I )
16 9 15 fndmexd
 |-  ( ( X e. A /\ Y e. A ) -> I e. _V )
17 1 psrbagf
 |-  ( Y e. A -> Y : I --> NN0 )
18 fss
 |-  ( ( Y : I --> NN0 /\ NN0 C_ CC ) -> Y : I --> CC )
19 17 11 18 sylancl
 |-  ( Y e. A -> Y : I --> CC )
20 19 adantl
 |-  ( ( X e. A /\ Y e. A ) -> Y : I --> CC )
21 1 psrbagfsupp
 |-  ( X e. A -> X finSupp 0 )
22 21 adantr
 |-  ( ( X e. A /\ Y e. A ) -> X finSupp 0 )
23 1 psrbagfsupp
 |-  ( Y e. A -> Y finSupp 0 )
24 23 adantl
 |-  ( ( X e. A /\ Y e. A ) -> Y finSupp 0 )
25 3 4 5 8 16 14 20 22 24 gsumadd
 |-  ( ( X e. A /\ Y e. A ) -> ( CCfld gsum ( X oF + Y ) ) = ( ( CCfld gsum X ) + ( CCfld gsum Y ) ) )
26 1 psrbagaddcl
 |-  ( ( X e. A /\ Y e. A ) -> ( X oF + Y ) e. A )
27 oveq2
 |-  ( h = ( X oF + Y ) -> ( CCfld gsum h ) = ( CCfld gsum ( X oF + Y ) ) )
28 ovex
 |-  ( CCfld gsum ( X oF + Y ) ) e. _V
29 27 2 28 fvmpt
 |-  ( ( X oF + Y ) e. A -> ( H ` ( X oF + Y ) ) = ( CCfld gsum ( X oF + Y ) ) )
30 26 29 syl
 |-  ( ( X e. A /\ Y e. A ) -> ( H ` ( X oF + Y ) ) = ( CCfld gsum ( X oF + Y ) ) )
31 oveq2
 |-  ( h = X -> ( CCfld gsum h ) = ( CCfld gsum X ) )
32 ovex
 |-  ( CCfld gsum X ) e. _V
33 31 2 32 fvmpt
 |-  ( X e. A -> ( H ` X ) = ( CCfld gsum X ) )
34 oveq2
 |-  ( h = Y -> ( CCfld gsum h ) = ( CCfld gsum Y ) )
35 ovex
 |-  ( CCfld gsum Y ) e. _V
36 34 2 35 fvmpt
 |-  ( Y e. A -> ( H ` Y ) = ( CCfld gsum Y ) )
37 33 36 oveqan12d
 |-  ( ( X e. A /\ Y e. A ) -> ( ( H ` X ) + ( H ` Y ) ) = ( ( CCfld gsum X ) + ( CCfld gsum Y ) ) )
38 25 30 37 3eqtr4d
 |-  ( ( X e. A /\ Y e. A ) -> ( H ` ( X oF + Y ) ) = ( ( H ` X ) + ( H ` Y ) ) )