Metamath Proof Explorer

Theorem scmatel

Description: An N x N scalar matrix over (a ring) R . (Contributed by AV, 18-Dec-2019)

Ref Expression
Hypotheses scmatval.k ⊢ K = Base R
scmatval.a ⊢ A = N Mat R
scmatval.b ⊢ B = Base A
scmatval.1 ⊢ 1 ˙ = 1 A
scmatval.t ⊢ · ˙ = ⋅ A
scmatval.s ⊢ S = N ScMat R
Assertion scmatel ⊢ N ∈ Fin ∧ R ∈ V → M ∈ S ↔ M ∈ B ∧ ∃ c ∈ K M = c · ˙ 1 ˙

Proof

Step Hyp Ref Expression
1 scmatval.k ⊢ K = Base R
2 scmatval.a ⊢ A = N Mat R
3 scmatval.b ⊢ B = Base A
4 scmatval.1 ⊢ 1 ˙ = 1 A
5 scmatval.t ⊢ · ˙ = ⋅ A
6 scmatval.s ⊢ S = N ScMat R
7 1 2 3 4 5 6 scmatval ⊢ N ∈ Fin ∧ R ∈ V → S = m ∈ B | ∃ c ∈ K m = c · ˙ 1 ˙
8 7 eleq2d ⊢ N ∈ Fin ∧ R ∈ V → M ∈ S ↔ M ∈ m ∈ B | ∃ c ∈ K m = c · ˙ 1 ˙
9 eqeq1 ⊢ m = M → m = c · ˙ 1 ˙ ↔ M = c · ˙ 1 ˙
10 9 rexbidv ⊢ m = M → ∃ c ∈ K m = c · ˙ 1 ˙ ↔ ∃ c ∈ K M = c · ˙ 1 ˙
11 10 elrab ⊢ M ∈ m ∈ B | ∃ c ∈ K m = c · ˙ 1 ˙ ↔ M ∈ B ∧ ∃ c ∈ K M = c · ˙ 1 ˙
12 8 11 bitrdi ⊢ N ∈ Fin ∧ R ∈ V → M ∈ S ↔ M ∈ B ∧ ∃ c ∈ K M = c · ˙ 1 ˙