Theorem gsummatr01lem1

Description: Lemma A for gsummatr01 . (Contributed by AV, 8-Jan-2019)

	Ref	Expression
Hypotheses	gsummatr01.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
	gsummatr01.r	$$⊢R=\left\{r\in P|r\left(K\right)=L\right\}$$
Assertion	gsummatr01lem1	$$⊢\left(Q\in R\wedge X\in N\right)\to Q\left(X\right)\in N$$

Proof

Step	Hyp	Ref	Expression
1		gsummatr01.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
2		gsummatr01.r	$$⊢R=\left\{r\in P|r\left(K\right)=L\right\}$$
3		fveq1	$$⊢r=Q\to r\left(K\right)=Q\left(K\right)$$
4	3	eqeq1d	$$⊢r=Q\to \left(r\left(K\right)=L\leftrightarrow Q\left(K\right)=L\right)$$
5	4 2	elrab2	$$⊢Q\in R\leftrightarrow \left(Q\in P\wedge Q\left(K\right)=L\right)$$
6	5	simplbi	$$⊢Q\in R\to Q\in P$$
7		eqid	$$⊢\mathrm{SymGrp}\left(N\right)=\mathrm{SymGrp}\left(N\right)$$
8	7 1	symgfv	$$⊢\left(Q\in P\wedge X\in N\right)\to Q\left(X\right)\in N$$
9	6 8	sylan	$$⊢\left(Q\in R\wedge X\in N\right)\to Q\left(X\right)\in N$$