Metamath Proof Explorer


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 ) )