Theorem mdetunilem6

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

	Ref	Expression
Hypotheses	mdetuni.a	$$⊢A=N\mathrm{Mat}R$$
	mdetuni.b	$$⊢B={\mathrm{Base}}_A$$
	mdetuni.k	$$⊢K={\mathrm{Base}}_R$$
	mdetuni.0g	$$⊢\underset{\dot{}}{0}=0_R$$
	mdetuni.1r	$$⊢\underset{\dot{}}{1}=1_R$$
	mdetuni.pg	$$⊢\underset{\dot{}}{+}={+}_R$$
	mdetuni.tg	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mdetuni.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	mdetuni.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mdetuni.ff	$$⊢\phi \to D:B⟶K$$
	mdetuni.al	$$⊢\phi \to \forall x\in B\forall y\in N\forall z\in N\left(\left(y\ne z\wedge \forall w\in Nyxw=zxw\right)\to D\left(x\right)=\underset{\dot{}}{0}\right)$$
	mdetuni.li	$$⊢\phi \to \forall x\in B\forall y\in B\forall z\in B\forall w\in N\left(\left({x\upharpoonright }_{\left(\left\{w\right\}\times N\right)}=\left({y\upharpoonright }_{\left(\left\{w\right\}\times N\right)}\right){\underset{\dot{}}{+}}_f\left({z\upharpoonright }_{\left(\left\{w\right\}\times N\right)}\right)\wedge {x\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}={y\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}\wedge {x\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}={z\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}\right)\to D\left(x\right)=D\left(y\right)\underset{\dot{}}{+}D\left(z\right)\right)$$
	mdetuni.sc	$$⊢\phi \to \forall x\in B\forall y\in K\forall z\in B\forall w\in N\left(\left({x\upharpoonright }_{\left(\left\{w\right\}\times N\right)}=\left(\left(\left\{w\right\}\times N\right)\times \left\{y\right\}\right){\underset{\dot{}}{·}}_f\left({z\upharpoonright }_{\left(\left\{w\right\}\times N\right)}\right)\wedge {x\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}={z\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}\right)\to D\left(x\right)=y\underset{\dot{}}{·}D\left(z\right)\right)$$
	mdetunilem6.ph	$$⊢\psi \to \phi$$
	mdetunilem6.ef	$$⊢\psi \to \left(E\in N\wedge F\in N\wedge E\ne F\right)$$
	mdetunilem6.gh	$$⊢\left(\psi \wedge b\in N\right)\to \left(G\in K\wedge H\in K\right)$$
	mdetunilem6.i	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to I\in K$$
