This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = ( ∅ Mat 𝑅 )
Assertion mat0dimcrng ( 𝑅 ∈ Ring → 𝐴 ∈ CRing )

Proof

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