Step |
Hyp |
Ref |
Expression |
1 |
|
zprod.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
zprod.2 |
|- ( ph -> M e. ZZ ) |
3 |
|
zprod.3 |
|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) ) |
4 |
|
zprod.4 |
|- ( ph -> A C_ Z ) |
5 |
|
zprod.5 |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 1 ) ) |
6 |
|
zprod.6 |
|- ( ( ph /\ k e. A ) -> B e. CC ) |
7 |
|
3simpb |
|- ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
8 |
|
nfcv |
|- F/_ i if ( k e. A , B , 1 ) |
9 |
|
nfv |
|- F/ k i e. A |
10 |
|
nfcsb1v |
|- F/_ k [_ i / k ]_ B |
11 |
|
nfcv |
|- F/_ k 1 |
12 |
9 10 11
|
nfif |
|- F/_ k if ( i e. A , [_ i / k ]_ B , 1 ) |
13 |
|
eleq1w |
|- ( k = i -> ( k e. A <-> i e. A ) ) |
14 |
|
csbeq1a |
|- ( k = i -> B = [_ i / k ]_ B ) |
15 |
13 14
|
ifbieq1d |
|- ( k = i -> if ( k e. A , B , 1 ) = if ( i e. A , [_ i / k ]_ B , 1 ) ) |
16 |
8 12 15
|
cbvmpt |
|- ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( i e. ZZ |-> if ( i e. A , [_ i / k ]_ B , 1 ) ) |
17 |
|
simpll |
|- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> ph ) |
18 |
6
|
ralrimiva |
|- ( ph -> A. k e. A B e. CC ) |
19 |
10
|
nfel1 |
|- F/ k [_ i / k ]_ B e. CC |
20 |
14
|
eleq1d |
|- ( k = i -> ( B e. CC <-> [_ i / k ]_ B e. CC ) ) |
21 |
19 20
|
rspc |
|- ( i e. A -> ( A. k e. A B e. CC -> [_ i / k ]_ B e. CC ) ) |
22 |
18 21
|
syl5 |
|- ( i e. A -> ( ph -> [_ i / k ]_ B e. CC ) ) |
23 |
17 22
|
mpan9 |
|- ( ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) /\ i e. A ) -> [_ i / k ]_ B e. CC ) |
24 |
|
simplr |
|- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> m e. ZZ ) |
25 |
2
|
ad2antrr |
|- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> M e. ZZ ) |
26 |
|
simpr |
|- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> A C_ ( ZZ>= ` m ) ) |
27 |
4 1
|
sseqtrdi |
|- ( ph -> A C_ ( ZZ>= ` M ) ) |
28 |
27
|
ad2antrr |
|- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> A C_ ( ZZ>= ` M ) ) |
29 |
16 23 24 25 26 28
|
prodrb |
|- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> ( seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x <-> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
30 |
29
|
biimpd |
|- ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> ( seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
31 |
30
|
expimpd |
|- ( ( ph /\ m e. ZZ ) -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
32 |
7 31
|
syl5 |
|- ( ( ph /\ m e. ZZ ) -> ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
33 |
32
|
rexlimdva |
|- ( ph -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
34 |
|
uzssz |
|- ( ZZ>= ` M ) C_ ZZ |
35 |
|
zssre |
|- ZZ C_ RR |
36 |
34 35
|
sstri |
|- ( ZZ>= ` M ) C_ RR |
37 |
1 36
|
eqsstri |
|- Z C_ RR |
38 |
4 37
|
sstrdi |
|- ( ph -> A C_ RR ) |
39 |
38
|
ad2antrr |
|- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A C_ RR ) |
40 |
|
ltso |
|- < Or RR |
41 |
|
soss |
|- ( A C_ RR -> ( < Or RR -> < Or A ) ) |
42 |
39 40 41
|
mpisyl |
|- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> < Or A ) |
43 |
|
fzfi |
|- ( 1 ... m ) e. Fin |
44 |
|
ovex |
|- ( 1 ... m ) e. _V |
45 |
44
|
f1oen |
|- ( f : ( 1 ... m ) -1-1-onto-> A -> ( 1 ... m ) ~~ A ) |
46 |
45
|
adantl |
|- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( 1 ... m ) ~~ A ) |
47 |
46
|
ensymd |
|- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A ~~ ( 1 ... m ) ) |
48 |
|
enfii |
|- ( ( ( 1 ... m ) e. Fin /\ A ~~ ( 1 ... m ) ) -> A e. Fin ) |
49 |
43 47 48
|
sylancr |
|- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A e. Fin ) |
50 |
|
fz1iso |
|- ( ( < Or A /\ A e. Fin ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) |
51 |
42 49 50
|
syl2anc |
|- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) |
52 |
|
simpll |
|- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> ph ) |
53 |
52 22
|
mpan9 |
|- ( ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) /\ i e. A ) -> [_ i / k ]_ B e. CC ) |
54 |
|
fveq2 |
|- ( n = j -> ( f ` n ) = ( f ` j ) ) |
55 |
54
|
csbeq1d |
|- ( n = j -> [_ ( f ` n ) / k ]_ B = [_ ( f ` j ) / k ]_ B ) |
56 |
|
csbcow |
|- [_ ( f ` j ) / i ]_ [_ i / k ]_ B = [_ ( f ` j ) / k ]_ B |
57 |
55 56
|
eqtr4di |
|- ( n = j -> [_ ( f ` n ) / k ]_ B = [_ ( f ` j ) / i ]_ [_ i / k ]_ B ) |
58 |
57
|
cbvmptv |
|- ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( j e. NN |-> [_ ( f ` j ) / i ]_ [_ i / k ]_ B ) |
59 |
|
eqid |
|- ( j e. NN |-> [_ ( g ` j ) / i ]_ [_ i / k ]_ B ) = ( j e. NN |-> [_ ( g ` j ) / i ]_ [_ i / k ]_ B ) |
60 |
|
simplr |
|- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> m e. NN ) |
61 |
2
|
ad2antrr |
|- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> M e. ZZ ) |
62 |
27
|
ad2antrr |
|- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> A C_ ( ZZ>= ` M ) ) |
63 |
|
simprl |
|- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> f : ( 1 ... m ) -1-1-onto-> A ) |
64 |
|
simprr |
|- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) |
65 |
16 53 58 59 60 61 62 63 64
|
prodmolem2a |
|- ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) |
66 |
65
|
expr |
|- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) |
67 |
66
|
exlimdv |
|- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) |
68 |
51 67
|
mpd |
|- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) |
69 |
|
breq2 |
|- ( x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) -> ( seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x <-> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) |
70 |
68 69
|
syl5ibrcom |
|- ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
71 |
70
|
expimpd |
|- ( ( ph /\ m e. NN ) -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
72 |
71
|
exlimdv |
|- ( ( ph /\ m e. NN ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
73 |
72
|
rexlimdva |
|- ( ph -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
74 |
33 73
|
jaod |
|- ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
75 |
2
|
adantr |
|- ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> M e. ZZ ) |
76 |
4
|
adantr |
|- ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> A C_ Z ) |
77 |
1
|
eleq2i |
|- ( n e. Z <-> n e. ( ZZ>= ` M ) ) |
78 |
|
eluzelz |
|- ( n e. ( ZZ>= ` M ) -> n e. ZZ ) |
79 |
78
|
adantl |
|- ( ( ph /\ n e. ( ZZ>= ` M ) ) -> n e. ZZ ) |
80 |
|
uztrn |
|- ( ( z e. ( ZZ>= ` n ) /\ n e. ( ZZ>= ` M ) ) -> z e. ( ZZ>= ` M ) ) |
81 |
80
|
ancoms |
|- ( ( n e. ( ZZ>= ` M ) /\ z e. ( ZZ>= ` n ) ) -> z e. ( ZZ>= ` M ) ) |
82 |
1
|
eleq2i |
|- ( k e. Z <-> k e. ( ZZ>= ` M ) ) |
83 |
1 34
|
eqsstri |
|- Z C_ ZZ |
84 |
83
|
sseli |
|- ( k e. Z -> k e. ZZ ) |
85 |
|
iftrue |
|- ( k e. A -> if ( k e. A , B , 1 ) = B ) |
86 |
85
|
adantl |
|- ( ( ph /\ k e. A ) -> if ( k e. A , B , 1 ) = B ) |
87 |
86 6
|
eqeltrd |
|- ( ( ph /\ k e. A ) -> if ( k e. A , B , 1 ) e. CC ) |
88 |
87
|
ex |
|- ( ph -> ( k e. A -> if ( k e. A , B , 1 ) e. CC ) ) |
89 |
|
iffalse |
|- ( -. k e. A -> if ( k e. A , B , 1 ) = 1 ) |
90 |
|
ax-1cn |
|- 1 e. CC |
91 |
89 90
|
eqeltrdi |
|- ( -. k e. A -> if ( k e. A , B , 1 ) e. CC ) |
92 |
88 91
|
pm2.61d1 |
|- ( ph -> if ( k e. A , B , 1 ) e. CC ) |
93 |
|
eqid |
|- ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( k e. ZZ |-> if ( k e. A , B , 1 ) ) |
94 |
93
|
fvmpt2 |
|- ( ( k e. ZZ /\ if ( k e. A , B , 1 ) e. CC ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = if ( k e. A , B , 1 ) ) |
95 |
84 92 94
|
syl2anr |
|- ( ( ph /\ k e. Z ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = if ( k e. A , B , 1 ) ) |
96 |
5 95
|
eqtr4d |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) ) |
97 |
82 96
|
sylan2br |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) ) |
98 |
97
|
ralrimiva |
|- ( ph -> A. k e. ( ZZ>= ` M ) ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) ) |
99 |
|
nffvmpt1 |
|- F/_ k ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) |
100 |
99
|
nfeq2 |
|- F/ k ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) |
101 |
|
fveq2 |
|- ( k = z -> ( F ` k ) = ( F ` z ) ) |
102 |
|
fveq2 |
|- ( k = z -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) ) |
103 |
101 102
|
eqeq12d |
|- ( k = z -> ( ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) <-> ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) ) ) |
104 |
100 103
|
rspc |
|- ( z e. ( ZZ>= ` M ) -> ( A. k e. ( ZZ>= ` M ) ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) -> ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) ) ) |
105 |
98 104
|
mpan9 |
|- ( ( ph /\ z e. ( ZZ>= ` M ) ) -> ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) ) |
106 |
81 105
|
sylan2 |
|- ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ z e. ( ZZ>= ` n ) ) ) -> ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) ) |
107 |
106
|
anassrs |
|- ( ( ( ph /\ n e. ( ZZ>= ` M ) ) /\ z e. ( ZZ>= ` n ) ) -> ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) ) |
108 |
79 107
|
seqfeq |
|- ( ( ph /\ n e. ( ZZ>= ` M ) ) -> seq n ( x. , F ) = seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ) |
109 |
108
|
breq1d |
|- ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( seq n ( x. , F ) ~~> y <-> seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) |
110 |
109
|
anbi2d |
|- ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) <-> ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) ) |
111 |
110
|
exbidv |
|- ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) <-> E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) ) |
112 |
77 111
|
sylan2b |
|- ( ( ph /\ n e. Z ) -> ( E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) <-> E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) ) |
113 |
112
|
rexbidva |
|- ( ph -> ( E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) <-> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) ) |
114 |
3 113
|
mpbid |
|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) |
115 |
114
|
adantr |
|- ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) |
116 |
|
simpr |
|- ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) |
117 |
|
fveq2 |
|- ( m = M -> ( ZZ>= ` m ) = ( ZZ>= ` M ) ) |
118 |
117 1
|
eqtr4di |
|- ( m = M -> ( ZZ>= ` m ) = Z ) |
119 |
118
|
sseq2d |
|- ( m = M -> ( A C_ ( ZZ>= ` m ) <-> A C_ Z ) ) |
120 |
118
|
rexeqdv |
|- ( m = M -> ( E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) <-> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) ) |
121 |
|
seqeq1 |
|- ( m = M -> seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) = seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ) |
122 |
121
|
breq1d |
|- ( m = M -> ( seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x <-> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
123 |
119 120 122
|
3anbi123d |
|- ( m = M -> ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) <-> ( A C_ Z /\ E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) ) |
124 |
123
|
rspcev |
|- ( ( M e. ZZ /\ ( A C_ Z /\ E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) -> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
125 |
75 76 115 116 124
|
syl13anc |
|- ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
126 |
125
|
orcd |
|- ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) |
127 |
126
|
ex |
|- ( ph -> ( seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) ) |
128 |
74 127
|
impbid |
|- ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) |
129 |
95 5
|
eqtr4d |
|- ( ( ph /\ k e. Z ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( F ` k ) ) |
130 |
82 129
|
sylan2br |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( F ` k ) ) |
131 |
130
|
ralrimiva |
|- ( ph -> A. k e. ( ZZ>= ` M ) ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( F ` k ) ) |
132 |
99
|
nfeq1 |
|- F/ k ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) = ( F ` z ) |
133 |
102 101
|
eqeq12d |
|- ( k = z -> ( ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( F ` k ) <-> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) = ( F ` z ) ) ) |
134 |
132 133
|
rspc |
|- ( z e. ( ZZ>= ` M ) -> ( A. k e. ( ZZ>= ` M ) ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( F ` k ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) = ( F ` z ) ) ) |
135 |
131 134
|
mpan9 |
|- ( ( ph /\ z e. ( ZZ>= ` M ) ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) = ( F ` z ) ) |
136 |
2 135
|
seqfeq |
|- ( ph -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) = seq M ( x. , F ) ) |
137 |
136
|
breq1d |
|- ( ph -> ( seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x <-> seq M ( x. , F ) ~~> x ) ) |
138 |
128 137
|
bitrd |
|- ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> seq M ( x. , F ) ~~> x ) ) |
139 |
138
|
iotabidv |
|- ( ph -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) = ( iota x seq M ( x. , F ) ~~> x ) ) |
140 |
|
df-prod |
|- prod_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) |
141 |
|
df-fv |
|- ( ~~> ` seq M ( x. , F ) ) = ( iota x seq M ( x. , F ) ~~> x ) |
142 |
139 140 141
|
3eqtr4g |
|- ( ph -> prod_ k e. A B = ( ~~> ` seq M ( x. , F ) ) ) |