mdetunilem8

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

Metamath Proof Explorer

Theorem mdetunilem8

Proof