Metamath Proof Explorer

Theorem mdetunilem8

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

Ref Expression
Hypotheses mdetuni.a 
|- A = ( N Mat R )
mdetuni.b 
|- B = ( Base ` A )
mdetuni.k 
|- K = ( Base ` R )
mdetuni.0g 
|- .0. = ( 0g ` R )
mdetuni.1r 
|- .1. = ( 1r ` R )
mdetuni.pg 
|- .+ = ( +g ` R )
mdetuni.tg 
|- .x. = ( .r ` R )
mdetuni.n 
|- ( ph -> N e. Fin )
mdetuni.r 
|- ( ph -> R e. Ring )
mdetuni.ff 
|- ( ph -> D : B --> K )
mdetuni.al 
|- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )
mdetuni.li 
|- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
mdetuni.sc 
|- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )
mdetunilem8.id 
|- ( ph -> ( D ` ( 1r ` A ) ) = .0. )
Assertion mdetunilem8 
|- ( ( ph /\ E : N --> N ) -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = .0. )

Proof

Step Hyp Ref Expression
1 mdetuni.a 
 |-  A = ( N Mat R )
2 mdetuni.b 
 |-  B = ( Base ` A )
3 mdetuni.k 
 |-  K = ( Base ` R )
4 mdetuni.0g 
 |-  .0. = ( 0g ` R )
5 mdetuni.1r 
 |-  .1. = ( 1r ` R )
6 mdetuni.pg 
 |-  .+ = ( +g ` R )
7 mdetuni.tg 
 |-  .x. = ( .r ` R )
8 mdetuni.n 
 |-  ( ph -> N e. Fin )
9 mdetuni.r 
 |-  ( ph -> R e. Ring )
10 mdetuni.ff 
 |-  ( ph -> D : B --> K )
11 mdetuni.al 
 |-  ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )
12 mdetuni.li 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
13 mdetuni.sc 
 |-  ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )
14 mdetunilem8.id 
 |-  ( ph -> ( D ` ( 1r ` A ) ) = .0. )
15 simpl 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ph )
16 enrefg 
 |-  ( N e. Fin -> N ~~ N )
17 8 16 syl 
 |-  ( ph -> N ~~ N )
18 f1finf1o 
 |-  ( ( N ~~ N /\ N e. Fin ) -> ( E : N -1-1-> N <-> E : N -1-1-onto-> N ) )
19 17 8 18 syl2anc 
 |-  ( ph -> ( E : N -1-1-> N <-> E : N -1-1-onto-> N ) )
20 19 biimpa 
 |-  ( ( ph /\ E : N -1-1-> N ) -> E : N -1-1-onto-> N )
21 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
22 8 9 21 syl2anc 
 |-  ( ph -> A e. Ring )
