gsummatr01lem2

	Ref	Expression
Hypotheses	gsummatr01.p	$⊢ P = {Base}_{SymGrp (N)}$
	gsummatr01.r	$⊢ R = \{r \in P \| r (K) = L\}$
Assertion	gsummatr01lem2	$⊢ (Q \in R \land X \in N) \to (\forall i \in N \forall j \in N i A j \in {Base}_{G} \to X A Q (X) \in {Base}_{G})$

Step	Hyp	Ref	Expression
1		gsummatr01.p	$⊢ P = {Base}_{SymGrp (N)}$
2		gsummatr01.r	$⊢ R = \{r \in P \| r (K) = L\}$
3		simpr	$⊢ (Q \in R \land X \in N) \to X \in N$
4	1 2	gsummatr01lem1	$⊢ (Q \in R \land X \in N) \to Q (X) \in N$
5	3 4	jca	$⊢ (Q \in R \land X \in N) \to (X \in N \land Q (X) \in N)$
6		ovrspc2v	$⊢ ((X \in N \land Q (X) \in N) \land \forall i \in N \forall j \in N i A j \in {Base}_{G}) \to X A Q (X) \in {Base}_{G}$
7	5 6	sylan	$⊢ ((Q \in R \land X \in N) \land \forall i \in N \forall j \in N i A j \in {Base}_{G}) \to X A Q (X) \in {Base}_{G}$
8	7	ex	$⊢ (Q \in R \land X \in N) \to (\forall i \in N \forall j \in N i A j \in {Base}_{G} \to X A Q (X) \in {Base}_{G})$

Metamath Proof Explorer