This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
minmar1cl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion minmar1cl ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐿 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 minmar1cl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 minmar1cl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4 1 2 3 minmar1marrep ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) )
5 4 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) )
6 5 oveqd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐿 ) = ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐿 ) )
7 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
8 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 9 3 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
11 10 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
12 7 8 11 3jca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) )
13 1 2 marrepcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐿 ) ∈ 𝐵 )
14 12 13 sylan ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐿 ) ∈ 𝐵 )
15 6 14 eqeltrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐿 ) ∈ 𝐵 )