Metamath Proof Explorer

Theorem minmar1marrep

Description: The minor matrix is a special case of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019) (Revised by AV, 4-Jul-2022)

Ref Expression
Hypotheses minmar1marrep.a ⊢ A = N Mat R
minmar1marrep.b ⊢ B = Base A
minmar1marrep.o ⊢ 1 ˙ = 1 R
Assertion minmar1marrep ⊢ R ∈ Ring ∧ M ∈ B → N minMatR1 R ⁡ M = M N matRRep R 1 ˙

Proof

Step Hyp Ref Expression
1 minmar1marrep.a ⊢ A = N Mat R
2 minmar1marrep.b ⊢ B = Base A
3 minmar1marrep.o ⊢ 1 ˙ = 1 R
4 eqid ⊢ N minMatR1 R = N minMatR1 R
5 eqid ⊢ 0 R = 0 R
6 1 2 4 3 5 minmar1val0 ⊢ M ∈ B → N minMatR1 R ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 R i M j
7 6 adantl ⊢ R ∈ Ring ∧ M ∈ B → N minMatR1 R ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 R i M j
8 simpr ⊢ R ∈ Ring ∧ M ∈ B → M ∈ B
9 eqid ⊢ Base R = Base R
10 9 3 ringidcl ⊢ R ∈ Ring → 1 ˙ ∈ Base R
11 10 adantr ⊢ R ∈ Ring ∧ M ∈ B → 1 ˙ ∈ Base R
12 eqid ⊢ N matRRep R = N matRRep R
13 1 2 12 5 marrepval0 ⊢ M ∈ B ∧ 1 ˙ ∈ Base R → M N matRRep R 1 ˙ = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 R i M j
14 8 11 13 syl2anc ⊢ R ∈ Ring ∧ M ∈ B → M N matRRep R 1 ˙ = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 R i M j
15 7 14 eqtr4d ⊢ R ∈ Ring ∧ M ∈ B → N minMatR1 R ⁡ M = M N matRRep R 1 ˙