Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  marep01ma Structured version   Visualization version   GIF version

Theorem marep01ma 20589
 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.)
Hypotheses
Ref Expression
marep01ma.a 𝐴 = (𝑁 Mat 𝑅)
marep01ma.b 𝐵 = (Base‘𝐴)
marep01ma.r 𝑅 ∈ CRing
marep01ma.0 0 = (0g𝑅)
marep01ma.1 1 = (1r𝑅)
Assertion
Ref Expression
marep01ma (𝑀𝐵 → (𝑘𝑁, 𝑙𝑁 ↦ if(𝑘 = 𝐻, if(𝑙 = 𝐼, 1 , 0 ), (𝑘𝑀𝑙))) ∈ 𝐵)
Distinct variable groups:   𝑘,𝑙,𝐵   𝑘,𝑀,𝑙   𝑘,𝑁,𝑙   𝑅,𝑘,𝑙
Allowed substitution hints:   𝐴(𝑘,𝑙)   1 (𝑘,𝑙)   𝐻(𝑘,𝑙)   𝐼(𝑘,𝑙)   0 (𝑘,𝑙)

Proof of Theorem marep01ma
StepHypRef Expression
1 marep01ma.a . 2 𝐴 = (𝑁 Mat 𝑅)
2 eqid 2724 . 2 (Base‘𝑅) = (Base‘𝑅)
3 marep01ma.b . 2 𝐵 = (Base‘𝐴)
41, 3matrcl 20341 . . 3 (𝑀𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
54simpld 477 . 2 (𝑀𝐵𝑁 ∈ Fin)
6 marep01ma.r . . 3 𝑅 ∈ CRing
76a1i 11 . 2 (𝑀𝐵𝑅 ∈ CRing)
8 crngring 18679 . . . . . 6 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
9 marep01ma.1 . . . . . . 7 1 = (1r𝑅)
102, 9ringidcl 18689 . . . . . 6 (𝑅 ∈ Ring → 1 ∈ (Base‘𝑅))
116, 8, 10mp2b 10 . . . . 5 1 ∈ (Base‘𝑅)
12 marep01ma.0 . . . . . . 7 0 = (0g𝑅)
132, 12ring0cl 18690 . . . . . 6 (𝑅 ∈ Ring → 0 ∈ (Base‘𝑅))
146, 8, 13mp2b 10 . . . . 5 0 ∈ (Base‘𝑅)
1511, 14keepel 4263 . . . 4 if(𝑙 = 𝐼, 1 , 0 ) ∈ (Base‘𝑅)
1615a1i 11 . . 3 ((𝑀𝐵𝑘𝑁𝑙𝑁) → if(𝑙 = 𝐼, 1 , 0 ) ∈ (Base‘𝑅))
17 simp2 1129 . . . 4 ((𝑀𝐵𝑘𝑁𝑙𝑁) → 𝑘𝑁)
18 simp3 1130 . . . 4 ((𝑀𝐵𝑘𝑁𝑙𝑁) → 𝑙𝑁)
19 id 22 . . . . . 6 (𝑀𝐵𝑀𝐵)
2019, 3syl6eleq 2813 . . . . 5 (𝑀𝐵𝑀 ∈ (Base‘𝐴))
21203ad2ant1 1125 . . . 4 ((𝑀𝐵𝑘𝑁𝑙𝑁) → 𝑀 ∈ (Base‘𝐴))
221, 2matecl 20354 . . . 4 ((𝑘𝑁𝑙𝑁𝑀 ∈ (Base‘𝐴)) → (𝑘𝑀𝑙) ∈ (Base‘𝑅))
2317, 18, 21, 22syl3anc 1439 . . 3 ((𝑀𝐵𝑘𝑁𝑙𝑁) → (𝑘𝑀𝑙) ∈ (Base‘𝑅))
2416, 23ifcld 4239 . 2 ((𝑀𝐵𝑘𝑁𝑙𝑁) → if(𝑘 = 𝐻, if(𝑙 = 𝐼, 1 , 0 ), (𝑘𝑀𝑙)) ∈ (Base‘𝑅))
251, 2, 3, 5, 7, 24matbas2d 20352 1 (𝑀𝐵 → (𝑘𝑁, 𝑙𝑁 ↦ if(𝑘 = 𝐻, if(𝑙 = 𝐼, 1 , 0 ), (𝑘𝑀𝑙))) ∈ 𝐵)