Theorem imasgim

Description: A relabeling of the elements of a group induces an isomorphism to the relabeled group.MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015) (Revised by Mario Carneiro, 11-Aug-2015)

	Ref	Expression
Hypotheses	imasgim.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imasgim.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imasgim.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}B$$
	imasgim.r	$$⊢\phi \to R\in \mathrm{Grp}$$
Assertion	imasgim	$$⊢\phi \to F\in \left(R\mathrm{GrpIso}U\right)$$

Proof

Step	Hyp	Ref	Expression
1		imasgim.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
2		imasgim.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		imasgim.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}B$$
4		imasgim.r	$$⊢\phi \to R\in \mathrm{Grp}$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
7		eqid	$$⊢{+}_R={+}_R$$
8		eqid	$$⊢{+}_U={+}_U$$
9		eqidd	$$⊢\phi \to {+}_R={+}_R$$
10		f1ofo	$$⊢F:V\underset{1-1\; onto}{⟶}B\to F:V\underset{onto}{⟶}B$$
11	3 10	syl	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
12	3	f1ocpbl	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(c\in V\wedge d\in V\right)\right)\to \left(\left(F\left(a\right)=F\left(c\right)\wedge F\left(b\right)=F\left(d\right)\right)\to F\left(a{+}_{R}b\right)=F\left(c{+}_{R}d\right)\right)$$
13		eqid	$$⊢0_R=0_R$$
14	1 2 9 11 12 4 13	imasgrp	$$⊢\phi \to \left(U\in \mathrm{Grp}\wedge F\left(0_R\right)=0_U\right)$$
15	14	simpld	$$⊢\phi \to U\in \mathrm{Grp}$$
16	1 2 11 4	imasbas	$$⊢\phi \to B={\mathrm{Base}}_U$$
17		f1oeq3	$$⊢B={\mathrm{Base}}_U\to \left(F:V\underset{1-1\; onto}{⟶}B\leftrightarrow F:V\underset{1-1\; onto}{⟶}{\mathrm{Base}}_U\right)$$
18	16 17	syl	$$⊢\phi \to \left(F:V\underset{1-1\; onto}{⟶}B\leftrightarrow F:V\underset{1-1\; onto}{⟶}{\mathrm{Base}}_U\right)$$
19	3 18	mpbid	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}{\mathrm{Base}}_U$$
20	2	f1oeq2d	$$⊢\phi \to \left(F:V\underset{1-1\; onto}{⟶}{\mathrm{Base}}_U\leftrightarrow F:{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}{\mathrm{Base}}_U\right)$$
21	19 20	mpbid	$$⊢\phi \to F:{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}{\mathrm{Base}}_U$$
22		f1of	$$⊢F:{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}{\mathrm{Base}}_U\to F:{\mathrm{Base}}_R⟶{\mathrm{Base}}_U$$
23	21 22	syl	$$⊢\phi \to F:{\mathrm{Base}}_R⟶{\mathrm{Base}}_U$$
24	2	eleq2d	$$⊢\phi \to \left(a\in V\leftrightarrow a\in {\mathrm{Base}}_R\right)$$
25	2	eleq2d	$$⊢\phi \to \left(b\in V\leftrightarrow b\in {\mathrm{Base}}_R\right)$$
26	24 25	anbi12d	$$⊢\phi \to \left(\left(a\in V\wedge b\in V\right)\leftrightarrow \left(a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_R\right)\right)$$
27	11 12 1 2 4 7 8	imasaddval	$$⊢\left(\phi \wedge a\in V\wedge b\in V\right)\to F\left(a\right){+}_{U}F\left(b\right)=F\left(a{+}_{R}b\right)$$
28	27	eqcomd	$$⊢\left(\phi \wedge a\in V\wedge b\in V\right)\to F\left(a{+}_{R}b\right)=F\left(a\right){+}_{U}F\left(b\right)$$
29	28	3expib	$$⊢\phi \to \left(\left(a\in V\wedge b\in V\right)\to F\left(a{+}_{R}b\right)=F\left(a\right){+}_{U}F\left(b\right)\right)$$
30	26 29	sylbird	$$⊢\phi \to \left(\left(a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_R\right)\to F\left(a{+}_{R}b\right)=F\left(a\right){+}_{U}F\left(b\right)\right)$$
31	30	imp	$$⊢\left(\phi \wedge \left(a\in {\mathrm{Base}}_R\wedge b\in {\mathrm{Base}}_R\right)\right)\to F\left(a{+}_{R}b\right)=F\left(a\right){+}_{U}F\left(b\right)$$
32	5 6 7 8 4 15 23 31	isghmd	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}U\right)$$
33	5 6	isgim	$$⊢F\in \left(R\mathrm{GrpIso}U\right)\leftrightarrow \left(F\in \left(R\mathrm{GrpHom}U\right)\wedge F:{\mathrm{Base}}_R\underset{1-1\; onto}{⟶}{\mathrm{Base}}_U\right)$$
34	32 21 33	sylanbrc	$$⊢\phi \to F\in \left(R\mathrm{GrpIso}U\right)$$