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 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dpjlem.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion dpjlem ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) = ( 𝑆 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dpjlem.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
4 1 2 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
5 4 ffnd ⊢ ( 𝜑 → 𝑆 Fn 𝐼 )
6 fnressn ⊢ ( ( 𝑆 Fn 𝐼 ∧ 𝑋 ∈ 𝐼 ) → ( 𝑆 ↾ { 𝑋 } ) = { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } )
7 5 3 6 syl2anc ⊢ ( 𝜑 → ( 𝑆 ↾ { 𝑋 } ) = { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } )
8 7 oveq2d ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) = ( 𝐺 DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ) )
9 4 3 ffvelcdmd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) )
10 dprdsn ⊢ ( ( 𝑋 ∈ 𝐼 ∧ ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 dom DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ∧ ( 𝐺 DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ) = ( 𝑆 ‘ 𝑋 ) ) )
11 3 9 10 syl2anc ⊢ ( 𝜑 → ( 𝐺 dom DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ∧ ( 𝐺 DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ) = ( 𝑆 ‘ 𝑋 ) ) )
12 11 simprd ⊢ ( 𝜑 → ( 𝐺 DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ) = ( 𝑆 ‘ 𝑋 ) )
13 8 12 eqtrd ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) = ( 𝑆 ‘ 𝑋 ) )