Assertion	mdetunilem6	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)={inv}_g\left(R\right)\left(D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdetuni.a	$$⊢A=N\mathrm{Mat}R$$
2		mdetuni.b	$$⊢B={\mathrm{Base}}_A$$
3		mdetuni.k	$$⊢K={\mathrm{Base}}_R$$
4		mdetuni.0g	$$⊢\underset{\dot{}}{0}=0_R$$
5		mdetuni.1r	$$⊢\underset{\dot{}}{1}=1_R$$
6		mdetuni.pg	$$⊢\underset{\dot{}}{+}={+}_R$$
7		mdetuni.tg	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
8		mdetuni.n	$$⊢\phi \to N\in \mathrm{Fin}$$
9		mdetuni.r	$$⊢\phi \to R\in \mathrm{Ring}$$
10		mdetuni.ff	$$⊢\phi \to D:B⟶K$$
11		mdetuni.al	$$⊢\phi \to \forall x\in B\forall y\in N\forall z\in N\left(\left(y\ne z\wedge \forall w\in Nyxw=zxw\right)\to D\left(x\right)=\underset{\dot{}}{0}\right)$$
12		mdetuni.li	$$⊢\phi \to \forall x\in B\forall y\in B\forall z\in B\forall w\in N\left(\left({x\upharpoonright }_{\left(\left\{w\right\}\times N\right)}=\left({y\upharpoonright }_{\left(\left\{w\right\}\times N\right)}\right){\underset{\dot{}}{+}}_f\left({z\upharpoonright }_{\left(\left\{w\right\}\times N\right)}\right)\wedge {x\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}={y\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}\wedge {x\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}={z\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}\right)\to D\left(x\right)=D\left(y\right)\underset{\dot{}}{+}D\left(z\right)\right)$$
13		mdetuni.sc	$$⊢\phi \to \forall x\in B\forall y\in K\forall z\in B\forall w\in N\left(\left({x\upharpoonright }_{\left(\left\{w\right\}\times N\right)}=\left(\left(\left\{w\right\}\times N\right)\times \left\{y\right\}\right){\underset{\dot{}}{·}}_f\left({z\upharpoonright }_{\left(\left\{w\right\}\times N\right)}\right)\wedge {x\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}={z\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}\right)\to D\left(x\right)=y\underset{\dot{}}{·}D\left(z\right)\right)$$
14		mdetunilem6.ph	$$⊢\psi \to \phi$$
15		mdetunilem6.ef	$$⊢\psi \to \left(E\in N\wedge F\in N\wedge E\ne F\right)$$
16		mdetunilem6.gh	$$⊢\left(\psi \wedge b\in N\right)\to \left(G\in K\wedge H\in K\right)$$
17		mdetunilem6.i	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to I\in K$$
18	15	simp1d	$$⊢\psi \to E\in N$$
19	16	simprd	$$⊢\left(\psi \wedge b\in N\right)\to H\in K$$
20	19	3adant2	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to H\in K$$
21	16	simpld	$$⊢\left(\psi \wedge b\in N\right)\to G\in K$$
22	21	3adant2	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to G\in K$$
23		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
24	14 9 23	3syl	$$⊢\psi \to R\in \mathrm{Grp}$$
25	24	adantr	$$⊢\left(\psi \wedge b\in N\right)\to R\in \mathrm{Grp}$$
26	3 6	grpcl	$$⊢\left(R\in \mathrm{Grp}\wedge H\in K\wedge G\in K\right)\to H\underset{\dot{}}{+}G\in K$$
27	25 19 21 26	syl3anc	$$⊢\left(\psi \wedge b\in N\right)\to H\underset{\dot{}}{+}G\in K$$
28	27	3adant2	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to H\underset{\dot{}}{+}G\in K$$
29	28 17	ifcld	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=F,H\underset{\dot{}}{+}G,I\right)\in K$$
30	20 22 29	3jca	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to \left(H\in K\wedge G\in K\wedge if\left(a=F,H\underset{\dot{}}{+}G,I\right)\in K\right)$$
31	1 2 3 4 5 6 7 8 9 10 11 12 13 14 18 30	mdetunilem5	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,H\underset{\dot{}}{+}G,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)\right)$$
32	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 27 17	mdetunilem2	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,H\underset{\dot{}}{+}G,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)\right)=\underset{\dot{}}{0}$$
33	15	simp2d	$$⊢\psi \to F\in N$$
34	20 17	ifcld	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=E,H,I\right)\in K$$
35	20 22 34	3jca	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to \left(H\in K\wedge G\in K\wedge if\left(a=E,H,I\right)\in K\right)$$
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14 33 35	mdetunilem5	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,H,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,H,I\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)$$
37	15	simp3d	$$⊢\psi \to E\ne F$$
38	37	necomd	$$⊢\psi \to F\ne E$$
39	33 18 38	3jca	$$⊢\psi \to \left(F\in N\wedge E\in N\wedge F\ne E\right)$$
40	1 2 3 4 5 6 7 8 9 10 11 12 13 14 39 19 17	mdetunilem2	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,H,I\right)\right)\right)\right)=\underset{\dot{}}{0}$$
41	40	oveq1d	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,H,I\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)=\underset{\dot{}}{0}\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)$$
42	37	neneqd	$$⊢\psi \to \neg E=F$$
43		eqtr2	$$⊢\left(a=E\wedge a=F\right)\to E=F$$
44	42 43	nsyl	$$⊢\psi \to \neg \left(a=E\wedge a=F\right)$$
45	44	3ad2ant1	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to \neg \left(a=E\wedge a=F\right)$$
46		ifcomnan	$$⊢\neg \left(a=E\wedge a=F\right)\to if\left(a=E,H,if\left(a=F,G,I\right)\right)=if\left(a=F,G,if\left(a=E,H,I\right)\right)$$
47	45 46	syl	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=E,H,if\left(a=F,G,I\right)\right)=if\left(a=F,G,if\left(a=E,H,I\right)\right)$$
48	47	mpoeq3dva	$$⊢\psi \to \left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)=\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)$$
49	48	fveq2d	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)$$
50	14 10	syl	$$⊢\psi \to D:B⟶K$$
51	14 8	syl	$$⊢\psi \to N\in \mathrm{Fin}$$
52	22 17	ifcld	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=F,G,I\right)\in K$$
53	20 52	ifcld	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=E,H,if\left(a=F,G,I\right)\right)\in K$$
54	1 3 2 51 24 53	matbas2d	$$⊢\psi \to \left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\in B$$
55	50 54	ffvelcdmd	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\in K$$
56	49 55	eqeltrrd	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)\in K$$
57	3 6 4	grplid	$$⊢\left(R\in \mathrm{Grp}\wedge D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)\in K\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)$$
58	24 56 57	syl2anc	$$⊢\psi \to \underset{\dot{}}{0}\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)$$
59	36 41 58	3eqtrd	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,H,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,H,I\right)\right)\right)\right)$$
60		ifcomnan	$$⊢\neg \left(a=E\wedge a=F\right)\to if\left(a=E,H,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)=if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,H,I\right)\right)$$
61	45 60	syl	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=E,H,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)=if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,H,I\right)\right)$$
62	61	mpoeq3dva	$$⊢\psi \to \left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)=\left(a\in N,b\in N⟼if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,H,I\right)\right)\right)$$
63	62	fveq2d	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,H,I\right)\right)\right)\right)$$
64	59 63 49	3eqtr4d	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)$$
65	22 17	ifcld	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=E,G,I\right)\in K$$
66	20 22 65	3jca	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to \left(H\in K\wedge G\in K\wedge if\left(a=E,G,I\right)\in K\right)$$
67	1 2 3 4 5 6 7 8 9 10 11 12 13 14 33 66	mdetunilem5	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,G,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,G,I\right)\right)\right)\right)$$
68	1 2 3 4 5 6 7 8 9 10 11 12 13 14 39 21 17	mdetunilem2	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,G,I\right)\right)\right)\right)=\underset{\dot{}}{0}$$
69	68	oveq2d	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=F,G,if\left(a=E,G,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{0}$$
70		ifcomnan	$$⊢\neg \left(a=E\wedge a=F\right)\to if\left(a=E,G,if\left(a=F,H,I\right)\right)=if\left(a=F,H,if\left(a=E,G,I\right)\right)$$
71	45 70	syl	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=E,G,if\left(a=F,H,I\right)\right)=if\left(a=F,H,if\left(a=E,G,I\right)\right)$$
72	71	mpoeq3dva	$$⊢\psi \to \left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)=\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)$$
73	72	fveq2d	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)$$
74	20 17	ifcld	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=F,H,I\right)\in K$$
75	22 74	ifcld	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=E,G,if\left(a=F,H,I\right)\right)\in K$$
76	1 3 2 51 24 75	matbas2d	$$⊢\psi \to \left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\in B$$
77	50 76	ffvelcdmd	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)\in K$$
78	73 77	eqeltrrd	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)\in K$$
79	3 6 4	grprid	$$⊢\left(R\in \mathrm{Grp}\wedge D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)\in K\right)\to D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{0}=D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)$$
80	24 78 79	syl2anc	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{0}=D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)$$
81	67 69 80	3eqtrd	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,G,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,H,if\left(a=E,G,I\right)\right)\right)\right)$$
82		ifcomnan	$$⊢\neg \left(a=E\wedge a=F\right)\to if\left(a=E,G,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)=if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,G,I\right)\right)$$
83	45 82	syl	$$⊢\left(\psi \wedge a\in N\wedge b\in N\right)\to if\left(a=E,G,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)=if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,G,I\right)\right)$$
84	83	mpoeq3dva	$$⊢\psi \to \left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)=\left(a\in N,b\in N⟼if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,G,I\right)\right)\right)$$
85	84	fveq2d	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=F,H\underset{\dot{}}{+}G,if\left(a=E,G,I\right)\right)\right)\right)$$
86	81 85 73	3eqtr4d	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)$$
87	64 86	oveq12d	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H\underset{\dot{}}{+}G,I\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)$$
88	31 32 87	3eqtr3rd	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)=\underset{\dot{}}{0}$$
89		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
90	3 6 4 89	grpinvid1	$$⊢\left(R\in \mathrm{Grp}\wedge D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\in K\wedge D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)\in K\right)\to \left({inv}_g\left(R\right)\left(D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)\leftrightarrow D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)=\underset{\dot{}}{0}\right)$$
91	24 55 77 90	syl3anc	$$⊢\psi \to \left({inv}_g\left(R\right)\left(D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)\leftrightarrow D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)=\underset{\dot{}}{0}\right)$$
92	88 91	mpbird	$$⊢\psi \to {inv}_g\left(R\right)\left(D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\right)=D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)$$
93	92	eqcomd	$$⊢\psi \to D\left(\left(a\in N,b\in N⟼if\left(a=E,G,if\left(a=F,H,I\right)\right)\right)\right)={inv}_g\left(R\right)\left(D\left(\left(a\in N,b\in N⟼if\left(a=E,H,if\left(a=F,G,I\right)\right)\right)\right)\right)$$