Metamath Proof Explorer

Theorem mat1dimid

Description: The identity 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 mat1dimid ⊢R∈Ring∧E∈V→1A=O1R

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 ⊢1R=1R
9 eqid ⊢0R=0R
10 1 8 9 mat1 ⊢E∈Fin∧R∈Ring→1A=x∈E,y∈E⟼ifx=y1R0R
11 7 10 syl ⊢R∈Ring∧E∈V→1A=x∈E,y∈E⟼ifx=y1R0R
12 simpr ⊢R∈Ring∧E∈V→E∈V
13 fvex ⊢1R∈V
14 fvex ⊢0R∈V
15 13 14 ifex ⊢ifE=E1R0R∈V
16 15 a1i ⊢R∈Ring∧E∈V→ifE=E1R0R∈V
17 eqid ⊢x∈E,y∈E⟼ifx=y1R0R=x∈E,y∈E⟼ifx=y1R0R
18 eqeq1 ⊢x=E→x=y↔E=y
19 18 ifbid ⊢x=E→ifx=y1R0R=ifE=y1R0R
20 eqeq2 ⊢y=E→E=y↔E=E
21 20 ifbid ⊢y=E→ifE=y1R0R=ifE=E1R0R
22 17 19 21 mposn ⊢E∈V∧E∈V∧ifE=E1R0R∈V→x∈E,y∈E⟼ifx=y1R0R=EEifE=E1R0R
23 12 12 16 22 syl3anc ⊢R∈Ring∧E∈V→x∈E,y∈E⟼ifx=y1R0R=EEifE=E1R0R
24 eqid ⊢E=E
25 24 iftruei ⊢ifE=E1R0R=1R
26 25 opeq2i ⊢EEifE=E1R0R=EE1R
27 26 sneqi ⊢EEifE=E1R0R=EE1R
28 23 27 eqtrdi ⊢R∈Ring∧E∈V→x∈E,y∈E⟼ifx=y1R0R=EE1R
29 3 opeq1i ⊢O1R=EE1R
30 29 sneqi ⊢O1R=EE1R
31 28 30 eqtr4di ⊢R∈Ring∧E∈V→x∈E,y∈E⟼ifx=y1R0R=O1R
32 11 31 eqtrd ⊢R∈Ring∧E∈V→1A=O1R