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 = ∅ Mat R
Assertion mat0dimcrng ⊢ R ∈ Ring → A ∈ CRing

Proof

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