Theorem gsummatr01lem1

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

	Ref	Expression
Hypotheses	gsummatr01.p	|- P = ( Base ` ( SymGrp ` N ) )
	gsummatr01.r	|- R = { r e. P | ( r ` K ) = L }
Assertion	gsummatr01lem1	|- ( ( Q e. R /\ X e. N ) -> ( Q ` X ) e. N )

Proof

Step	Hyp	Ref	Expression
1		gsummatr01.p	|- P = ( Base ` ( SymGrp ` N ) )
2		gsummatr01.r	|- R = { r e. P | ( r ` K ) = L }
3		fveq1	|- ( r = Q -> ( r ` K ) = ( Q ` K ) )
4	3	eqeq1d	|- ( r = Q -> ( ( r ` K ) = L <-> ( Q ` K ) = L ) )
5	4 2	elrab2	|- ( Q e. R <-> ( Q e. P /\ ( Q ` K ) = L ) )
6	5	simplbi	|- ( Q e. R -> Q e. P )
7		eqid	|- ( SymGrp ` N ) = ( SymGrp ` N )
8	7 1	symgfv	|- ( ( Q e. P /\ X e. N ) -> ( Q ` X ) e. N )
9	6 8	sylan	|- ( ( Q e. R /\ X e. N ) -> ( Q ` X ) e. N )