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	ffvelrnd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) )
10		dprdsn	⊢ ( ( 𝑋 ∈ 𝐼 ∧ ( 𝑆 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 dom DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ∧ ( 𝐺 DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ) = ( 𝑆 ‘ 𝑋 ) ) )
11	3 9 10	syl2anc	⊢ ( 𝜑 → ( 𝐺 dom DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ∧ ( 𝐺 DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ) = ( 𝑆 ‘ 𝑋 ) ) )
12	11	simprd	⊢ ( 𝜑 → ( 𝐺 DProd { ⟨ 𝑋 , ( 𝑆 ‘ 𝑋 ) ⟩ } ) = ( 𝑆 ‘ 𝑋 ) )
13	8 12	eqtrd	⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) = ( 𝑆 ‘ 𝑋 ) )