23 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
24 2 23 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
25 22 24 syl 
 |-  ( ph -> ( 1r ` A ) e. B )
26 25 adantr 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( 1r ` A ) e. B )
27 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem7 
 |-  ( ( ph /\ E : N -1-1-onto-> N /\ ( 1r ` A ) e. B ) -> ( D ` ( a e. N , b e. N |-> ( ( E ` a ) ( 1r ` A ) b ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) .x. ( D ` ( 1r ` A ) ) ) )
28 15 20 26 27 syl3anc 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( D ` ( a e. N , b e. N |-> ( ( E ` a ) ( 1r ` A ) b ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) .x. ( D ` ( 1r ` A ) ) ) )
29 8 adantr 
 |-  ( ( ph /\ E : N -1-1-> N ) -> N e. Fin )
30 29 3ad2ant1 
 |-  ( ( ( ph /\ E : N -1-1-> N ) /\ a e. N /\ b e. N ) -> N e. Fin )
31 9 adantr 
 |-  ( ( ph /\ E : N -1-1-> N ) -> R e. Ring )
32 31 3ad2ant1 
 |-  ( ( ( ph /\ E : N -1-1-> N ) /\ a e. N /\ b e. N ) -> R e. Ring )
33 simp1r 
 |-  ( ( ( ph /\ E : N -1-1-> N ) /\ a e. N /\ b e. N ) -> E : N -1-1-> N )
34 f1f 
 |-  ( E : N -1-1-> N -> E : N --> N )
35 33 34 syl 
 |-  ( ( ( ph /\ E : N -1-1-> N ) /\ a e. N /\ b e. N ) -> E : N --> N )
36 simp2 
 |-  ( ( ( ph /\ E : N -1-1-> N ) /\ a e. N /\ b e. N ) -> a e. N )
37 35 36 ffvelrnd 
 |-  ( ( ( ph /\ E : N -1-1-> N ) /\ a e. N /\ b e. N ) -> ( E ` a ) e. N )
38 simp3 
 |-  ( ( ( ph /\ E : N -1-1-> N ) /\ a e. N /\ b e. N ) -> b e. N )
39 1 5 4 30 32 37 38 23 mat1ov 
 |-  ( ( ( ph /\ E : N -1-1-> N ) /\ a e. N /\ b e. N ) -> ( ( E ` a ) ( 1r ` A ) b ) = if ( ( E ` a ) = b , .1. , .0. ) )
40 39 mpoeq3dva 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( a e. N , b e. N |-> ( ( E ` a ) ( 1r ` A ) b ) ) = ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) )
41 40 fveq2d 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( D ` ( a e. N , b e. N |-> ( ( E ` a ) ( 1r ` A ) b ) ) ) = ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) )
42 14 adantr 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( D ` ( 1r ` A ) ) = .0. )
43 42 oveq2d 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) .x. ( D ` ( 1r ` A ) ) ) = ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) .x. .0. ) )
44 zrhpsgnmhm 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
45 9 8 44 syl2anc 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) )
46 eqid 
 |-  ( Base ` ( SymGrp ` N ) ) = ( Base ` ( SymGrp ` N ) )
47 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
48 47 3 mgpbas 
 |-  K = ( Base ` ( mulGrp ` R ) )
49 46 48 mhmf 
 |-  ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) e. ( ( SymGrp ` N ) MndHom ( mulGrp ` R ) ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
50 45 49 syl 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
51 50 adantr 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) : ( Base ` ( SymGrp ` N ) ) --> K )
52 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
53 52 46 elsymgbas 
 |-  ( N e. Fin -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
54 29 53 syl 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( E e. ( Base ` ( SymGrp ` N ) ) <-> E : N -1-1-onto-> N ) )
55 20 54 mpbird 
 |-  ( ( ph /\ E : N -1-1-> N ) -> E e. ( Base ` ( SymGrp ` N ) ) )
56 51 55 ffvelrnd 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) e. K )
57 3 7 4 ringrz 
 |-  ( ( R e. Ring /\ ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) e. K ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) .x. .0. ) = .0. )
