Metamath Proof Explorer

Theorem bj-finsumval0

Description: Value of a finite sum. (Contributed by BJ, 9-Jun-2019) (Proof shortened by AV, 5-May-2021)

Ref Expression
Hypotheses bj-finsumval0.1 
|- ( ph -> A e. CMnd )
bj-finsumval0.2 
|- ( ph -> I e. Fin )
bj-finsumval0.3 
|- ( ph -> B : I --> ( Base ` A ) )
Assertion bj-finsumval0 
|- ( ph -> ( A FinSum B ) = ( iota s E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) )

Proof

Step Hyp Ref Expression
1 bj-finsumval0.1 
 |-  ( ph -> A e. CMnd )
2 bj-finsumval0.2 
 |-  ( ph -> I e. Fin )
3 bj-finsumval0.3 
 |-  ( ph -> B : I --> ( Base ` A ) )
4 df-ov 
 |-  ( A FinSum B ) = ( FinSum ` <. A , B >. )
5 df-bj-finsum 
 |-  FinSum = ( x e. { <. y , z >. | ( y e. CMnd /\ E. t e. Fin z : t --> ( Base ` y ) ) } |-> ( iota s E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) ) )
6 simpr 
 |-  ( ( ph /\ x = <. A , B >. ) -> x = <. A , B >. )
7 6 fveq2d 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( 1st ` x ) = ( 1st ` <. A , B >. ) )
8 1 adantr 
 |-  ( ( ph /\ x = <. A , B >. ) -> A e. CMnd )
9 3 2 fexd 
 |-  ( ph -> B e. _V )
10 9 adantr 
 |-  ( ( ph /\ x = <. A , B >. ) -> B e. _V )
11 op1stg 
 |-  ( ( A e. CMnd /\ B e. _V ) -> ( 1st ` <. A , B >. ) = A )
12 8 10 11 syl2anc 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( 1st ` <. A , B >. ) = A )
13 7 12 eqtrd 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( 1st ` x ) = A )
14 6 fveq2d 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( 2nd ` x ) = ( 2nd ` <. A , B >. ) )
15 op2ndg 
 |-  ( ( A e. CMnd /\ B e. _V ) -> ( 2nd ` <. A , B >. ) = B )
16 8 10 15 syl2anc 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( 2nd ` <. A , B >. ) = B )
17 14 16 eqtrd 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( 2nd ` x ) = B )
18 17 dmeqd 
 |-  ( ( ph /\ x = <. A , B >. ) -> dom ( 2nd ` x ) = dom B )
19 3 fdmd 
 |-  ( ph -> dom B = I )
20 19 adantr 
 |-  ( ( ph /\ x = <. A , B >. ) -> dom B = I )
21 18 20 eqtrd 
 |-  ( ( ph /\ x = <. A , B >. ) -> dom ( 2nd ` x ) = I )
22 f1oeq3 
 |-  ( dom ( 2nd ` x ) = I -> ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) <-> f : ( 1 ... m ) -1-1-onto-> I ) )
23 22 biimpd 
 |-  ( dom ( 2nd ` x ) = I -> ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) -> f : ( 1 ... m ) -1-1-onto-> I ) )
24 23 ad2antll 
 |-  ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) -> ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) -> f : ( 1 ... m ) -1-1-onto-> I ) )
25 24 adantrd 
 |-  ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) -> ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) -> f : ( 1 ... m ) -1-1-onto-> I ) )
26 25 adantr 
 |-  ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) -> f : ( 1 ... m ) -1-1-onto-> I ) )
27 eqidd 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> 1 = 1 )
28 simprl 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) ) -> ( 1st ` x ) = A )
29 28 fveq2d 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) ) -> ( +g ` ( 1st ` x ) ) = ( +g ` A ) )
30 29 adantrr 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( +g ` ( 1st ` x ) ) = ( +g ` A ) )
31 simprrl 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) ) -> ( 2nd ` x ) = B )
32 31 adantr 
 |-  ( ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) ) /\ n e. NN ) -> ( 2nd ` x ) = B )
33 32 fveq1d 
 |-  ( ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) ) /\ n e. NN ) -> ( ( 2nd ` x ) ` ( f ` n ) ) = ( B ` ( f ` n ) ) )
34 33 mpteq2dva 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) ) -> ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) = ( n e. NN |-> ( B ` ( f ` n ) ) ) )
35 34 adantrr 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) = ( n e. NN |-> ( B ` ( f ` n ) ) ) )
36 27 30 35 seqeq123d 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) = seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) )
37 simprr 
 |-  ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) -> dom ( 2nd ` x ) = I )
38 37 anim1ci 
 |-  ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> ( m e. NN0 /\ dom ( 2nd ` x ) = I ) )
