Theorem isgrpinv

Description: Properties showing that a function M is the inverse function of a group. (Contributed by NM, 7-Aug-2013) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	grpinv.b	$$⊢B={\mathrm{Base}}_G$$
	grpinv.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpinv.u	$$⊢\underset{\dot{}}{0}=0_G$$
	grpinv.n	$$⊢N={inv}_g\left(G\right)$$
Assertion	isgrpinv	$$⊢G\in \mathrm{Grp}\to \left(\left(M:B⟶B\wedge \forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\leftrightarrow N=M\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpinv.b	$$⊢B={\mathrm{Base}}_G$$
2		grpinv.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpinv.u	$$⊢\underset{\dot{}}{0}=0_G$$
4		grpinv.n	$$⊢N={inv}_g\left(G\right)$$
5	1 2 3 4	grpinvval	$$⊢x\in B\to N\left(x\right)=\left(\iota e\in B|e\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
6	5	ad2antlr	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\wedge x\in B\right)\wedge M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to N\left(x\right)=\left(\iota e\in B|e\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
7		simpr	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\wedge x\in B\right)\wedge M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
8		simpllr	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\wedge x\in B\right)\wedge M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to M:B⟶B$$
9		simplr	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\wedge x\in B\right)\wedge M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to x\in B$$
10	8 9	ffvelrnd	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\wedge x\in B\right)\wedge M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to M\left(x\right)\in B$$
11	1 2 3	grpinveu	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to \exists !e\in Be\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
12	11	ad4ant13	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\wedge x\in B\right)\wedge M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to \exists !e\in Be\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
13		oveq1	$$⊢e=M\left(x\right)\to e\underset{\dot{}}{+}x=M\left(x\right)\underset{\dot{}}{+}x$$
14	13	eqeq1d	$$⊢e=M\left(x\right)\to \left(e\underset{\dot{}}{+}x=\underset{\dot{}}{0}\leftrightarrow M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
15	14	riota2	$$⊢\left(M\left(x\right)\in B\wedge \exists !e\in Be\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to \left(M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\leftrightarrow \left(\iota e\in B|e\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)=M\left(x\right)\right)$$
16	10 12 15	syl2anc	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\wedge x\in B\right)\wedge M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to \left(M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\leftrightarrow \left(\iota e\in B|e\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)=M\left(x\right)\right)$$
17	7 16	mpbid	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\wedge x\in B\right)\wedge M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to \left(\iota e\in B|e\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)=M\left(x\right)$$
18	6 17	eqtrd	$$⊢\left(\left(\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\wedge x\in B\right)\wedge M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to N\left(x\right)=M\left(x\right)$$
19	18	ex	$$⊢\left(\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\wedge x\in B\right)\to \left(M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\to N\left(x\right)=M\left(x\right)\right)$$
20	19	ralimdva	$$⊢\left(G\in \mathrm{Grp}\wedge M:B⟶B\right)\to \left(\forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\to \forall x\in BN\left(x\right)=M\left(x\right)\right)$$
21	20	impr	$$⊢\left(G\in \mathrm{Grp}\wedge \left(M:B⟶B\wedge \forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)\to \forall x\in BN\left(x\right)=M\left(x\right)$$
22	1 4	grpinvfn	$$⊢NFnB$$
23		ffn	$$⊢M:B⟶B\to MFnB$$
24	23	ad2antrl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(M:B⟶B\wedge \forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)\to MFnB$$
25		eqfnfv	$$⊢\left(NFnB\wedge MFnB\right)\to \left(N=M\leftrightarrow \forall x\in BN\left(x\right)=M\left(x\right)\right)$$
26	22 24 25	sylancr	$$⊢\left(G\in \mathrm{Grp}\wedge \left(M:B⟶B\wedge \forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)\to \left(N=M\leftrightarrow \forall x\in BN\left(x\right)=M\left(x\right)\right)$$
27	21 26	mpbird	$$⊢\left(G\in \mathrm{Grp}\wedge \left(M:B⟶B\wedge \forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)\to N=M$$
28	27	ex	$$⊢G\in \mathrm{Grp}\to \left(\left(M:B⟶B\wedge \forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\to N=M\right)$$
29	1 4	grpinvf	$$⊢G\in \mathrm{Grp}\to N:B⟶B$$
30	1 2 3 4	grplinv	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to N\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
31	30	ralrimiva	$$⊢G\in \mathrm{Grp}\to \forall x\in BN\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
32	29 31	jca	$$⊢G\in \mathrm{Grp}\to \left(N:B⟶B\wedge \forall x\in BN\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
33		feq1	$$⊢N=M\to \left(N:B⟶B\leftrightarrow M:B⟶B\right)$$
34		fveq1	$$⊢N=M\to N\left(x\right)=M\left(x\right)$$
35	34	oveq1d	$$⊢N=M\to N\left(x\right)\underset{\dot{}}{+}x=M\left(x\right)\underset{\dot{}}{+}x$$
36	35	eqeq1d	$$⊢N=M\to \left(N\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\leftrightarrow M\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
37	36	ralbidv	$$⊢N=M\to \left(\forall x\in BN\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\leftrightarrow \forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)$$
38	33 37	anbi12d	$$⊢N=M\to \left(\left(N:B⟶B\wedge \forall x\in BN\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\leftrightarrow \left(M:B⟶B\wedge \forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
39	32 38	syl5ibcom	$$⊢G\in \mathrm{Grp}\to \left(N=M\to \left(M:B⟶B\wedge \forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\right)$$
40	28 39	impbid	$$⊢G\in \mathrm{Grp}\to \left(\left(M:B⟶B\wedge \forall x\in BM\left(x\right)\underset{\dot{}}{+}x=\underset{\dot{}}{0}\right)\leftrightarrow N=M\right)$$