Metamath Proof Explorer

Theorem scmatmats

Description: The set of an N x N scalar matrices over the ring R expressed as a subset of N x N matrices over the ring R with certain properties for their entries. (Contributed by AV, 31-Oct-2019) (Revised by AV, 19-Dec-2019)

Ref Expression
Hypotheses scmatmat.a ⊢A=NMatR
scmatmat.b ⊢B=BaseA
scmatmat.s ⊢S=NScMatR
scmate.k ⊢K=BaseR
scmate.0 ⊢0˙=0R
Assertion scmatmats ⊢N∈Fin∧R∈Ring→S=m∈B|∃c∈K∀i∈N∀j∈Nimj=ifi=jc0˙

Proof

Step Hyp Ref Expression
1 scmatmat.a ⊢A=NMatR
2 scmatmat.b ⊢B=BaseA
3 scmatmat.s ⊢S=NScMatR
4 scmate.k ⊢K=BaseR
5 scmate.0 ⊢0˙=0R
6 eqid ⊢1A=1A
7 eqid ⊢⋅A=⋅A
8 4 1 2 6 7 3 scmatval ⊢N∈Fin∧R∈Ring→S=m∈B|∃c∈Km=c⋅A1A
9 simpr ⊢N∈Fin∧R∈Ring∧m∈B→m∈B
10 9 adantr ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→m∈B
11 simpll ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→N∈Fin∧R∈Ring
12 1 matring ⊢N∈Fin∧R∈Ring→A∈Ring
13 2 6 ringidcl ⊢A∈Ring→1A∈B
14 12 13 syl ⊢N∈Fin∧R∈Ring→1A∈B
15 14 adantr ⊢N∈Fin∧R∈Ring∧m∈B→1A∈B
16 15 anim1ci ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→c∈K∧1A∈B
17 4 1 2 7 matvscl ⊢N∈Fin∧R∈Ring∧c∈K∧1A∈B→c⋅A1A∈B
18 11 16 17 syl2anc ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→c⋅A1A∈B
19 1 2 eqmat ⊢m∈B∧c⋅A1A∈B→m=c⋅A1A↔∀i∈N∀j∈Nimj=ic⋅A1Aj
20 10 18 19 syl2anc ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→m=c⋅A1A↔∀i∈N∀j∈Nimj=ic⋅A1Aj
21 simplll ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→N∈Fin
22 simpllr ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→R∈Ring
23 simpr ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→c∈K
24 21 22 23 3jca ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→N∈Fin∧R∈Ring∧c∈K
25 1 4 5 6 7 scmatscmide ⊢N∈Fin∧R∈Ring∧c∈K∧i∈N∧j∈N→ic⋅A1Aj=ifi=jc0˙
26 24 25 sylan ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K∧i∈N∧j∈N→ic⋅A1Aj=ifi=jc0˙
27 26 eqeq2d ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K∧i∈N∧j∈N→imj=ic⋅A1Aj↔imj=ifi=jc0˙
28 27 2ralbidva ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→∀i∈N∀j∈Nimj=ic⋅A1Aj↔∀i∈N∀j∈Nimj=ifi=jc0˙
29 20 28 bitrd ⊢N∈Fin∧R∈Ring∧m∈B∧c∈K→m=c⋅A1A↔∀i∈N∀j∈Nimj=ifi=jc0˙
30 29 rexbidva ⊢N∈Fin∧R∈Ring∧m∈B→∃c∈Km=c⋅A1A↔∃c∈K∀i∈N∀j∈Nimj=ifi=jc0˙
31 30 rabbidva ⊢N∈Fin∧R∈Ring→m∈B|∃c∈Km=c⋅A1A=m∈B|∃c∈K∀i∈N∀j∈Nimj=ifi=jc0˙
32 8 31 eqtrd ⊢N∈Fin∧R∈Ring→S=m∈B|∃c∈K∀i∈N∀j∈Nimj=ifi=jc0˙