Theorem matepm2cl

Description: Each entry of a matrix with an index as permutation of the other is an element of the underlying ring. (Contributed by AV, 1-Jan-2019)

	Ref	Expression
Hypotheses	matepmcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matepmcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	matepmcl.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
Assertion	matepm2cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		matepmcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matepmcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		matepmcl.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
4		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ 𝑁 ) → 𝑛 ∈ 𝑁 )
5		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
6	5 3	symgfv	⊢ ( ( 𝑄 ∈ 𝑃 ∧ 𝑛 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 )
7	6	3ad2antl2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 )
8	2	eleq2i	⊢ ( 𝑀 ∈ 𝐵 ↔ 𝑀 ∈ ( Base ‘ 𝐴 ) )
9	8	biimpi	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
10	9	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
11	10	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
12		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13	1 12	matecl	⊢ ( ( 𝑛 ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑅 ) )
14	4 7 11 13	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ 𝑁 ) → ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑅 ) )
15	14	ralrimiva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑅 ) )