Metamath Proof Explorer

Theorem marrepcl

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

Ref Expression
Hypotheses marrepcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
marrepcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion marrepcl ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐿 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 marrepcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 marrepcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 eqid ⊢ ( 𝑁 matRRep 𝑅 ) = ( 𝑁 matRRep 𝑅 )
4 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
5 1 2 3 4 marrepval ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐿 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
6 5 3adantl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐿 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
9 8 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
10 9 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝑁 ∈ Fin )
11 10 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
12 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
13 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝑆 ∈ ( Base ‘ 𝑅 ) )
14 7 4 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
15 14 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
16 13 15 ifcld ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → if ( 𝑗 = 𝐿 , 𝑆 , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
17 16 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → if ( 𝑗 = 𝐿 , 𝑆 , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
18 17 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑗 = 𝐿 , 𝑆 , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
19 simp2 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
20 simp3 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
21 2 eleq2i ⊢ ( 𝑀 ∈ 𝐵 ↔ 𝑀 ∈ ( Base ‘ 𝐴 ) )
22 21 biimpi ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
23 22 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
24 23 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
25 24 3ad2ant1 ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
26 1 7 matecl ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
27 19 20 25 26 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
28 18 27 ifcld ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
29 1 7 2 11 12 28 matbas2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ∈ 𝐵 )
30 6 29 eqeltrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐿 ) ∈ 𝐵 )