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 = E Mat R
mat1dim.b ⊢ B = Base R
mat1dim.o ⊢ O = E E
Assertion mat1dim0 ⊢ R ∈ Ring ∧ E ∈ V → 0 A = O 0 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 ⊢ 0 R = 0 R
9 1 8 mat0op ⊢ E ∈ Fin ∧ R ∈ Ring → 0 A = x ∈ E , y ∈ E ⟼ 0 R
10 7 9 syl ⊢ R ∈ Ring ∧ E ∈ V → 0 A = x ∈ E , y ∈ E ⟼ 0 R
11 simpr ⊢ R ∈ Ring ∧ E ∈ V → E ∈ V
12 fvexd ⊢ R ∈ Ring ∧ E ∈ V → 0 R ∈ V
13 eqid ⊢ x ∈ E , y ∈ E ⟼ 0 R = x ∈ E , y ∈ E ⟼ 0 R
14 eqidd ⊢ x = E → 0 R = 0 R
15 eqidd ⊢ y = E → 0 R = 0 R
16 13 14 15 mposn ⊢ E ∈ V ∧ E ∈ V ∧ 0 R ∈ V → x ∈ E , y ∈ E ⟼ 0 R = E E 0 R
17 3 eqcomi ⊢ E E = O
18 17 opeq1i ⊢ E E 0 R = O 0 R
19 18 sneqi ⊢ E E 0 R = O 0 R
20 16 19 eqtrdi ⊢ E ∈ V ∧ E ∈ V ∧ 0 R ∈ V → x ∈ E , y ∈ E ⟼ 0 R = O 0 R
21 11 11 12 20 syl3anc ⊢ R ∈ Ring ∧ E ∈ V → x ∈ E , y ∈ E ⟼ 0 R = O 0 R
22 10 21 eqtrd ⊢ R ∈ Ring ∧ E ∈ V → 0 A = O 0 R