39 hashfz1 
 |-  ( m e. NN0 -> ( # ` ( 1 ... m ) ) = m )
40 39 eqcomd 
 |-  ( m e. NN0 -> m = ( # ` ( 1 ... m ) ) )
41 40 ad2antrl 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( m e. NN0 /\ dom ( 2nd ` x ) = I ) ) -> m = ( # ` ( 1 ... m ) ) )
42 fzfid 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( m e. NN0 /\ dom ( 2nd ` x ) = I ) ) -> ( 1 ... m ) e. Fin )
43 19.8a 
 |-  ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) -> E. f f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) )
44 43 adantr 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( m e. NN0 /\ dom ( 2nd ` x ) = I ) ) -> E. f f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) )
45 hasheqf1oi 
 |-  ( ( 1 ... m ) e. Fin -> ( E. f f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) -> ( # ` ( 1 ... m ) ) = ( # ` dom ( 2nd ` x ) ) ) )
46 42 44 45 sylc 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( m e. NN0 /\ dom ( 2nd ` x ) = I ) ) -> ( # ` ( 1 ... m ) ) = ( # ` dom ( 2nd ` x ) ) )
47 simprr 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( m e. NN0 /\ dom ( 2nd ` x ) = I ) ) -> dom ( 2nd ` x ) = I )
48 47 fveq2d 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( m e. NN0 /\ dom ( 2nd ` x ) = I ) ) -> ( # ` dom ( 2nd ` x ) ) = ( # ` I ) )
49 41 46 48 3eqtrd 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( m e. NN0 /\ dom ( 2nd ` x ) = I ) ) -> m = ( # ` I ) )
50 38 49 sylan2 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> m = ( # ` I ) )
51 36 50 fveq12d 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) )
52 51 eqeq2d 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) <-> s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) )
53 52 biimpd 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) -> s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) )
54 53 impancom 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) -> ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) )
55 54 com12 
 |-  ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) -> s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) )
56 26 55 jcad 
 |-  ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) -> ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) )
57 22 biimprd 
 |-  ( dom ( 2nd ` x ) = I -> ( f : ( 1 ... m ) -1-1-onto-> I -> f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) ) )
58 57 ad2antll 
 |-  ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) -> ( f : ( 1 ... m ) -1-1-onto-> I -> f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) ) )
59 58 adantr 
 |-  ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> ( f : ( 1 ... m ) -1-1-onto-> I -> f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) ) )
60 59 adantrd 
 |-  ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> ( ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) -> f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) ) )
61 eqidd 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> 1 = 1 )
62 simpl 
 |-  ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) -> ( 1st ` x ) = A )
63 tru 
 |-  T.
64 62 63 jctir 
 |-  ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) -> ( ( 1st ` x ) = A /\ T. ) )
65 64 ad2antrl 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( ( 1st ` x ) = A /\ T. ) )
66 simpl 
 |-  ( ( ( 1st ` x ) = A /\ T. ) -> ( 1st ` x ) = A )
67 66 eqcomd 
 |-  ( ( ( 1st ` x ) = A /\ T. ) -> A = ( 1st ` x ) )
68 65 67 syl 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> A = ( 1st ` x ) )
69 68 fveq2d 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( +g ` A ) = ( +g ` ( 1st ` x ) ) )
70 simpl 
 |-  ( ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) -> ( 2nd ` x ) = B )
71 70 eqcomd 
 |-  ( ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) -> B = ( 2nd ` x ) )
72 71 ad2antll 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) ) -> B = ( 2nd ` x ) )
73 72 adantr 
 |-  ( ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) ) /\ n e. NN ) -> B = ( 2nd ` x ) )
74 73 fveq1d 
 |-  ( ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) ) /\ n e. NN ) -> ( B ` ( f ` n ) ) = ( ( 2nd ` x ) ` ( f ` n ) ) )
75 74 adantlrr 
 |-  ( ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) /\ n e. NN ) -> ( B ` ( f ` n ) ) = ( ( 2nd ` x ) ` ( f ` n ) ) )
76 75 mpteq2dva 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( n e. NN |-> ( B ` ( f ` n ) ) ) = ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) )
77 61 69 76 seqeq123d 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) = seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) )
78 59 impcom 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) )
79 simprr 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> m e. NN0 )
80 37 ad2antrl 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> dom ( 2nd ` x ) = I )
81 78 79 80 49 syl12anc 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> m = ( # ` I ) )
82 81 eqcomd 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( # ` I ) = m )
83 77 82 fveq12d 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) )
84 83 eqeq2d 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) <-> s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) )
85 84 biimpd 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) ) -> ( s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) -> s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) )
86 85 impancom 
 |-  ( ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) -> ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) )
87 86 com12 
 |-  ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> ( ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) -> s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) )
88 60 87 jcad 
 |-  ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> ( ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) -> ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) ) )
89 56 88 impbid 
 |-  ( ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) /\ m e. NN0 ) -> ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) )
