Theorem mulgfvi

Description: The group multiple operation is compatible with identity-function protection. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Hypothesis	mulgfvi.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	mulgfvi	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{I}\left(G\right)}$$

Proof

Step	Hyp	Ref	Expression
1		mulgfvi.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
2		fvi	$$⊢G\in \mathrm{V}\to \mathrm{I}\left(G\right)=G$$
3	2	eqcomd	$$⊢G\in \mathrm{V}\to G=\mathrm{I}\left(G\right)$$
4	3	fveq2d	$$⊢G\in \mathrm{V}\to {\cdot }_G={\cdot }_{\mathrm{I}\left(G\right)}$$
5		fvprc	$$⊢\neg G\in \mathrm{V}\to {\cdot }_G=\varnothing$$
6		fvprc	$$⊢\neg G\in \mathrm{V}\to \mathrm{I}\left(G\right)=\varnothing$$
7	6	fveq2d	$$⊢\neg G\in \mathrm{V}\to {\cdot }_{\mathrm{I}\left(G\right)}={\cdot }_{\varnothing }$$
8		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
9		eqid	$$⊢{\cdot }_{\varnothing }={\cdot }_{\varnothing }$$
10	8 9	mulgfn	$$⊢{\cdot }_{\varnothing }Fn\left(\mathbb{Z}\times \varnothing \right)$$
11		xp0	$$⊢\mathbb{Z}\times \varnothing =\varnothing$$
12	11	fneq2i	$$⊢{\cdot }_{\varnothing }Fn\left(\mathbb{Z}\times \varnothing \right)\leftrightarrow {\cdot }_{\varnothing }Fn\varnothing$$
13	10 12	mpbi	$$⊢{\cdot }_{\varnothing }Fn\varnothing$$
14		fn0	$$⊢{\cdot }_{\varnothing }Fn\varnothing \leftrightarrow {\cdot }_{\varnothing }=\varnothing$$
15	13 14	mpbi	$$⊢{\cdot }_{\varnothing }=\varnothing$$
16	7 15	eqtrdi	$$⊢\neg G\in \mathrm{V}\to {\cdot }_{\mathrm{I}\left(G\right)}=\varnothing$$
17	5 16	eqtr4d	$$⊢\neg G\in \mathrm{V}\to {\cdot }_G={\cdot }_{\mathrm{I}\left(G\right)}$$
18	4 17	pm2.61i	$$⊢{\cdot }_G={\cdot }_{\mathrm{I}\left(G\right)}$$
19	1 18	eqtri	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{I}\left(G\right)}$$