Metamath Proof Explorer

Theorem minmar1cl

Description: Closure of the row replacement function for square matrices: The matrix for a minor is a matrix. (Contributed by AV, 13-Feb-2019)

Ref Expression
Hypotheses minmar1cl.a ⊢ A = N Mat R
minmar1cl.b ⊢ B = Base A
Assertion minmar1cl ⊢ R ∈ Ring ∧ M ∈ B ∧ K ∈ N ∧ L ∈ N → K N minMatR1 R ⁡ M L ∈ B

Proof

Step Hyp Ref Expression
1 minmar1cl.a ⊢ A = N Mat R
2 minmar1cl.b ⊢ B = Base A
3 eqid ⊢ 1 R = 1 R
4 1 2 3 minmar1marrep ⊢ R ∈ Ring ∧ M ∈ B → N minMatR1 R ⁡ M = M N matRRep R 1 R
5 4 adantr ⊢ R ∈ Ring ∧ M ∈ B ∧ K ∈ N ∧ L ∈ N → N minMatR1 R ⁡ M = M N matRRep R 1 R
6 5 oveqd ⊢ R ∈ Ring ∧ M ∈ B ∧ K ∈ N ∧ L ∈ N → K N minMatR1 R ⁡ M L = K M N matRRep R 1 R L
7 simpl ⊢ R ∈ Ring ∧ M ∈ B → R ∈ Ring
8 simpr ⊢ R ∈ Ring ∧ M ∈ B → M ∈ B
9 eqid ⊢ Base R = Base R
10 9 3 ringidcl ⊢ R ∈ Ring → 1 R ∈ Base R
11 10 adantr ⊢ R ∈ Ring ∧ M ∈ B → 1 R ∈ Base R
12 7 8 11 3jca ⊢ R ∈ Ring ∧ M ∈ B → R ∈ Ring ∧ M ∈ B ∧ 1 R ∈ Base R
13 1 2 marrepcl ⊢ R ∈ Ring ∧ M ∈ B ∧ 1 R ∈ Base R ∧ K ∈ N ∧ L ∈ N → K M N matRRep R 1 R L ∈ B
14 12 13 sylan ⊢ R ∈ Ring ∧ M ∈ B ∧ K ∈ N ∧ L ∈ N → K M N matRRep R 1 R L ∈ B
15 6 14 eqeltrd ⊢ R ∈ Ring ∧ M ∈ B ∧ K ∈ N ∧ L ∈ N → K N minMatR1 R ⁡ M L ∈ B