Theorem dpjlem

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

	Ref	Expression
Hypotheses	dpjfval.1	|- ( ph -> G dom DProd S )
	dpjfval.2	|- ( ph -> dom S = I )
	dpjlem.3	|- ( ph -> X e. I )
Assertion	dpjlem	|- ( ph -> ( G DProd ( S |` { X } ) ) = ( S ` X ) )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	|- ( ph -> G dom DProd S )
2		dpjfval.2	|- ( ph -> dom S = I )
3		dpjlem.3	|- ( ph -> X e. I )
4	1 2	dprdf2	|- ( ph -> S : I --> ( SubGrp ` G ) )
5	4	ffnd	|- ( ph -> S Fn I )
6		fnressn	|- ( ( S Fn I /\ X e. I ) -> ( S |` { X } ) = { <. X , ( S ` X ) >. } )
7	5 3 6	syl2anc	|- ( ph -> ( S |` { X } ) = { <. X , ( S ` X ) >. } )
8	7	oveq2d	|- ( ph -> ( G DProd ( S |` { X } ) ) = ( G DProd { <. X , ( S ` X ) >. } ) )
9	4 3	ffvelrnd	|- ( ph -> ( S ` X ) e. ( SubGrp ` G ) )
10		dprdsn	|- ( ( X e. I /\ ( S ` X ) e. ( SubGrp ` G ) ) -> ( G dom DProd { <. X , ( S ` X ) >. } /\ ( G DProd { <. X , ( S ` X ) >. } ) = ( S ` X ) ) )
11	3 9 10	syl2anc	|- ( ph -> ( G dom DProd { <. X , ( S ` X ) >. } /\ ( G DProd { <. X , ( S ` X ) >. } ) = ( S ` X ) ) )
12	11	simprd	|- ( ph -> ( G DProd { <. X , ( S ` X ) >. } ) = ( S ` X ) )
13	8 12	eqtrd	|- ( ph -> ( G DProd ( S |` { X } ) ) = ( S ` X ) )