Theorem matepmcl

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	|- A = ( N Mat R )
	matepmcl.b	|- B = ( Base ` A )
	matepmcl.p	|- P = ( Base ` ( SymGrp ` N ) )
Assertion	matepmcl	|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> A. n e. N ( ( Q ` n ) M n ) e. ( Base ` R ) )

Proof

Step	Hyp	Ref	Expression
1		matepmcl.a	|- A = ( N Mat R )
2		matepmcl.b	|- B = ( Base ` A )
3		matepmcl.p	|- P = ( Base ` ( SymGrp ` N ) )
4		eqid	|- ( SymGrp ` N ) = ( SymGrp ` N )
5	4 3	symgfv	|- ( ( Q e. P /\ n e. N ) -> ( Q ` n ) e. N )
6	5	3ad2antl2	|- ( ( ( R e. Ring /\ Q e. P /\ M e. B ) /\ n e. N ) -> ( Q ` n ) e. N )
7		simpr	|- ( ( ( R e. Ring /\ Q e. P /\ M e. B ) /\ n e. N ) -> n e. N )
8	2	eleq2i	|- ( M e. B <-> M e. ( Base ` A ) )
9	8	biimpi	|- ( M e. B -> M e. ( Base ` A ) )
10	9	3ad2ant3	|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> M e. ( Base ` A ) )
11	10	adantr	|- ( ( ( R e. Ring /\ Q e. P /\ M e. B ) /\ n e. N ) -> M e. ( Base ` A ) )
12		eqid	|- ( Base ` R ) = ( Base ` R )
13	1 12	matecl	|- ( ( ( Q ` n ) e. N /\ n e. N /\ M e. ( Base ` A ) ) -> ( ( Q ` n ) M n ) e. ( Base ` R ) )
14	6 7 11 13	syl3anc	|- ( ( ( R e. Ring /\ Q e. P /\ M e. B ) /\ n e. N ) -> ( ( Q ` n ) M n ) e. ( Base ` R ) )
15	14	ralrimiva	|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> A. n e. N ( ( Q ` n ) M n ) e. ( Base ` R ) )