Metamath Proof Explorer

Theorem scmatval

Description: The set of N x N scalar matrices 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 scmatval ⊢ N ∈ Fin ∧ R ∈ V → 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 df-scmat ⊢ ScMat = n ∈ Fin , r ∈ V ⟼ ⦋ n Mat r / a⦌ m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a
8 7 a1i ⊢ N ∈ Fin ∧ R ∈ V → ScMat = n ∈ Fin , r ∈ V ⟼ ⦋ n Mat r / a⦌ m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a
9 ovexd ⊢ N ∈ Fin ∧ R ∈ V ∧ n = N ∧ r = R → n Mat r ∈ V
10 fveq2 ⊢ a = n Mat r → Base a = Base n Mat r
11 fveq2 ⊢ a = n Mat r → ⋅ a = ⋅ n Mat r
12 eqidd ⊢ a = n Mat r → c = c
13 fveq2 ⊢ a = n Mat r → 1 a = 1 n Mat r
14 11 12 13 oveq123d ⊢ a = n Mat r → c ⋅ a 1 a = c ⋅ n Mat r 1 n Mat r
15 14 eqeq2d ⊢ a = n Mat r → m = c ⋅ a 1 a ↔ m = c ⋅ n Mat r 1 n Mat r
16 15 rexbidv ⊢ a = n Mat r → ∃ c ∈ Base r m = c ⋅ a 1 a ↔ ∃ c ∈ Base r m = c ⋅ n Mat r 1 n Mat r
17 10 16 rabeqbidv ⊢ a = n Mat r → m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a = m ∈ Base n Mat r | ∃ c ∈ Base r m = c ⋅ n Mat r 1 n Mat r
18 17 adantl ⊢ N ∈ Fin ∧ R ∈ V ∧ n = N ∧ r = R ∧ a = n Mat r → m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a = m ∈ Base n Mat r | ∃ c ∈ Base r m = c ⋅ n Mat r 1 n Mat r
19 9 18 csbied ⊢ N ∈ Fin ∧ R ∈ V ∧ n = N ∧ r = R → ⦋ n Mat r / a⦌ m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a = m ∈ Base n Mat r | ∃ c ∈ Base r m = c ⋅ n Mat r 1 n Mat r
20 oveq12 ⊢ n = N ∧ r = R → n Mat r = N Mat R
21 20 fveq2d ⊢ n = N ∧ r = R → Base n Mat r = Base N Mat R
22 2 fveq2i ⊢ Base A = Base N Mat R
23 3 22 eqtri ⊢ B = Base N Mat R
24 21 23 eqtr4di ⊢ n = N ∧ r = R → Base n Mat r = B
25 fveq2 ⊢ r = R → Base r = Base R
26 25 1 eqtr4di ⊢ r = R → Base r = K
27 26 adantl ⊢ n = N ∧ r = R → Base r = K
28 20 fveq2d ⊢ n = N ∧ r = R → ⋅ n Mat r = ⋅ N Mat R
29 2 fveq2i ⊢ ⋅ A = ⋅ N Mat R
30 5 29 eqtri ⊢ · ˙ = ⋅ N Mat R
31 28 30 eqtr4di ⊢ n = N ∧ r = R → ⋅ n Mat r = · ˙
32 eqidd ⊢ n = N ∧ r = R → c = c
33 20 fveq2d ⊢ n = N ∧ r = R → 1 n Mat r = 1 N Mat R
34 2 fveq2i ⊢ 1 A = 1 N Mat R
35 4 34 eqtri ⊢ 1 ˙ = 1 N Mat R
36 33 35 eqtr4di ⊢ n = N ∧ r = R → 1 n Mat r = 1 ˙
37 31 32 36 oveq123d ⊢ n = N ∧ r = R → c ⋅ n Mat r 1 n Mat r = c · ˙ 1 ˙
38 37 eqeq2d ⊢ n = N ∧ r = R → m = c ⋅ n Mat r 1 n Mat r ↔ m = c · ˙ 1 ˙
39 27 38 rexeqbidv ⊢ n = N ∧ r = R → ∃ c ∈ Base r m = c ⋅ n Mat r 1 n Mat r ↔ ∃ c ∈ K m = c · ˙ 1 ˙
40 24 39 rabeqbidv ⊢ n = N ∧ r = R → m ∈ Base n Mat r | ∃ c ∈ Base r m = c ⋅ n Mat r 1 n Mat r = m ∈ B | ∃ c ∈ K m = c · ˙ 1 ˙
41 40 adantl ⊢ N ∈ Fin ∧ R ∈ V ∧ n = N ∧ r = R → m ∈ Base n Mat r | ∃ c ∈ Base r m = c ⋅ n Mat r 1 n Mat r = m ∈ B | ∃ c ∈ K m = c · ˙ 1 ˙
42 19 41 eqtrd ⊢ N ∈ Fin ∧ R ∈ V ∧ n = N ∧ r = R → ⦋ n Mat r / a⦌ m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a = m ∈ B | ∃ c ∈ K m = c · ˙ 1 ˙
43 simpl ⊢ N ∈ Fin ∧ R ∈ V → N ∈ Fin
44 elex ⊢ R ∈ V → R ∈ V
45 44 adantl ⊢ N ∈ Fin ∧ R ∈ V → R ∈ V
46 3 fvexi ⊢ B ∈ V
47 46 rabex ⊢ m ∈ B | ∃ c ∈ K m = c · ˙ 1 ˙ ∈ V
48 47 a1i ⊢ N ∈ Fin ∧ R ∈ V → m ∈ B | ∃ c ∈ K m = c · ˙ 1 ˙ ∈ V
49 8 42 43 45 48 ovmpod ⊢ N ∈ Fin ∧ R ∈ V → N ScMat R = m ∈ B | ∃ c ∈ K m = c · ˙ 1 ˙
50 6 49 eqtrid ⊢ N ∈ Fin ∧ R ∈ V → S = m ∈ B | ∃ c ∈ K m = c · ˙ 1 ˙