dpjlem

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

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

Metamath Proof Explorer