Theorem dprd0

Description: The empty family is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypothesis	dprd0.0	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	dprd0	$$⊢G\in \mathrm{Grp}\to \left(G\mathrm{dom}\mathrm{DProd}\varnothing \wedge G\mathrm{DProd}\varnothing =\left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dprd0.0	$$⊢\underset{\dot{}}{0}=0_G$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	1	dprdz	$$⊢\left(G\in \mathrm{Grp}\wedge \varnothing \in \mathrm{V}\right)\to \left(G\mathrm{dom}\mathrm{DProd}\left(x\in \varnothing ⟼\left\{\underset{\dot{}}{0}\right\}\right)\wedge G\mathrm{DProd}\left(x\in \varnothing ⟼\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
4	2 3	mpan2	$$⊢G\in \mathrm{Grp}\to \left(G\mathrm{dom}\mathrm{DProd}\left(x\in \varnothing ⟼\left\{\underset{\dot{}}{0}\right\}\right)\wedge G\mathrm{DProd}\left(x\in \varnothing ⟼\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
5		mpt0	$$⊢\left(x\in \varnothing ⟼\left\{\underset{\dot{}}{0}\right\}\right)=\varnothing$$
6	5	breq2i	$$⊢G\mathrm{dom}\mathrm{DProd}\left(x\in \varnothing ⟼\left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow G\mathrm{dom}\mathrm{DProd}\varnothing$$
7	5	oveq2i	$$⊢G\mathrm{DProd}\left(x\in \varnothing ⟼\left\{\underset{\dot{}}{0}\right\}\right)=G\mathrm{DProd}\varnothing$$
8	7	eqeq1i	$$⊢G\mathrm{DProd}\left(x\in \varnothing ⟼\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow G\mathrm{DProd}\varnothing =\left\{\underset{\dot{}}{0}\right\}$$
9	6 8	anbi12i	$$⊢\left(G\mathrm{dom}\mathrm{DProd}\left(x\in \varnothing ⟼\left\{\underset{\dot{}}{0}\right\}\right)\wedge G\mathrm{DProd}\left(x\in \varnothing ⟼\left\{\underset{\dot{}}{0}\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(G\mathrm{dom}\mathrm{DProd}\varnothing \wedge G\mathrm{DProd}\varnothing =\left\{\underset{\dot{}}{0}\right\}\right)$$
10	4 9	sylib	$$⊢G\in \mathrm{Grp}\to \left(G\mathrm{dom}\mathrm{DProd}\varnothing \wedge G\mathrm{DProd}\varnothing =\left\{\underset{\dot{}}{0}\right\}\right)$$