Theorem gsummatr01lem1

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

	Ref	Expression
Hypotheses	gsummatr01.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	gsummatr01.r	⊢ 𝑅 = { 𝑟 ∈ 𝑃 ∣ ( 𝑟 ‘ 𝐾 ) = 𝐿 }
Assertion	gsummatr01lem1	⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑋 ) ∈ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		gsummatr01.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		gsummatr01.r	⊢ 𝑅 = { 𝑟 ∈ 𝑃 ∣ ( 𝑟 ‘ 𝐾 ) = 𝐿 }
3		fveq1	⊢ ( 𝑟 = 𝑄 → ( 𝑟 ‘ 𝐾 ) = ( 𝑄 ‘ 𝐾 ) )
4	3	eqeq1d	⊢ ( 𝑟 = 𝑄 → ( ( 𝑟 ‘ 𝐾 ) = 𝐿 ↔ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
5	4 2	elrab2	⊢ ( 𝑄 ∈ 𝑅 ↔ ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
6	5	simplbi	⊢ ( 𝑄 ∈ 𝑅 → 𝑄 ∈ 𝑃 )
7		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
8	7 1	symgfv	⊢ ( ( 𝑄 ∈ 𝑃 ∧ 𝑋 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑋 ) ∈ 𝑁 )
9	6 8	sylan	⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑋 ) ∈ 𝑁 )