Metamath Proof Explorer

Theorem mat1dim0

Description: The zero of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019)

Ref Expression
Hypotheses mat1dim.a ⊢A=EMatR
mat1dim.b ⊢B=BaseR
mat1dim.o ⊢O=EE
Assertion mat1dim0 ⊢R∈Ring∧E∈V→0A=O0R

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢A=EMatR
2 mat1dim.b ⊢B=BaseR
3 mat1dim.o ⊢O=EE
4 snfi ⊢E∈Fin
5 4 a1i ⊢E∈V→E∈Fin
6 5 anim2i ⊢R∈Ring∧E∈V→R∈Ring∧E∈Fin
7 6 ancomd ⊢R∈Ring∧E∈V→E∈Fin∧R∈Ring
8 eqid ⊢0R=0R
9 1 8 mat0op ⊢E∈Fin∧R∈Ring→0A=x∈E,y∈E⟼0R
10 7 9 syl ⊢R∈Ring∧E∈V→0A=x∈E,y∈E⟼0R
11 simpr ⊢R∈Ring∧E∈V→E∈V
12 fvexd ⊢R∈Ring∧E∈V→0R∈V
13 eqid ⊢x∈E,y∈E⟼0R=x∈E,y∈E⟼0R
14 eqidd ⊢x=E→0R=0R
15 eqidd ⊢y=E→0R=0R
16 13 14 15 mposn ⊢E∈V∧E∈V∧0R∈V→x∈E,y∈E⟼0R=EE0R
17 3 eqcomi ⊢EE=O
18 17 opeq1i ⊢EE0R=O0R
19 18 sneqi ⊢EE0R=O0R
20 16 19 eqtrdi ⊢E∈V∧E∈V∧0R∈V→x∈E,y∈E⟼0R=O0R
21 11 11 12 20 syl3anc ⊢R∈Ring∧E∈V→x∈E,y∈E⟼0R=O0R
22 10 21 eqtrd ⊢R∈Ring∧E∈V→0A=O0R