Theorem dpjlem

Description: Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dpjfval.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	dpjfval.2	$$⊢\phi \to \mathrm{dom}S=I$$
	dpjlem.3	$$⊢\phi \to X\in I$$
Assertion	dpjlem	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)=S\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
2		dpjfval.2	$$⊢\phi \to \mathrm{dom}S=I$$
3		dpjlem.3	$$⊢\phi \to X\in I$$
4	1 2	dprdf2	$$⊢\phi \to S:I⟶\mathrm{SubGrp}\left(G\right)$$
5	4	ffnd	$$⊢\phi \to SFnI$$
6		fnressn	$$⊢\left(SFnI\wedge X\in I\right)\to {S\upharpoonright }_{\left\{X\right\}}=\left\{⟨X,S\left(X\right)⟩\right\}$$
7	5 3 6	syl2anc	$$⊢\phi \to {S\upharpoonright }_{\left\{X\right\}}=\left\{⟨X,S\left(X\right)⟩\right\}$$
8	7	oveq2d	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)=G\mathrm{DProd}\left\{⟨X,S\left(X\right)⟩\right\}$$
9	4 3	ffvelcdmd	$$⊢\phi \to S\left(X\right)\in \mathrm{SubGrp}\left(G\right)$$
10		dprdsn	$$⊢\left(X\in I\wedge S\left(X\right)\in \mathrm{SubGrp}\left(G\right)\right)\to \left(G\mathrm{dom}\mathrm{DProd}\left\{⟨X,S\left(X\right)⟩\right\}\wedge G\mathrm{DProd}\left\{⟨X,S\left(X\right)⟩\right\}=S\left(X\right)\right)$$
11	3 9 10	syl2anc	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}\left\{⟨X,S\left(X\right)⟩\right\}\wedge G\mathrm{DProd}\left\{⟨X,S\left(X\right)⟩\right\}=S\left(X\right)\right)$$
12	11	simprd	$$⊢\phi \to G\mathrm{DProd}\left\{⟨X,S\left(X\right)⟩\right\}=S\left(X\right)$$
13	8 12	eqtrd	$$⊢\phi \to G\mathrm{DProd}\left({S\upharpoonright }_{\left\{X\right\}}\right)=S\left(X\right)$$