Step |
Hyp |
Ref |
Expression |
1 |
|
reprval.a |
|- ( ph -> A C_ NN ) |
2 |
|
reprval.m |
|- ( ph -> M e. ZZ ) |
3 |
|
reprval.s |
|- ( ph -> S e. NN0 ) |
4 |
|
reprlt.1 |
|- ( ph -> M < S ) |
5 |
1 2 3
|
reprval |
|- ( ph -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } ) |
6 |
2
|
zred |
|- ( ph -> M e. RR ) |
7 |
6
|
adantr |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> M e. RR ) |
8 |
3
|
nn0red |
|- ( ph -> S e. RR ) |
9 |
8
|
adantr |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> S e. RR ) |
10 |
|
fzofi |
|- ( 0 ..^ S ) e. Fin |
11 |
10
|
a1i |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> ( 0 ..^ S ) e. Fin ) |
12 |
|
nnssre |
|- NN C_ RR |
13 |
12
|
a1i |
|- ( ph -> NN C_ RR ) |
14 |
1 13
|
sstrd |
|- ( ph -> A C_ RR ) |
15 |
14
|
ad2antrr |
|- ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> A C_ RR ) |
16 |
|
nnex |
|- NN e. _V |
17 |
16
|
a1i |
|- ( ph -> NN e. _V ) |
18 |
17 1
|
ssexd |
|- ( ph -> A e. _V ) |
19 |
18
|
adantr |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> A e. _V ) |
20 |
10
|
elexi |
|- ( 0 ..^ S ) e. _V |
21 |
20
|
a1i |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> ( 0 ..^ S ) e. _V ) |
22 |
|
simpr |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> c e. ( A ^m ( 0 ..^ S ) ) ) |
23 |
|
elmapg |
|- ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) -> ( c e. ( A ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> A ) ) |
24 |
23
|
biimpa |
|- ( ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> c : ( 0 ..^ S ) --> A ) |
25 |
19 21 22 24
|
syl21anc |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> c : ( 0 ..^ S ) --> A ) |
26 |
25
|
adantr |
|- ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> c : ( 0 ..^ S ) --> A ) |
27 |
|
simpr |
|- ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) ) |
28 |
26 27
|
ffvelrnd |
|- ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. A ) |
29 |
15 28
|
sseldd |
|- ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. RR ) |
30 |
11 29
|
fsumrecl |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) e. RR ) |
31 |
4
|
adantr |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> M < S ) |
32 |
|
ax-1cn |
|- 1 e. CC |
33 |
|
fsumconst |
|- ( ( ( 0 ..^ S ) e. Fin /\ 1 e. CC ) -> sum_ a e. ( 0 ..^ S ) 1 = ( ( # ` ( 0 ..^ S ) ) x. 1 ) ) |
34 |
10 32 33
|
mp2an |
|- sum_ a e. ( 0 ..^ S ) 1 = ( ( # ` ( 0 ..^ S ) ) x. 1 ) |
35 |
|
hashcl |
|- ( ( 0 ..^ S ) e. Fin -> ( # ` ( 0 ..^ S ) ) e. NN0 ) |
36 |
10 35
|
ax-mp |
|- ( # ` ( 0 ..^ S ) ) e. NN0 |
37 |
36
|
nn0cni |
|- ( # ` ( 0 ..^ S ) ) e. CC |
38 |
37
|
mulid1i |
|- ( ( # ` ( 0 ..^ S ) ) x. 1 ) = ( # ` ( 0 ..^ S ) ) |
39 |
34 38
|
eqtri |
|- sum_ a e. ( 0 ..^ S ) 1 = ( # ` ( 0 ..^ S ) ) |
40 |
|
hashfzo0 |
|- ( S e. NN0 -> ( # ` ( 0 ..^ S ) ) = S ) |
41 |
3 40
|
syl |
|- ( ph -> ( # ` ( 0 ..^ S ) ) = S ) |
42 |
39 41
|
syl5eq |
|- ( ph -> sum_ a e. ( 0 ..^ S ) 1 = S ) |
43 |
42
|
adantr |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) 1 = S ) |
44 |
|
1red |
|- ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> 1 e. RR ) |
45 |
1
|
ad2antrr |
|- ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> A C_ NN ) |
46 |
45 28
|
sseldd |
|- ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. NN ) |
47 |
|
nnge1 |
|- ( ( c ` a ) e. NN -> 1 <_ ( c ` a ) ) |
48 |
46 47
|
syl |
|- ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> 1 <_ ( c ` a ) ) |
49 |
11 44 29 48
|
fsumle |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) 1 <_ sum_ a e. ( 0 ..^ S ) ( c ` a ) ) |
50 |
43 49
|
eqbrtrrd |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> S <_ sum_ a e. ( 0 ..^ S ) ( c ` a ) ) |
51 |
7 9 30 31 50
|
ltletrd |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> M < sum_ a e. ( 0 ..^ S ) ( c ` a ) ) |
52 |
7 51
|
ltned |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> M =/= sum_ a e. ( 0 ..^ S ) ( c ` a ) ) |
53 |
52
|
necomd |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) =/= M ) |
54 |
53
|
neneqd |
|- ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> -. sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) |
55 |
54
|
ralrimiva |
|- ( ph -> A. c e. ( A ^m ( 0 ..^ S ) ) -. sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) |
56 |
|
rabeq0 |
|- ( { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } = (/) <-> A. c e. ( A ^m ( 0 ..^ S ) ) -. sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) |
57 |
55 56
|
sylibr |
|- ( ph -> { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } = (/) ) |
58 |
5 57
|
eqtrd |
|- ( ph -> ( A ( repr ` S ) M ) = (/) ) |