Metamath Proof Explorer

Theorem repr0

Description: There is exactly one representation with no elements (an empty sum), only for M = 0 . (Contributed by Thierry Arnoux, 2-Dec-2021)

Ref Expression
Hypotheses reprval.a 
|- ( ph -> A C_ NN )
reprval.m 
|- ( ph -> M e. ZZ )
reprval.s 
|- ( ph -> S e. NN0 )
Assertion repr0 
|- ( ph -> ( A ( repr ` 0 ) M ) = if ( M = 0 , { (/) } , (/) ) )

Proof

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 0nn0 
 |-  0 e. NN0
5 4 a1i 
 |-  ( ph -> 0 e. NN0 )
6 1 2 5 reprval 
 |-  ( ph -> ( A ( repr ` 0 ) M ) = { c e. ( A ^m ( 0 ..^ 0 ) ) | sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M } )
7 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
8 7 sumeq1i 
 |-  sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = sum_ a e. (/) ( c ` a )
9 sum0 
 |-  sum_ a e. (/) ( c ` a ) = 0
10 8 9 eqtri 
 |-  sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = 0
11 10 eqeq1i 
 |-  ( sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M <-> 0 = M )
12 11 a1i 
 |-  ( c = (/) -> ( sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M <-> 0 = M ) )
13 0ex 
 |-  (/) e. _V
14 13 snid 
 |-  (/) e. { (/) }
15 nnex 
 |-  NN e. _V
16 15 a1i 
 |-  ( ph -> NN e. _V )
17 16 1 ssexd 
 |-  ( ph -> A e. _V )
18 mapdm0 
 |-  ( A e. _V -> ( A ^m (/) ) = { (/) } )
19 17 18 syl 
 |-  ( ph -> ( A ^m (/) ) = { (/) } )
20 14 19 eleqtrrid 
 |-  ( ph -> (/) e. ( A ^m (/) ) )
21 7 oveq2i 
 |-  ( A ^m ( 0 ..^ 0 ) ) = ( A ^m (/) )
22 20 21 eleqtrrdi 
 |-  ( ph -> (/) e. ( A ^m ( 0 ..^ 0 ) ) )
23 22 adantr 
 |-  ( ( ph /\ M = 0 ) -> (/) e. ( A ^m ( 0 ..^ 0 ) ) )
24 simpr 
 |-  ( ( ph /\ M = 0 ) -> M = 0 )
25 24 eqcomd 
 |-  ( ( ph /\ M = 0 ) -> 0 = M )
26 21 19 eqtrid 
 |-  ( ph -> ( A ^m ( 0 ..^ 0 ) ) = { (/) } )
27 26 eleq2d 
 |-  ( ph -> ( c e. ( A ^m ( 0 ..^ 0 ) ) <-> c e. { (/) } ) )
28 27 biimpa 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ 0 ) ) ) -> c e. { (/) } )
29 elsni 
 |-  ( c e. { (/) } -> c = (/) )
30 28 29 syl 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ 0 ) ) ) -> c = (/) )
31 30 ad4ant13 
 |-  ( ( ( ( ph /\ M = 0 ) /\ c e. ( A ^m ( 0 ..^ 0 ) ) ) /\ sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M ) -> c = (/) )
32 12 23 25 31 rabeqsnd 
 |-  ( ( ph /\ M = 0 ) -> { c e. ( A ^m ( 0 ..^ 0 ) ) | sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M } = { (/) } )
33 32 eqcomd 
 |-  ( ( ph /\ M = 0 ) -> { (/) } = { c e. ( A ^m ( 0 ..^ 0 ) ) | sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M } )
34 10 a1i 
 |-  ( ( ( ph /\ -. M = 0 ) /\ c e. ( A ^m ( 0 ..^ 0 ) ) ) -> sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = 0 )
35 simplr 
 |-  ( ( ( ph /\ -. M = 0 ) /\ c e. ( A ^m ( 0 ..^ 0 ) ) ) -> -. M = 0 )
36 35 neqned 
 |-  ( ( ( ph /\ -. M = 0 ) /\ c e. ( A ^m ( 0 ..^ 0 ) ) ) -> M =/= 0 )
37 36 necomd 
 |-  ( ( ( ph /\ -. M = 0 ) /\ c e. ( A ^m ( 0 ..^ 0 ) ) ) -> 0 =/= M )
38 34 37 eqnetrd 
 |-  ( ( ( ph /\ -. M = 0 ) /\ c e. ( A ^m ( 0 ..^ 0 ) ) ) -> sum_ a e. ( 0 ..^ 0 ) ( c ` a ) =/= M )
39 38 neneqd 
 |-  ( ( ( ph /\ -. M = 0 ) /\ c e. ( A ^m ( 0 ..^ 0 ) ) ) -> -. sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M )
40 39 ralrimiva 
 |-  ( ( ph /\ -. M = 0 ) -> A. c e. ( A ^m ( 0 ..^ 0 ) ) -. sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M )
41 rabeq0 
 |-  ( { c e. ( A ^m ( 0 ..^ 0 ) ) | sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M } = (/) <-> A. c e. ( A ^m ( 0 ..^ 0 ) ) -. sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M )
42 40 41 sylibr 
 |-  ( ( ph /\ -. M = 0 ) -> { c e. ( A ^m ( 0 ..^ 0 ) ) | sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M } = (/) )
43 42 eqcomd 
 |-  ( ( ph /\ -. M = 0 ) -> (/) = { c e. ( A ^m ( 0 ..^ 0 ) ) | sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M } )
44 33 43 ifeqda 
 |-  ( ph -> if ( M = 0 , { (/) } , (/) ) = { c e. ( A ^m ( 0 ..^ 0 ) ) | sum_ a e. ( 0 ..^ 0 ) ( c ` a ) = M } )
45 6 44 eqtr4d 
 |-  ( ph -> ( A ( repr ` 0 ) M ) = if ( M = 0 , { (/) } , (/) ) )