58 31 56 57 syl2anc 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) .x. .0. ) = .0. )
59 43 58 eqtrd 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( ( ( ( ZRHom ` R ) o. ( pmSgn ` N ) ) ` E ) .x. ( D ` ( 1r ` A ) ) ) = .0. )
60 28 41 59 3eqtr3d 
 |-  ( ( ph /\ E : N -1-1-> N ) -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = .0. )
61 60 ex 
 |-  ( ph -> ( E : N -1-1-> N -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = .0. ) )
62 61 adantr 
 |-  ( ( ph /\ E : N --> N ) -> ( E : N -1-1-> N -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = .0. ) )
63 dff13 
 |-  ( E : N -1-1-> N <-> ( E : N --> N /\ A. c e. N A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) ) )
64 ibar 
 |-  ( E : N --> N -> ( A. c e. N A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) <-> ( E : N --> N /\ A. c e. N A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) ) ) )
65 64 adantl 
 |-  ( ( ph /\ E : N --> N ) -> ( A. c e. N A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) <-> ( E : N --> N /\ A. c e. N A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) ) ) )
66 63 65 bitr4id 
 |-  ( ( ph /\ E : N --> N ) -> ( E : N -1-1-> N <-> A. c e. N A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) ) )
67 66 notbid 
 |-  ( ( ph /\ E : N --> N ) -> ( -. E : N -1-1-> N <-> -. A. c e. N A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) ) )
68 rexnal 
 |-  ( E. c e. N -. A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) <-> -. A. c e. N A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) )
69 rexnal 
 |-  ( E. d e. N -. ( ( E ` c ) = ( E ` d ) -> c = d ) <-> -. A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) )
70 df-ne 
 |-  ( c =/= d <-> -. c = d )
71 70 anbi2i 
 |-  ( ( ( E ` c ) = ( E ` d ) /\ c =/= d ) <-> ( ( E ` c ) = ( E ` d ) /\ -. c = d ) )
72 annim 
 |-  ( ( ( E ` c ) = ( E ` d ) /\ -. c = d ) <-> -. ( ( E ` c ) = ( E ` d ) -> c = d ) )
73 71 72 bitr2i 
 |-  ( -. ( ( E ` c ) = ( E ` d ) -> c = d ) <-> ( ( E ` c ) = ( E ` d ) /\ c =/= d ) )
74 73 rexbii 
 |-  ( E. d e. N -. ( ( E ` c ) = ( E ` d ) -> c = d ) <-> E. d e. N ( ( E ` c ) = ( E ` d ) /\ c =/= d ) )
75 69 74 bitr3i 
 |-  ( -. A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) <-> E. d e. N ( ( E ` c ) = ( E ` d ) /\ c =/= d ) )
76 75 rexbii 
 |-  ( E. c e. N -. A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) <-> E. c e. N E. d e. N ( ( E ` c ) = ( E ` d ) /\ c =/= d ) )
77 68 76 bitr3i 
 |-  ( -. A. c e. N A. d e. N ( ( E ` c ) = ( E ` d ) -> c = d ) <-> E. c e. N E. d e. N ( ( E ` c ) = ( E ` d ) /\ c =/= d ) )
78 67 77 bitrdi 
 |-  ( ( ph /\ E : N --> N ) -> ( -. E : N -1-1-> N <-> E. c e. N E. d e. N ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) )
79 simprrl 
 |-  ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) -> ( E ` c ) = ( E ` d ) )
80 fveqeq2 
 |-  ( a = c -> ( ( E ` a ) = b <-> ( E ` c ) = b ) )
81 80 ifbid 
 |-  ( a = c -> if ( ( E ` a ) = b , .1. , .0. ) = if ( ( E ` c ) = b , .1. , .0. ) )
82 iftrue 
 |-  ( a = c -> if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) = if ( ( E ` c ) = b , .1. , .0. ) )
83 81 82 eqtr4d 
 |-  ( a = c -> if ( ( E ` a ) = b , .1. , .0. ) = if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) )
84 fveqeq2 
 |-  ( a = d -> ( ( E ` a ) = b <-> ( E ` d ) = b ) )
85 84 ifbid 
 |-  ( a = d -> if ( ( E ` a ) = b , .1. , .0. ) = if ( ( E ` d ) = b , .1. , .0. ) )
86 iftrue 
 |-  ( a = d -> if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) = if ( ( E ` d ) = b , .1. , .0. ) )
87 85 86 eqtr4d 
 |-  ( a = d -> if ( ( E ` a ) = b , .1. , .0. ) = if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) )
88 iffalse 
 |-  ( -. a = d -> if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) = if ( ( E ` a ) = b , .1. , .0. ) )
89 88 eqcomd 
 |-  ( -. a = d -> if ( ( E ` a ) = b , .1. , .0. ) = if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) )
90 87 89 pm2.61i 
 |-  if ( ( E ` a ) = b , .1. , .0. ) = if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) )
91 iffalse 
 |-  ( -. a = c -> if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) = if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) )
92 90 91 eqtr4id 
 |-  ( -. a = c -> if ( ( E ` a ) = b , .1. , .0. ) = if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) )
93 83 92 pm2.61i 
 |-  if ( ( E ` a ) = b , .1. , .0. ) = if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) )
94 eqeq1 
 |-  ( ( E ` d ) = ( E ` c ) -> ( ( E ` d ) = b <-> ( E ` c ) = b ) )
