Theorem mat1ric

Description: A ring is isomorphic to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 30-Dec-2019)

	Ref	Expression
Hypothesis	mat1ric.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
Assertion	mat1ric	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ≃𝑟 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mat1ric.a	⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
2		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
4		eqid	⊢ ⟨ 𝐸 , 𝐸 ⟩ = ⟨ 𝐸 , 𝐸 ⟩
5		opeq2	⊢ ( 𝑥 = 𝑦 → ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑥 ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑦 ⟩ )
6	5	sneqd	⊢ ( 𝑥 = 𝑦 → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑥 ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑦 ⟩ } )
7	6	cbvmptv	⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑥 ⟩ } ) = ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑦 ⟩ } )
8	2 1 3 4 7	mat1rngiso	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑥 ⟩ } ) ∈ ( 𝑅 RingIso 𝐴 ) )
9	8	ne0d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑅 RingIso 𝐴 ) ≠ ∅ )
10		brric	⊢ ( 𝑅 ≃𝑟 𝐴 ↔ ( 𝑅 RingIso 𝐴 ) ≠ ∅ )
11	9 10	sylibr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ≃𝑟 𝐴 )