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 ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
Assertion mat1dimid ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 1r ‘ 𝐴 ) = { ⟨ 𝑂 , ( 1r ‘ 𝑅 ) ⟩ } )

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
2 mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
4 snfi ⊢ { 𝐸 } ∈ Fin
5 4 a1i ⊢ ( 𝐸 ∈ 𝑉 → { 𝐸 } ∈ Fin )
6 5 anim2i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑅 ∈ Ring ∧ { 𝐸 } ∈ Fin ) )
7 6 ancomd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) )
8 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
9 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
10 1 8 9 mat1 ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
11 7 10 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 1r ‘ 𝐴 ) = ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
12 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐸 ∈ 𝑉 )
13 fvex ⊢ ( 1r ‘ 𝑅 ) ∈ V
14 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
15 13 14 ifex ⊢ if ( 𝐸 = 𝐸 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ V
16 15 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → if ( 𝐸 = 𝐸 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ V )
17 eqid ⊢ ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
18 eqeq1 ⊢ ( 𝑥 = 𝐸 → ( 𝑥 = 𝑦 ↔ 𝐸 = 𝑦 ) )
19 18 ifbid ⊢ ( 𝑥 = 𝐸 → if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝐸 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
20 eqeq2 ⊢ ( 𝑦 = 𝐸 → ( 𝐸 = 𝑦 ↔ 𝐸 = 𝐸 ) )
21 20 ifbid ⊢ ( 𝑦 = 𝐸 → if ( 𝐸 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝐸 = 𝐸 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
22 17 19 21 mposn ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ∧ if ( 𝐸 = 𝐸 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ V ) → ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , if ( 𝐸 = 𝐸 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ⟩ } )
23 12 12 16 22 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , if ( 𝐸 = 𝐸 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ⟩ } )
24 eqid ⊢ 𝐸 = 𝐸
25 24 iftruei ⊢ if ( 𝐸 = 𝐸 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 )
26 25 opeq2i ⊢ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , if ( 𝐸 = 𝐸 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 1r ‘ 𝑅 ) ⟩
27 26 sneqi ⊢ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , if ( 𝐸 = 𝐸 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 1r ‘ 𝑅 ) ⟩ }
28 23 27 eqtrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 1r ‘ 𝑅 ) ⟩ } )
29 3 opeq1i ⊢ ⟨ 𝑂 , ( 1r ‘ 𝑅 ) ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 1r ‘ 𝑅 ) ⟩
30 29 sneqi ⊢ { ⟨ 𝑂 , ( 1r ‘ 𝑅 ) ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 1r ‘ 𝑅 ) ⟩ }
31 28 30 eqtr4di ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑥 ∈ { 𝐸 } , 𝑦 ∈ { 𝐸 } ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = { ⟨ 𝑂 , ( 1r ‘ 𝑅 ) ⟩ } )
32 11 31 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 1r ‘ 𝐴 ) = { ⟨ 𝑂 , ( 1r ‘ 𝑅 ) ⟩ } )