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	|- A = ( N Mat R )
	matepmcl.b	|- B = ( Base ` A )
	matepmcl.p	|- P = ( Base ` ( SymGrp ` N ) )
Assertion	matepm2cl	|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> A. n e. N ( n M ( Q ` 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		simpr	|- ( ( ( R e. Ring /\ Q e. P /\ M e. B ) /\ n e. N ) -> n e. N )
5		eqid	|- ( SymGrp ` N ) = ( SymGrp ` N )
6	5 3	symgfv	|- ( ( Q e. P /\ n e. N ) -> ( Q ` n ) e. N )
7	6	3ad2antl2	|- ( ( ( R e. Ring /\ Q e. P /\ M e. B ) /\ n e. N ) -> ( Q ` 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	|- ( ( n e. N /\ ( Q ` n ) e. N /\ M e. ( Base ` A ) ) -> ( n M ( Q ` n ) ) e. ( Base ` R ) )
14	4 7 11 13	syl3anc	|- ( ( ( R e. Ring /\ Q e. P /\ M e. B ) /\ n e. N ) -> ( n M ( Q ` n ) ) e. ( Base ` R ) )
15	14	ralrimiva	|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> A. n e. N ( n M ( Q ` n ) ) e. ( Base ` R ) )