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