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

Metamath Proof Explorer

Theorem mdetunilem8

Description: Lemma for mdetuni . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses mdetuni.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetuni.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mdetuni.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mdetuni.0g ⊢ 0 = ( 0g ‘ 𝑅 )
mdetuni.1r ⊢ 1 = ( 1r ‘ 𝑅 )
mdetuni.pg ⊢ + = ( +g ‘ 𝑅 )
mdetuni.tg ⊢ · = ( .r ‘ 𝑅 )
mdetuni.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mdetuni.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mdetuni.ff ⊢ ( 𝜑 → 𝐷 : 𝐵 ⟶ 𝐾 )
mdetuni.al ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) )
mdetuni.li ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
mdetuni.sc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
mdetunilem8.id ⊢ ( 𝜑 → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) = 0 )
Assertion mdetunilem8 ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 mdetuni.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mdetuni.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 mdetuni.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 mdetuni.0g ⊢ 0 = ( 0g ‘ 𝑅 )
5 mdetuni.1r ⊢ 1 = ( 1r ‘ 𝑅 )
6 mdetuni.pg ⊢ + = ( +g ‘ 𝑅 )
7 mdetuni.tg ⊢ · = ( .r ‘ 𝑅 )
8 mdetuni.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
9 mdetuni.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 mdetuni.ff ⊢ ( 𝜑 → 𝐷 : 𝐵 ⟶ 𝐾 )
11 mdetuni.al ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) )
12 mdetuni.li ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
13 mdetuni.sc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
14 mdetunilem8.id ⊢ ( 𝜑 → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) = 0 )
15 simpl ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → 𝜑 )
16 enrefg ⊢ ( 𝑁 ∈ Fin → 𝑁 ≈ 𝑁 )
17 8 16 syl ⊢ ( 𝜑 → 𝑁 ≈ 𝑁 )
18 f1finf1o ⊢ ( ( 𝑁 ≈ 𝑁 ∧ 𝑁 ∈ Fin ) → ( 𝐸 : 𝑁 –1-1→ 𝑁 ↔ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ) )
19 17 8 18 syl2anc ⊢ ( 𝜑 → ( 𝐸 : 𝑁 –1-1→ 𝑁 ↔ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ) )
20 19 biimpa ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → 𝐸 : 𝑁 –1-1-onto→ 𝑁 )
21 1 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
22 8 9 21 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ Ring )
23 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
24 2 23 ringidcl ⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
25 22 24 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
27 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem7 ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝐸 ‘ 𝑎 ) ( 1r ‘ 𝐴 ) 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ) )
28 15 20 26 27 syl3anc ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝐸 ‘ 𝑎 ) ( 1r ‘ 𝐴 ) 𝑏 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ) )
29 8 adantr ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → 𝑁 ∈ Fin )
30 29 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑁 ∈ Fin )
31 9 adantr ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → 𝑅 ∈ Ring )
32 31 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑅 ∈ Ring )
33 simp1r ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐸 : 𝑁 –1-1→ 𝑁 )
34 f1f ⊢ ( 𝐸 : 𝑁 –1-1→ 𝑁 → 𝐸 : 𝑁 ⟶ 𝑁 )
35 33 34 syl ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐸 : 𝑁 ⟶ 𝑁 )
36 simp2 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
37 35 36 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐸 ‘ 𝑎 ) ∈ 𝑁 )
38 simp3 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
39 1 5 4 30 32 37 38 23 mat1ov ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝐸 ‘ 𝑎 ) ( 1r ‘ 𝐴 ) 𝑏 ) = if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) )
40 39 mpoeq3dva ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝐸 ‘ 𝑎 ) ( 1r ‘ 𝐴 ) 𝑏 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) )
41 40 fveq2d ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( ( 𝐸 ‘ 𝑎 ) ( 1r ‘ 𝐴 ) 𝑏 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) )
42 14 adantr ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) = 0 )
43 42 oveq2d ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ) = ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · 0 ) )
44 zrhpsgnmhm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
45 9 8 44 syl2anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
46 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
47 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
48 47 3 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
49 46 48 mhmf ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ∈ ( ( SymGrp ‘ 𝑁 ) MndHom ( mulGrp ‘ 𝑅 ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
50 45 49 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ 𝐾 )
52 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
53 52 46 elsymgbas ⊢ ( 𝑁 ∈ Fin → ( 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↔ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ) )
54 29 53 syl ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↔ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ) )
55 20 54 mpbird ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
56 51 55 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) ∈ 𝐾 )
57 3 7 4 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) ∈ 𝐾 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · 0 ) = 0 )
58 31 56 57 syl2anc ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · 0 ) = 0 )
59 43 58 eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝐸 ) · ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ) = 0 )
60 28 41 59 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 –1-1→ 𝑁 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = 0 )
61 60 ex ⊢ ( 𝜑 → ( 𝐸 : 𝑁 –1-1→ 𝑁 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = 0 ) )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) → ( 𝐸 : 𝑁 –1-1→ 𝑁 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = 0 ) )
63 dff13 ⊢ ( 𝐸 : 𝑁 –1-1→ 𝑁 ↔ ( 𝐸 : 𝑁 ⟶ 𝑁 ∧ ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ) )
64 ibar ⊢ ( 𝐸 : 𝑁 ⟶ 𝑁 → ( ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ↔ ( 𝐸 : 𝑁 ⟶ 𝑁 ∧ ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ) ) )
65 64 adantl ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) → ( ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ↔ ( 𝐸 : 𝑁 ⟶ 𝑁 ∧ ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ) ) )
66 63 65 bitr4id ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) → ( 𝐸 : 𝑁 –1-1→ 𝑁 ↔ ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ) )
67 66 notbid ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) → ( ¬ 𝐸 : 𝑁 –1-1→ 𝑁 ↔ ¬ ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ) )
68 rexnal ⊢ ( ∃ 𝑐 ∈ 𝑁 ¬ ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ↔ ¬ ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) )
69 rexnal ⊢ ( ∃ 𝑑 ∈ 𝑁 ¬ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ↔ ¬ ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) )
70 df-ne ⊢ ( 𝑐 ≠ 𝑑 ↔ ¬ 𝑐 = 𝑑 )
71 70 anbi2i ⊢ ( ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ↔ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ ¬ 𝑐 = 𝑑 ) )
72 annim ⊢ ( ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ ¬ 𝑐 = 𝑑 ) ↔ ¬ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) )
73 71 72 bitr2i ⊢ ( ¬ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ↔ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) )
74 73 rexbii ⊢ ( ∃ 𝑑 ∈ 𝑁 ¬ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ↔ ∃ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) )
75 69 74 bitr3i ⊢ ( ¬ ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ↔ ∃ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) )
76 75 rexbii ⊢ ( ∃ 𝑐 ∈ 𝑁 ¬ ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ↔ ∃ 𝑐 ∈ 𝑁 ∃ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) )
77 68 76 bitr3i ⊢ ( ¬ ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → 𝑐 = 𝑑 ) ↔ ∃ 𝑐 ∈ 𝑁 ∃ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) )
78 67 77 bitrdi ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) → ( ¬ 𝐸 : 𝑁 –1-1→ 𝑁 ↔ ∃ 𝑐 ∈ 𝑁 ∃ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) )
79 simprrl ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) → ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) )
80 fveqeq2 ⊢ ( 𝑎 = 𝑐 → ( ( 𝐸 ‘ 𝑎 ) = 𝑏 ↔ ( 𝐸 ‘ 𝑐 ) = 𝑏 ) )
81 80 ifbid ⊢ ( 𝑎 = 𝑐 → if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) = if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) )
82 iftrue ⊢ ( 𝑎 = 𝑐 → if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) )
83 81 82 eqtr4d ⊢ ( 𝑎 = 𝑐 → if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) = if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) )
84 fveqeq2 ⊢ ( 𝑎 = 𝑑 → ( ( 𝐸 ‘ 𝑎 ) = 𝑏 ↔ ( 𝐸 ‘ 𝑑 ) = 𝑏 ) )
85 84 ifbid ⊢ ( 𝑎 = 𝑑 → if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) = if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) )
86 iftrue ⊢ ( 𝑎 = 𝑑 → if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) = if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) )
87 85 86 eqtr4d ⊢ ( 𝑎 = 𝑑 → if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) = if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) )
88 iffalse ⊢ ( ¬ 𝑎 = 𝑑 → if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) = if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) )
89 88 eqcomd ⊢ ( ¬ 𝑎 = 𝑑 → if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) = if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) )
90 87 89 pm2.61i ⊢ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) = if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) )
91 iffalse ⊢ ( ¬ 𝑎 = 𝑐 → if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) )
92 90 91 eqtr4id ⊢ ( ¬ 𝑎 = 𝑐 → if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) = if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) )
93 83 92 pm2.61i ⊢ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) = if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) )
94 eqeq1 ⊢ ( ( 𝐸 ‘ 𝑑 ) = ( 𝐸 ‘ 𝑐 ) → ( ( 𝐸 ‘ 𝑑 ) = 𝑏 ↔ ( 𝐸 ‘ 𝑐 ) = 𝑏 ) )
95 94 eqcoms ⊢ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → ( ( 𝐸 ‘ 𝑑 ) = 𝑏 ↔ ( 𝐸 ‘ 𝑐 ) = 𝑏 ) )
96 95 ifbid ⊢ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) = if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) )
97 96 ifeq1d ⊢ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) = if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) )
98 97 ifeq2d ⊢ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑑 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) )
99 93 98 eqtrid ⊢ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) = if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) )
100 99 mpoeq3dv ⊢ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) ) )
101 100 fveq2d ⊢ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) ) ) )
102 79 101 syl ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) ) ) )
103 simpll ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) → 𝜑 )
104 simprll ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) → 𝑐 ∈ 𝑁 )
105 simprlr ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) → 𝑑 ∈ 𝑁 )
106 simprrr ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) → 𝑐 ≠ 𝑑 )
107 104 105 106 3jca ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) → ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ∧ 𝑐 ≠ 𝑑 ) )
108 3 5 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐾 )
109 9 108 syl ⊢ ( 𝜑 → 1 ∈ 𝐾 )
110 3 4 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 )
111 9 110 syl ⊢ ( 𝜑 → 0 ∈ 𝐾 )
112 109 111 ifcld ⊢ ( 𝜑 → if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) ∈ 𝐾 )
113 112 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑁 ) → if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) ∈ 𝐾 )
114 simp1ll ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝜑 )
115 109 111 ifcld ⊢ ( 𝜑 → if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ∈ 𝐾 )
116 114 115 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ∈ 𝐾 )
117 1 2 3 4 5 6 7 8 9 10 11 12 13 103 107 113 116 mdetunilem2 ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑐 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( 𝑎 = 𝑑 , if ( ( 𝐸 ‘ 𝑐 ) = 𝑏 , 1 , 0 ) , if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) ) ) = 0 )
118 102 117 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = 0 )
119 118 expr ⊢ ( ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) ∧ ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) → ( ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = 0 ) )
120 119 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) → ( ∃ 𝑐 ∈ 𝑁 ∃ 𝑑 ∈ 𝑁 ( ( 𝐸 ‘ 𝑐 ) = ( 𝐸 ‘ 𝑑 ) ∧ 𝑐 ≠ 𝑑 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = 0 ) )
121 78 120 sylbid ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) → ( ¬ 𝐸 : 𝑁 –1-1→ 𝑁 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = 0 ) )
122 62 121 pm2.61d ⊢ ( ( 𝜑 ∧ 𝐸 : 𝑁 ⟶ 𝑁 ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( ( 𝐸 ‘ 𝑎 ) = 𝑏 , 1 , 0 ) ) ) = 0 )