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{˙}{\cdot} = \cdot_{G}$
	Assertion	mulgfvi	$⊢ \underset{˙}{\cdot} = \cdot_{I (G)}$

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

Metamath Proof Explorer