90 89 ex 
 |-  ( ( ( 1st ` x ) = A /\ ( ( 2nd ` x ) = B /\ dom ( 2nd ` x ) = I ) ) -> ( m e. NN0 -> ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) ) )
91 13 17 21 90 syl12anc 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( m e. NN0 -> ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) ) )
92 91 imp 
 |-  ( ( ( ph /\ x = <. A , B >. ) /\ m e. NN0 ) -> ( ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) )
93 92 exbidv 
 |-  ( ( ( ph /\ x = <. A , B >. ) /\ m e. NN0 ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) )
94 93 rexbidva 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) <-> E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) )
95 94 iotabidv 
 |-  ( ( ph /\ x = <. A , B >. ) -> ( iota s E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> dom ( 2nd ` x ) /\ s = ( seq 1 ( ( +g ` ( 1st ` x ) ) , ( n e. NN |-> ( ( 2nd ` x ) ` ( f ` n ) ) ) ) ` m ) ) ) = ( iota s E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) )
96 eleq1 
 |-  ( t = I -> ( t e. Fin <-> I e. Fin ) )
97 feq2 
 |-  ( t = I -> ( B : t --> ( Base ` A ) <-> B : I --> ( Base ` A ) ) )
98 96 97 anbi12d 
 |-  ( t = I -> ( ( t e. Fin /\ B : t --> ( Base ` A ) ) <-> ( I e. Fin /\ B : I --> ( Base ` A ) ) ) )
99 98 ceqsexgv 
 |-  ( I e. Fin -> ( E. t ( t = I /\ ( t e. Fin /\ B : t --> ( Base ` A ) ) ) <-> ( I e. Fin /\ B : I --> ( Base ` A ) ) ) )
100 2 99 syl 
 |-  ( ph -> ( E. t ( t = I /\ ( t e. Fin /\ B : t --> ( Base ` A ) ) ) <-> ( I e. Fin /\ B : I --> ( Base ` A ) ) ) )
101 2 3 100 mpbir2and 
 |-  ( ph -> E. t ( t = I /\ ( t e. Fin /\ B : t --> ( Base ` A ) ) ) )
102 exsimpr 
 |-  ( E. t ( t = I /\ ( t e. Fin /\ B : t --> ( Base ` A ) ) ) -> E. t ( t e. Fin /\ B : t --> ( Base ` A ) ) )
103 101 102 syl 
 |-  ( ph -> E. t ( t e. Fin /\ B : t --> ( Base ` A ) ) )
104 df-rex 
 |-  ( E. t e. Fin B : t --> ( Base ` A ) <-> E. t ( t e. Fin /\ B : t --> ( Base ` A ) ) )
105 103 104 sylibr 
 |-  ( ph -> E. t e. Fin B : t --> ( Base ` A ) )
106 eleq1 
 |-  ( y = A -> ( y e. CMnd <-> A e. CMnd ) )
107 fveq2 
 |-  ( y = A -> ( Base ` y ) = ( Base ` A ) )
108 107 feq3d 
 |-  ( y = A -> ( z : t --> ( Base ` y ) <-> z : t --> ( Base ` A ) ) )
109 108 rexbidv 
 |-  ( y = A -> ( E. t e. Fin z : t --> ( Base ` y ) <-> E. t e. Fin z : t --> ( Base ` A ) ) )
110 106 109 anbi12d 
 |-  ( y = A -> ( ( y e. CMnd /\ E. t e. Fin z : t --> ( Base ` y ) ) <-> ( A e. CMnd /\ E. t e. Fin z : t --> ( Base ` A ) ) ) )
111 feq1 
 |-  ( z = B -> ( z : t --> ( Base ` A ) <-> B : t --> ( Base ` A ) ) )
112 111 rexbidv 
 |-  ( z = B -> ( E. t e. Fin z : t --> ( Base ` A ) <-> E. t e. Fin B : t --> ( Base ` A ) ) )
113 112 anbi2d 
 |-  ( z = B -> ( ( A e. CMnd /\ E. t e. Fin z : t --> ( Base ` A ) ) <-> ( A e. CMnd /\ E. t e. Fin B : t --> ( Base ` A ) ) ) )
114 110 113 opelopabg 
 |-  ( ( A e. CMnd /\ B e. _V ) -> ( <. A , B >. e. { <. y , z >. | ( y e. CMnd /\ E. t e. Fin z : t --> ( Base ` y ) ) } <-> ( A e. CMnd /\ E. t e. Fin B : t --> ( Base ` A ) ) ) )
115 1 9 114 syl2anc 
 |-  ( ph -> ( <. A , B >. e. { <. y , z >. | ( y e. CMnd /\ E. t e. Fin z : t --> ( Base ` y ) ) } <-> ( A e. CMnd /\ E. t e. Fin B : t --> ( Base ` A ) ) ) )
116 1 105 115 mpbir2and 
 |-  ( ph -> <. A , B >. e. { <. y , z >. | ( y e. CMnd /\ E. t e. Fin z : t --> ( Base ` y ) ) } )
117 iotaex 
 |-  ( iota s E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) e. _V
118 117 a1i 
 |-  ( ph -> ( iota s E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) e. _V )
119 5 95 116 118 fvmptd2 
 |-  ( ph -> ( FinSum ` <. A , B >. ) = ( iota s E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) )
120 4 119 eqtrid 
 |-  ( ph -> ( A FinSum B ) = ( iota s E. m e. NN0 E. f ( f : ( 1 ... m ) -1-1-onto-> I /\ s = ( seq 1 ( ( +g ` A ) , ( n e. NN |-> ( B ` ( f ` n ) ) ) ) ` ( # ` I ) ) ) ) )