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 , { ∅ } , ∅ ) )