This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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