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 = E Mat R
mat1dim.b ⊢ B = Base R
mat1dim.o ⊢ O = E E
Assertion mat1dimid ⊢ R ∈ Ring ∧ E ∈ V → 1 A = O 1 R

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢ A = E Mat R
2 mat1dim.b ⊢ B = Base R
3 mat1dim.o ⊢ O = E E
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 ⊢ 1 R = 1 R
9 eqid ⊢ 0 R = 0 R
10 1 8 9 mat1 ⊢ E ∈ Fin ∧ R ∈ Ring → 1 A = x ∈ E , y ∈ E ⟼ if x = y 1 R 0 R
11 7 10 syl ⊢ R ∈ Ring ∧ E ∈ V → 1 A = x ∈ E , y ∈ E ⟼ if x = y 1 R 0 R
12 simpr ⊢ R ∈ Ring ∧ E ∈ V → E ∈ V
13 fvex ⊢ 1 R ∈ V
14 fvex ⊢ 0 R ∈ V
15 13 14 ifex ⊢ if E = E 1 R 0 R ∈ V
16 15 a1i ⊢ R ∈ Ring ∧ E ∈ V → if E = E 1 R 0 R ∈ V
17 eqid ⊢ x ∈ E , y ∈ E ⟼ if x = y 1 R 0 R = x ∈ E , y ∈ E ⟼ if x = y 1 R 0 R
18 eqeq1 ⊢ x = E → x = y ↔ E = y
19 18 ifbid ⊢ x = E → if x = y 1 R 0 R = if E = y 1 R 0 R
20 eqeq2 ⊢ y = E → E = y ↔ E = E
21 20 ifbid ⊢ y = E → if E = y 1 R 0 R = if E = E 1 R 0 R
22 17 19 21 mposn ⊢ E ∈ V ∧ E ∈ V ∧ if E = E 1 R 0 R ∈ V → x ∈ E , y ∈ E ⟼ if x = y 1 R 0 R = E E if E = E 1 R 0 R
23 12 12 16 22 syl3anc ⊢ R ∈ Ring ∧ E ∈ V → x ∈ E , y ∈ E ⟼ if x = y 1 R 0 R = E E if E = E 1 R 0 R
24 eqid ⊢ E = E
25 24 iftruei ⊢ if E = E 1 R 0 R = 1 R
26 25 opeq2i ⊢ E E if E = E 1 R 0 R = E E 1 R
27 26 sneqi ⊢ E E if E = E 1 R 0 R = E E 1 R
28 23 27 eqtrdi ⊢ R ∈ Ring ∧ E ∈ V → x ∈ E , y ∈ E ⟼ if x = y 1 R 0 R = E E 1 R
29 3 opeq1i ⊢ O 1 R = E E 1 R
30 29 sneqi ⊢ O 1 R = E E 1 R
31 28 30 eqtr4di ⊢ R ∈ Ring ∧ E ∈ V → x ∈ E , y ∈ E ⟼ if x = y 1 R 0 R = O 1 R
32 11 31 eqtrd ⊢ R ∈ Ring ∧ E ∈ V → 1 A = O 1 R