Theorem gsummatr01lem2

Description: Lemma B 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	gsummatr01lem2	|- ( ( Q e. R /\ X e. N ) -> ( A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) -> ( X A ( Q ` X ) ) e. ( Base ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummatr01.p	|- P = ( Base ` ( SymGrp ` N ) )
2		gsummatr01.r	|- R = { r e. P | ( r ` K ) = L }
3		simpr	|- ( ( Q e. R /\ X e. N ) -> X e. N )
4	1 2	gsummatr01lem1	|- ( ( Q e. R /\ X e. N ) -> ( Q ` X ) e. N )
5	3 4	jca	|- ( ( Q e. R /\ X e. N ) -> ( X e. N /\ ( Q ` X ) e. N ) )
6		ovrspc2v	|- ( ( ( X e. N /\ ( Q ` X ) e. N ) /\ A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) ) -> ( X A ( Q ` X ) ) e. ( Base ` G ) )
7	5 6	sylan	|- ( ( ( Q e. R /\ X e. N ) /\ A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) ) -> ( X A ( Q ` X ) ) e. ( Base ` G ) )
8	7	ex	|- ( ( Q e. R /\ X e. N ) -> ( A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) -> ( X A ( Q ` X ) ) e. ( Base ` G ) ) )