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)

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 
|- ( ( I e. V /\ 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 
 |-  ( ( I e. V /\ X e. A /\ Y e. A ) -> CCfld e. CMnd )
9 simp1 
 |-  ( ( I e. V /\ X e. A /\ Y e. A ) -> I e. V )
10 1 psrbagf 
 |-  ( ( I e. V /\ 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 
 |-  ( ( I e. V /\ X e. A ) -> X : I --> CC )
14 13 3adant3 
 |-  ( ( I e. V /\ X e. A /\ Y e. A ) -> X : I --> CC )
15 1 psrbagf 
 |-  ( ( I e. V /\ Y e. A ) -> Y : I --> NN0 )
16 fss 
 |-  ( ( Y : I --> NN0 /\ NN0 C_ CC ) -> Y : I --> CC )
17 15 11 16 sylancl 
 |-  ( ( I e. V /\ Y e. A ) -> Y : I --> CC )
18 17 3adant2 
 |-  ( ( I e. V /\ X e. A /\ Y e. A ) -> Y : I --> CC )
19 1 psrbagfsupp 
 |-  ( ( X e. A /\ I e. V ) -> X finSupp 0 )
20 19 ancoms 
 |-  ( ( I e. V /\ X e. A ) -> X finSupp 0 )
21 20 3adant3 
 |-  ( ( I e. V /\ X e. A /\ Y e. A ) -> X finSupp 0 )
22 1 psrbagfsupp 
 |-  ( ( Y e. A /\ I e. V ) -> Y finSupp 0 )
23 22 ancoms 
 |-  ( ( I e. V /\ Y e. A ) -> Y finSupp 0 )
24 23 3adant2 
 |-  ( ( I e. V /\ X e. A /\ Y e. A ) -> Y finSupp 0 )
25 3 4 5 8 9 14 18 21 24 gsumadd 
 |-  ( ( I e. V /\ X e. A /\ Y e. A ) -> ( CCfld gsum ( X oF + Y ) ) = ( ( CCfld gsum X ) + ( CCfld gsum Y ) ) )
26 1 psrbagaddcl 
 |-  ( ( I e. V /\ 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 
 |-  ( ( I e. V /\ 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 37 3adant1 
 |-  ( ( I e. V /\ X e. A /\ Y e. A ) -> ( ( H ` X ) + ( H ` Y ) ) = ( ( CCfld gsum X ) + ( CCfld gsum Y ) ) )
39 25 30 38 3eqtr4d 
 |-  ( ( I e. V /\ X e. A /\ Y e. A ) -> ( H ` ( X oF + Y ) ) = ( ( H ` X ) + ( H ` Y ) ) )