Metamath Proof Explorer

Theorem marep01ma

Description: Replacing a row of a square matrix by a row with 0's and a 1 results in a square matrix of the same dimension. (Contributed by AV, 30-Dec-2018)

Ref Expression
Hypotheses marep01ma.a ⊢ A = N Mat R
marep01ma.b ⊢ B = Base A
marep01ma.r ⊢ R ∈ CRing
marep01ma.0 ⊢ 0 ˙ = 0 R
marep01ma.1 ⊢ 1 ˙ = 1 R
Assertion marep01ma ⊢ M ∈ B → k ∈ N , l ∈ N ⟼ if k = H if l = I 1 ˙ 0 ˙ k M l ∈ B

Proof

Step Hyp Ref Expression
1 marep01ma.a ⊢ A = N Mat R
2 marep01ma.b ⊢ B = Base A
3 marep01ma.r ⊢ R ∈ CRing
4 marep01ma.0 ⊢ 0 ˙ = 0 R
5 marep01ma.1 ⊢ 1 ˙ = 1 R
6 eqid ⊢ Base R = Base R
7 1 2 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
8 7 simpld ⊢ M ∈ B → N ∈ Fin
9 3 a1i ⊢ M ∈ B → R ∈ CRing
10 crngring ⊢ R ∈ CRing → R ∈ Ring
11 6 5 ringidcl ⊢ R ∈ Ring → 1 ˙ ∈ Base R
12 3 10 11 mp2b ⊢ 1 ˙ ∈ Base R
13 6 4 ring0cl ⊢ R ∈ Ring → 0 ˙ ∈ Base R
14 3 10 13 mp2b ⊢ 0 ˙ ∈ Base R
15 12 14 ifcli ⊢ if l = I 1 ˙ 0 ˙ ∈ Base R
16 15 a1i ⊢ M ∈ B ∧ k ∈ N ∧ l ∈ N → if l = I 1 ˙ 0 ˙ ∈ Base R
17 simp2 ⊢ M ∈ B ∧ k ∈ N ∧ l ∈ N → k ∈ N
18 simp3 ⊢ M ∈ B ∧ k ∈ N ∧ l ∈ N → l ∈ N
19 id ⊢ M ∈ B → M ∈ B
20 19 2 eleqtrdi ⊢ M ∈ B → M ∈ Base A
21 20 3ad2ant1 ⊢ M ∈ B ∧ k ∈ N ∧ l ∈ N → M ∈ Base A
22 1 6 matecl ⊢ k ∈ N ∧ l ∈ N ∧ M ∈ Base A → k M l ∈ Base R
23 17 18 21 22 syl3anc ⊢ M ∈ B ∧ k ∈ N ∧ l ∈ N → k M l ∈ Base R
24 16 23 ifcld ⊢ M ∈ B ∧ k ∈ N ∧ l ∈ N → if k = H if l = I 1 ˙ 0 ˙ k M l ∈ Base R
25 1 6 2 8 9 24 matbas2d ⊢ M ∈ B → k ∈ N , l ∈ N ⟼ if k = H if l = I 1 ˙ 0 ˙ k M l ∈ B