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 ∈ Ring ∧ Q ∈ P ∧ M ∈ B → ∀ n ∈ N n M Q ⁡ n ∈ 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 ∈ Ring ∧ Q ∈ P ∧ M ∈ B ∧ n ∈ N → n ∈ N
5 eqid ⊢ SymGrp ⁡ N = SymGrp ⁡ N
6 5 3 symgfv ⊢ Q ∈ P ∧ n ∈ N → Q ⁡ n ∈ N
7 6 3ad2antl2 ⊢ R ∈ Ring ∧ Q ∈ P ∧ M ∈ B ∧ n ∈ N → Q ⁡ n ∈ N
8 2 eleq2i ⊢ M ∈ B ↔ M ∈ Base A
9 8 biimpi ⊢ M ∈ B → M ∈ Base A
10 9 3ad2ant3 ⊢ R ∈ Ring ∧ Q ∈ P ∧ M ∈ B → M ∈ Base A
11 10 adantr ⊢ R ∈ Ring ∧ Q ∈ P ∧ M ∈ B ∧ n ∈ N → M ∈ Base A
12 eqid ⊢ Base R = Base R
13 1 12 matecl ⊢ n ∈ N ∧ Q ⁡ n ∈ N ∧ M ∈ Base A → n M Q ⁡ n ∈ Base R
14 4 7 11 13 syl3anc ⊢ R ∈ Ring ∧ Q ∈ P ∧ M ∈ B ∧ n ∈ N → n M Q ⁡ n ∈ Base R
15 14 ralrimiva ⊢ R ∈ Ring ∧ Q ∈ P ∧ M ∈ B → ∀ n ∈ N n M Q ⁡ n ∈ Base R