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 ⊢ 𝐴 = ( 𝑁 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 ‘ 𝑅 ) )