Theorem gsummatr01lem2

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

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

Proof

Step	Hyp	Ref	Expression
1		gsummatr01.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		gsummatr01.r	⊢ 𝑅 = { 𝑟 ∈ 𝑃 ∣ ( 𝑟 ‘ 𝐾 ) = 𝐿 }
3		simpr	⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁 ) → 𝑋 ∈ 𝑁 )
4	1 2	gsummatr01lem1	⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑋 ) ∈ 𝑁 )
5	3 4	jca	⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁 ) → ( 𝑋 ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑋 ) ∈ 𝑁 ) )
6		ovrspc2v	⊢ ( ( ( 𝑋 ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝑋 𝐴 ( 𝑄 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐺 ) )
7	5 6	sylan	⊢ ( ( ( 𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝑋 𝐴 ( 𝑄 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐺 ) )
8	7	ex	⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) → ( 𝑋 𝐴 ( 𝑄 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐺 ) ) )