This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
Assertion repr0 ( 𝜑 → ( 𝐴 ( repr ‘ 0 ) 𝑀 ) = if ( 𝑀 = 0 , { ∅ } , ∅ ) )

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2 reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4 0nn0 ⊢ 0 ∈ ℕ0
5 4 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
6 1 2 5 reprval ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 0 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
7 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
8 7 sumeq1i ⊢ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = Σ 𝑎 ∈ ∅ ( 𝑐 ‘ 𝑎 )
9 sum0 ⊢ Σ 𝑎 ∈ ∅ ( 𝑐 ‘ 𝑎 ) = 0
10 8 9 eqtri ⊢ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 0
11 10 eqeq1i ⊢ ( Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ↔ 0 = 𝑀 )
12 11 a1i ⊢ ( 𝑐 = ∅ → ( Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ↔ 0 = 𝑀 ) )
13 0ex ⊢ ∅ ∈ V
14 13 snid ⊢ ∅ ∈ { ∅ }
15 nnex ⊢ ℕ ∈ V
16 15 a1i ⊢ ( 𝜑 → ℕ ∈ V )
17 16 1 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
18 mapdm0 ⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m ∅ ) = { ∅ } )
19 17 18 syl ⊢ ( 𝜑 → ( 𝐴 ↑m ∅ ) = { ∅ } )
20 14 19 eleqtrrid ⊢ ( 𝜑 → ∅ ∈ ( 𝐴 ↑m ∅ ) )
21 7 oveq2i ⊢ ( 𝐴 ↑m ( 0 ..^ 0 ) ) = ( 𝐴 ↑m ∅ )
22 20 21 eleqtrrdi ⊢ ( 𝜑 → ∅ ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 0 ) → ∅ ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑀 = 0 ) → 𝑀 = 0 )
25 24 eqcomd ⊢ ( ( 𝜑 ∧ 𝑀 = 0 ) → 0 = 𝑀 )
26 21 19 eqtrid ⊢ ( 𝜑 → ( 𝐴 ↑m ( 0 ..^ 0 ) ) = { ∅ } )
27 26 eleq2d ⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ↔ 𝑐 ∈ { ∅ } ) )
28 27 biimpa ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ) → 𝑐 ∈ { ∅ } )
29 elsni ⊢ ( 𝑐 ∈ { ∅ } → 𝑐 = ∅ )
30 28 29 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ) → 𝑐 = ∅ )
31 30 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑀 = 0 ) ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) → 𝑐 = ∅ )
32 12 23 25 31 rabeqsnd ⊢ ( ( 𝜑 ∧ 𝑀 = 0 ) → { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } = { ∅ } )
33 32 eqcomd ⊢ ( ( 𝜑 ∧ 𝑀 = 0 ) → { ∅ } = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
34 10 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 0 ) ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 0 )
35 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 0 ) ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ) → ¬ 𝑀 = 0 )
36 35 neqned ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 0 ) ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ) → 𝑀 ≠ 0 )
37 36 necomd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 0 ) ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ) → 0 ≠ 𝑀 )
38 34 37 eqnetrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 0 ) ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ) → Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) ≠ 𝑀 )
39 38 neneqd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 0 ) ∧ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ) → ¬ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 )
40 39 ralrimiva ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 0 ) → ∀ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ¬ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 )
41 rabeq0 ⊢ ( { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } = ∅ ↔ ∀ 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ¬ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 )
42 40 41 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 0 ) → { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } = ∅ )
43 42 eqcomd ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 0 ) → ∅ = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
44 33 43 ifeqda ⊢ ( 𝜑 → if ( 𝑀 = 0 , { ∅ } , ∅ ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 0 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 0 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
45 6 44 eqtr4d ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 0 ) 𝑀 ) = if ( 𝑀 = 0 , { ∅ } , ∅ ) )