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 
|- 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 ) ) )