Metamath Proof Explorer

Theorem mat0dimcrng

Description: The algebra of matrices with dimension 0 (over an arbitrary ring!) is a commutative ring. (Contributed by AV, 10-Aug-2019)

Ref Expression
Hypothesis mat0dim.a ⊢A=∅MatR
Assertion mat0dimcrng ⊢R∈Ring→A∈CRing

Proof

Step Hyp Ref Expression
1 mat0dim.a ⊢A=∅MatR
2 0fin ⊢∅∈Fin
3 1 matring ⊢∅∈Fin∧R∈Ring→A∈Ring
4 2 3 mpan ⊢R∈Ring→A∈Ring
5 mat0dimbas0 ⊢R∈Ring→Base∅MatR=∅
6 1 eqcomi ⊢∅MatR=A
7 6 fveq2i ⊢Base∅MatR=BaseA
8 7 eqeq1i ⊢Base∅MatR=∅↔BaseA=∅
9 eqidd ⊢BaseA=∅∧R∈Ring→∅⋅A∅=∅⋅A∅
10 0ex ⊢∅∈V
11 oveq1 ⊢x=∅→x⋅Ay=∅⋅Ay
12 oveq2 ⊢x=∅→y⋅Ax=y⋅A∅
13 11 12 eqeq12d ⊢x=∅→x⋅Ay=y⋅Ax↔∅⋅Ay=y⋅A∅
14 13 ralbidv ⊢x=∅→∀y∈∅x⋅Ay=y⋅Ax↔∀y∈∅∅⋅Ay=y⋅A∅
15 10 14 ralsn ⊢∀x∈∅∀y∈∅x⋅Ay=y⋅Ax↔∀y∈∅∅⋅Ay=y⋅A∅
16 oveq2 ⊢y=∅→∅⋅Ay=∅⋅A∅
17 oveq1 ⊢y=∅→y⋅A∅=∅⋅A∅
18 16 17 eqeq12d ⊢y=∅→∅⋅Ay=y⋅A∅↔∅⋅A∅=∅⋅A∅
19 10 18 ralsn ⊢∀y∈∅∅⋅Ay=y⋅A∅↔∅⋅A∅=∅⋅A∅
20 15 19 bitri ⊢∀x∈∅∀y∈∅x⋅Ay=y⋅Ax↔∅⋅A∅=∅⋅A∅
21 9 20 sylibr ⊢BaseA=∅∧R∈Ring→∀x∈∅∀y∈∅x⋅Ay=y⋅Ax
22 raleq ⊢BaseA=∅→∀y∈BaseAx⋅Ay=y⋅Ax↔∀y∈∅x⋅Ay=y⋅Ax
23 22 raleqbi1dv ⊢BaseA=∅→∀x∈BaseA∀y∈BaseAx⋅Ay=y⋅Ax↔∀x∈∅∀y∈∅x⋅Ay=y⋅Ax
24 23 adantr ⊢BaseA=∅∧R∈Ring→∀x∈BaseA∀y∈BaseAx⋅Ay=y⋅Ax↔∀x∈∅∀y∈∅x⋅Ay=y⋅Ax
25 21 24 mpbird ⊢BaseA=∅∧R∈Ring→∀x∈BaseA∀y∈BaseAx⋅Ay=y⋅Ax
26 25 ex ⊢BaseA=∅→R∈Ring→∀x∈BaseA∀y∈BaseAx⋅Ay=y⋅Ax
27 8 26 sylbi ⊢Base∅MatR=∅→R∈Ring→∀x∈BaseA∀y∈BaseAx⋅Ay=y⋅Ax
28 5 27 mpcom ⊢R∈Ring→∀x∈BaseA∀y∈BaseAx⋅Ay=y⋅Ax
29 eqid ⊢BaseA=BaseA
30 eqid ⊢⋅A=⋅A
31 29 30 iscrng2 ⊢A∈CRing↔A∈Ring∧∀x∈BaseA∀y∈BaseAx⋅Ay=y⋅Ax
32 4 28 31 sylanbrc ⊢R∈Ring→A∈CRing