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 𝐴 = ( 𝑁 Mat 𝑅 )
matepmcl.b 𝐵 = ( Base ‘ 𝐴 )
matepmcl.p 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
Assertion matepmcl ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃𝑀𝐵 ) → ∀ 𝑛𝑁 ( ( 𝑄𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 matepmcl.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 matepmcl.b 𝐵 = ( Base ‘ 𝐴 )
3 matepmcl.p 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
4 eqid ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
5 4 3 symgfv ( ( 𝑄𝑃𝑛𝑁 ) → ( 𝑄𝑛 ) ∈ 𝑁 )
6 5 3ad2antl2 ( ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃𝑀𝐵 ) ∧ 𝑛𝑁 ) → ( 𝑄𝑛 ) ∈ 𝑁 )
7 simpr ( ( ( 𝑅 ∈ 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 6 7 11 13 syl3anc ( ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃𝑀𝐵 ) ∧ 𝑛𝑁 ) → ( ( 𝑄𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
15 14 ralrimiva ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃𝑀𝐵 ) → ∀ 𝑛𝑁 ( ( 𝑄𝑛 ) 𝑀 𝑛 ) ∈ ( Base ‘ 𝑅 ) )