Metamath Proof Explorer

Theorem scmatid

Description: The identity matrix is a scalar matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 18-Dec-2019)

Ref Expression
Hypotheses scmatid.a ⊢A=NMatR
scmatid.b ⊢B=BaseA
scmatid.e ⊢E=BaseR
scmatid.0 ⊢0˙=0R
scmatid.s ⊢S=NScMatR
Assertion scmatid ⊢N∈Fin∧R∈Ring→1A∈S

Proof

Step Hyp Ref Expression
1 scmatid.a ⊢A=NMatR
2 scmatid.b ⊢B=BaseA
3 scmatid.e ⊢E=BaseR
4 scmatid.0 ⊢0˙=0R
5 scmatid.s ⊢S=NScMatR
6 1 matring ⊢N∈Fin∧R∈Ring→A∈Ring
7 eqid ⊢1A=1A
8 2 7 ringidcl ⊢A∈Ring→1A∈B
9 6 8 syl ⊢N∈Fin∧R∈Ring→1A∈B
10 1 matsca2 ⊢N∈Fin∧R∈Ring→R=Scalar⁡A
11 10 eqcomd ⊢N∈Fin∧R∈Ring→Scalar⁡A=R
12 11 fveq2d ⊢N∈Fin∧R∈Ring→1Scalar⁡A=1R
13 eqid ⊢BaseR=BaseR
14 eqid ⊢1R=1R
15 13 14 ringidcl ⊢R∈Ring→1R∈BaseR
16 15 adantl ⊢N∈Fin∧R∈Ring→1R∈BaseR
17 12 16 eqeltrd ⊢N∈Fin∧R∈Ring→1Scalar⁡A∈BaseR
18 oveq1 ⊢c=1Scalar⁡A→c⋅A1A=1Scalar⁡A⋅A1A
19 18 eqeq2d ⊢c=1Scalar⁡A→1A=c⋅A1A↔1A=1Scalar⁡A⋅A1A
20 19 adantl ⊢N∈Fin∧R∈Ring∧c=1Scalar⁡A→1A=c⋅A1A↔1A=1Scalar⁡A⋅A1A
21 1 matlmod ⊢N∈Fin∧R∈Ring→A∈LMod
22 eqid ⊢Scalar⁡A=Scalar⁡A
23 eqid ⊢⋅A=⋅A
24 eqid ⊢1Scalar⁡A=1Scalar⁡A
25 2 22 23 24 lmodvs1 ⊢A∈LMod∧1A∈B→1Scalar⁡A⋅A1A=1A
26 21 9 25 syl2anc ⊢N∈Fin∧R∈Ring→1Scalar⁡A⋅A1A=1A
27 26 eqcomd ⊢N∈Fin∧R∈Ring→1A=1Scalar⁡A⋅A1A
28 17 20 27 rspcedvd ⊢N∈Fin∧R∈Ring→∃c∈BaseR1A=c⋅A1A
29 13 1 2 7 23 5 scmatel ⊢N∈Fin∧R∈Ring→1A∈S↔1A∈B∧∃c∈BaseR1A=c⋅A1A
30 9 28 29 mpbir2and ⊢N∈Fin∧R∈Ring→1A∈S