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		0fin	⊢ ∅ ∈ 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 )