This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmd 
 |-  ( 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 ) )