Theorem zrhpsgnmhm

Description: Embedding of permutation signs into an arbitrary ring is a homomorphism. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Assertion	zrhpsgnmhm	$$⊢\left(R\in \mathrm{Ring}\wedge A\in \mathrm{Fin}\right)\to \mathrm{\mathbb{Z}RHom}\left(R\right)\circ \mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{MndHom}{\mathrm{mulGrp}}_R\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(R\right)=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
2	1	zrhrhm	$$⊢R\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(R\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
3		eqid	$$⊢{\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}={\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
4		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
5	3 4	rhmmhm	$$⊢\mathrm{\mathbb{Z}RHom}\left(R\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)\to \mathrm{\mathbb{Z}RHom}\left(R\right)\in \left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\mathrm{MndHom}{\mathrm{mulGrp}}_R\right)$$
6	2 5	syl	$$⊢R\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(R\right)\in \left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\mathrm{MndHom}{\mathrm{mulGrp}}_R\right)$$
7		eqid	$$⊢\mathrm{SymGrp}\left(A\right)=\mathrm{SymGrp}\left(A\right)$$
8		eqid	$$⊢\mathrm{pmSgn}\left(A\right)=\mathrm{pmSgn}\left(A\right)$$
9		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
10	7 8 9	psgnghm2	$$⊢A\in \mathrm{Fin}\to \mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)$$
11		ghmmhm	$$⊢\mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)\to \mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{MndHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)$$
12	10 11	syl	$$⊢A\in \mathrm{Fin}\to \mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{MndHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)$$
13		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
14	13	cnmsgnsubg	$$⊢\left\{1,-1\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
15		subgsubm	$$⊢\left\{1,-1\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)\to \left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
16	14 15	ax-mp	$$⊢\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
17		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
18		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
19		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
20		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
21	18 19 20	drngui	$$⊢ℂ\setminus \left\{0\right\}=\mathrm{Unit}\left({ℂ}_{\mathrm{fld}}\right)$$
22		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
23	21 22	unitsubm	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to ℂ\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
24	13	subsubm	$$⊢ℂ\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\to \left(\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)\leftrightarrow \left(\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left\{1,-1\right\}\subseteq ℂ\setminus \left\{0\right\}\right)\right)$$
25	17 23 24	mp2b	$$⊢\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)\leftrightarrow \left(\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left\{1,-1\right\}\subseteq ℂ\setminus \left\{0\right\}\right)$$
26	16 25	mpbi	$$⊢\left(\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left\{1,-1\right\}\subseteq ℂ\setminus \left\{0\right\}\right)$$
27	26	simpli	$$⊢\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
28		1z	$$⊢1\in \mathbb{Z}$$
29		neg1z	$$⊢-1\in \mathbb{Z}$$
30		prssi	$$⊢\left(1\in \mathbb{Z}\wedge -1\in \mathbb{Z}\right)\to \left\{1,-1\right\}\subseteq \mathbb{Z}$$
31	28 29 30	mp2an	$$⊢\left\{1,-1\right\}\subseteq \mathbb{Z}$$
32		zsubrg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
33	22	subrgsubm	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \mathbb{Z}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
34		zringmpg	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}={\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
35	34	eqcomi	$$⊢{\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
36	35	subsubm	$$⊢\mathbb{Z}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\to \left(\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\leftrightarrow \left(\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left\{1,-1\right\}\subseteq \mathbb{Z}\right)\right)$$
37	32 33 36	mp2b	$$⊢\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\leftrightarrow \left(\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left\{1,-1\right\}\subseteq \mathbb{Z}\right)$$
38	27 31 37	mpbir2an	$$⊢\left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)$$
39		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
40		ressabs	$$⊢\left(\mathbb{Z}\in \mathrm{V}\wedge \left\{1,-1\right\}\subseteq \mathbb{Z}\right)\to \left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right){\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
41	39 31 40	mp2an	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right){\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
42	34	oveq1i	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Z}\right){\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
43	41 42	eqtr3i	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
44	43	resmhm2	$$⊢\left(\mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{MndHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}\right)\right)\wedge \left\{1,-1\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\right)\to \mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{MndHom}{\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)$$
45	12 38 44	sylancl	$$⊢A\in \mathrm{Fin}\to \mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{MndHom}{\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)$$
46		mhmco	$$⊢\left(\mathrm{\mathbb{Z}RHom}\left(R\right)\in \left({\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\mathrm{MndHom}{\mathrm{mulGrp}}_R\right)\wedge \mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{MndHom}{\mathrm{mulGrp}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\right)\to \mathrm{\mathbb{Z}RHom}\left(R\right)\circ \mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{MndHom}{\mathrm{mulGrp}}_R\right)$$
47	6 45 46	syl2an	$$⊢\left(R\in \mathrm{Ring}\wedge A\in \mathrm{Fin}\right)\to \mathrm{\mathbb{Z}RHom}\left(R\right)\circ \mathrm{pmSgn}\left(A\right)\in \left(\mathrm{SymGrp}\left(A\right)\mathrm{MndHom}{\mathrm{mulGrp}}_R\right)$$