95 94 eqcoms 
 |-  ( ( E ` c ) = ( E ` d ) -> ( ( E ` d ) = b <-> ( E ` c ) = b ) )
96 95 ifbid 
 |-  ( ( E ` c ) = ( E ` d ) -> if ( ( E ` d ) = b , .1. , .0. ) = if ( ( E ` c ) = b , .1. , .0. ) )
97 96 ifeq1d 
 |-  ( ( E ` c ) = ( E ` d ) -> if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) = if ( a = d , if ( ( E ` c ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) )
98 97 ifeq2d 
 |-  ( ( E ` c ) = ( E ` d ) -> if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` d ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) = if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` c ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) )
99 93 98 eqtrid 
 |-  ( ( E ` c ) = ( E ` d ) -> if ( ( E ` a ) = b , .1. , .0. ) = if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` c ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) )
100 99 mpoeq3dv 
 |-  ( ( E ` c ) = ( E ` d ) -> ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) = ( a e. N , b e. N |-> if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` c ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) ) )
101 100 fveq2d 
 |-  ( ( E ` c ) = ( E ` d ) -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` c ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) ) ) )
102 79 101 syl 
 |-  ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = ( D ` ( a e. N , b e. N |-> if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` c ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) ) ) )
103 simpll 
 |-  ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) -> ph )
104 simprll 
 |-  ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) -> c e. N )
105 simprlr 
 |-  ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) -> d e. N )
106 simprrr 
 |-  ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) -> c =/= d )
107 104 105 106 3jca 
 |-  ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) -> ( c e. N /\ d e. N /\ c =/= d ) )
108 3 5 ringidcl 
 |-  ( R e. Ring -> .1. e. K )
109 9 108 syl 
 |-  ( ph -> .1. e. K )
110 3 4 ring0cl 
 |-  ( R e. Ring -> .0. e. K )
111 9 110 syl 
 |-  ( ph -> .0. e. K )
112 109 111 ifcld 
 |-  ( ph -> if ( ( E ` c ) = b , .1. , .0. ) e. K )
113 112 ad3antrrr 
 |-  ( ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) /\ b e. N ) -> if ( ( E ` c ) = b , .1. , .0. ) e. K )
114 simp1ll 
 |-  ( ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) /\ a e. N /\ b e. N ) -> ph )
115 109 111 ifcld 
 |-  ( ph -> if ( ( E ` a ) = b , .1. , .0. ) e. K )
116 114 115 syl 
 |-  ( ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) /\ a e. N /\ b e. N ) -> if ( ( E ` a ) = b , .1. , .0. ) e. K )
117 1 2 3 4 5 6 7 8 9 10 11 12 13 103 107 113 116 mdetunilem2 
 |-  ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) -> ( D ` ( a e. N , b e. N |-> if ( a = c , if ( ( E ` c ) = b , .1. , .0. ) , if ( a = d , if ( ( E ` c ) = b , .1. , .0. ) , if ( ( E ` a ) = b , .1. , .0. ) ) ) ) ) = .0. )
118 102 117 eqtrd 
 |-  ( ( ( ph /\ E : N --> N ) /\ ( ( c e. N /\ d e. N ) /\ ( ( E ` c ) = ( E ` d ) /\ c =/= d ) ) ) -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = .0. )
119 118 expr 
 |-  ( ( ( ph /\ E : N --> N ) /\ ( c e. N /\ d e. N ) ) -> ( ( ( E ` c ) = ( E ` d ) /\ c =/= d ) -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = .0. ) )
120 119 rexlimdvva 
 |-  ( ( ph /\ E : N --> N ) -> ( E. c e. N E. d e. N ( ( E ` c ) = ( E ` d ) /\ c =/= d ) -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = .0. ) )
121 78 120 sylbid 
 |-  ( ( ph /\ E : N --> N ) -> ( -. E : N -1-1-> N -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = .0. ) )
122 62 121 pm2.61d 
 |-  ( ( ph /\ E : N --> N ) -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = .0. )