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

Theorem dmatmulcl 21729
Description: The product of two diagonal matrices is a diagonal matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 18-Dec-2019.)
Hypotheses
Ref Expression
dmatid.a 𝐴 = (𝑁 Mat 𝑅)
dmatid.b 𝐵 = (Base‘𝐴)
dmatid.0 0 = (0g𝑅)
dmatid.d 𝐷 = (𝑁 DMat 𝑅)
Assertion
Ref Expression
dmatmulcl (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → (𝑋(.r𝐴)𝑌) ∈ 𝐷)

Proof of Theorem dmatmulcl
Dummy variables 𝑖 𝑗 𝑥 𝑦 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq 7322 . . . . . 6 (𝑚 = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) → (𝑖𝑚𝑗) = (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗))
21eqeq1d 2738 . . . . 5 (𝑚 = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) → ((𝑖𝑚𝑗) = 0 ↔ (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 ))
32imbi2d 340 . . . 4 (𝑚 = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) → ((𝑖𝑗 → (𝑖𝑚𝑗) = 0 ) ↔ (𝑖𝑗 → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 )))
432ralbidv 3208 . . 3 (𝑚 = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) → (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑚𝑗) = 0 ) ↔ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 )))
5 dmatid.a . . . 4 𝐴 = (𝑁 Mat 𝑅)
6 eqid 2736 . . . 4 (Base‘𝑅) = (Base‘𝑅)
7 dmatid.b . . . 4 𝐵 = (Base‘𝐴)
8 simpll 764 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 𝑁 ∈ Fin)
9 simplr 766 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 𝑅 ∈ Ring)
1093ad2ant1 1132 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 𝑅 ∈ Ring)
11 eqid 2736 . . . . . . 7 (Base‘𝐴) = (Base‘𝐴)
12 simp2 1136 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 𝑥𝑁)
13 simp3 1137 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 𝑦𝑁)
14 dmatid.0 . . . . . . . . . . 11 0 = (0g𝑅)
15 dmatid.d . . . . . . . . . . 11 𝐷 = (𝑁 DMat 𝑅)
165, 11, 14, 15dmatmat 21723 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋𝐷𝑋 ∈ (Base‘𝐴)))
1716imp 407 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑋𝐷) → 𝑋 ∈ (Base‘𝐴))
1817adantrr 714 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 𝑋 ∈ (Base‘𝐴))
19183ad2ant1 1132 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 𝑋 ∈ (Base‘𝐴))
205, 6, 11, 12, 13, 19matecld 21655 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → (𝑥𝑋𝑦) ∈ (Base‘𝑅))
215, 11, 14, 15dmatmat 21723 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑌𝐷𝑌 ∈ (Base‘𝐴)))
2221imp 407 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑌𝐷) → 𝑌 ∈ (Base‘𝐴))
2322adantrl 713 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 𝑌 ∈ (Base‘𝐴))
24233ad2ant1 1132 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 𝑌 ∈ (Base‘𝐴))
255, 6, 11, 12, 13, 24matecld 21655 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → (𝑥𝑌𝑦) ∈ (Base‘𝑅))
26 eqid 2736 . . . . . . 7 (.r𝑅) = (.r𝑅)
276, 26ringcl 19872 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝑥𝑋𝑦) ∈ (Base‘𝑅) ∧ (𝑥𝑌𝑦) ∈ (Base‘𝑅)) → ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)) ∈ (Base‘𝑅))
2810, 20, 25, 27syl3anc 1370 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)) ∈ (Base‘𝑅))
296, 14ring0cl 19880 . . . . . . . 8 (𝑅 ∈ Ring → 0 ∈ (Base‘𝑅))
3029adantl 482 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0 ∈ (Base‘𝑅))
3130adantr 481 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 0 ∈ (Base‘𝑅))
32313ad2ant1 1132 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 0 ∈ (Base‘𝑅))
3328, 32ifcld 4516 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ) ∈ (Base‘𝑅))
345, 6, 7, 8, 9, 33matbas2d 21652 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) ∈ 𝐵)
35 eqidd 2737 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )))
36 eqeq12 2753 . . . . . . . . 9 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥 = 𝑦𝑖 = 𝑗))
37 oveq12 7325 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥𝑋𝑦) = (𝑖𝑋𝑗))
38 oveq12 7325 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥𝑌𝑦) = (𝑖𝑌𝑗))
3937, 38oveq12d 7334 . . . . . . . . 9 ((𝑥 = 𝑖𝑦 = 𝑗) → ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)) = ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)))
4036, 39ifbieq1d 4494 . . . . . . . 8 ((𝑥 = 𝑖𝑦 = 𝑗) → if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ) = if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ))
4140adantl 482 . . . . . . 7 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) ∧ (𝑥 = 𝑖𝑦 = 𝑗)) → if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ) = if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ))
42 simplrl 774 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → 𝑖𝑁)
43 simplrr 775 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → 𝑗𝑁)
44 ovex 7349 . . . . . . . . 9 ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)) ∈ V
4514fvexi 6825 . . . . . . . . 9 0 ∈ V
4644, 45ifex 4520 . . . . . . . 8 if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ) ∈ V
4746a1i 11 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ) ∈ V)
4835, 41, 42, 43, 47ovmpod 7466 . . . . . 6 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ))
49 ifnefalse 4482 . . . . . . 7 (𝑖𝑗 → if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ) = 0 )
5049adantl 482 . . . . . 6 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ) = 0 )
5148, 50eqtrd 2776 . . . . 5 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 )
5251ex 413 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖𝑗 → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 ))
5352ralrimivva 3193 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 ))
544, 34, 53elrabd 3635 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) ∈ {𝑚𝐵 ∣ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑚𝑗) = 0 )})
555, 7, 14, 15dmatmul 21726 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → (𝑋(.r𝐴)𝑌) = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )))
565, 7, 14, 15dmatval 21721 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐷 = {𝑚𝐵 ∣ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑚𝑗) = 0 )})
5756adantr 481 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 𝐷 = {𝑚𝐵 ∣ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑚𝑗) = 0 )})
5854, 55, 573eltr4d 2852 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → (𝑋(.r𝐴)𝑌) ∈ 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2940  wral 3061  {crab 3403  Vcvv 3440  ifcif 4470  cfv 6465  (class class class)co 7316  cmpo 7318  Fincfn 8782  Basecbs 16986  .rcmulr 17037  0gc0g 17224  Ringcrg 19855   Mat cmat 21634   DMat cdmat 21717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5223  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-cnex 11006  ax-resscn 11007  ax-1cn 11008  ax-icn 11009  ax-addcl 11010  ax-addrcl 11011  ax-mulcl 11012  ax-mulrcl 11013  ax-mulcom 11014  ax-addass 11015  ax-mulass 11016  ax-distr 11017  ax-i2m1 11018  ax-1ne0 11019  ax-1rid 11020  ax-rnegex 11021  ax-rrecex 11022  ax-cnre 11023  ax-pre-lttri 11024  ax-pre-lttrn 11025  ax-pre-ltadd 11026  ax-pre-mulgt0 11027
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-ot 4579  df-uni 4850  df-int 4892  df-iun 4938  df-iin 4939  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7273  df-ov 7319  df-oprab 7320  df-mpo 7321  df-of 7574  df-om 7759  df-1st 7877  df-2nd 7878  df-supp 8026  df-frecs 8145  df-wrecs 8176  df-recs 8250  df-rdg 8289  df-1o 8345  df-er 8547  df-map 8666  df-ixp 8735  df-en 8783  df-dom 8784  df-sdom 8785  df-fin 8786  df-fsupp 9205  df-sup 9277  df-oi 9345  df-card 9774  df-pnf 11090  df-mnf 11091  df-xr 11092  df-ltxr 11093  df-le 11094  df-sub 11286  df-neg 11287  df-nn 12053  df-2 12115  df-3 12116  df-4 12117  df-5 12118  df-6 12119  df-7 12120  df-8 12121  df-9 12122  df-n0 12313  df-z 12399  df-dec 12517  df-uz 12662  df-fz 13319  df-fzo 13462  df-seq 13801  df-hash 14124  df-struct 16922  df-sets 16939  df-slot 16957  df-ndx 16969  df-base 16987  df-ress 17016  df-plusg 17049  df-mulr 17050  df-sca 17052  df-vsca 17053  df-ip 17054  df-tset 17055  df-ple 17056  df-ds 17058  df-hom 17060  df-cco 17061  df-0g 17226  df-gsum 17227  df-prds 17232  df-pws 17234  df-mre 17369  df-mrc 17370  df-acs 17372  df-mgm 18400  df-sgrp 18449  df-mnd 18460  df-submnd 18505  df-grp 18653  df-minusg 18654  df-mulg 18774  df-cntz 18996  df-cmn 19460  df-abl 19461  df-mgp 19793  df-ur 19810  df-ring 19857  df-sra 20514  df-rgmod 20515  df-dsmm 21019  df-frlm 21034  df-mamu 21613  df-mat 21635  df-dmat 21719
This theorem is referenced by:  dmatsrng  21730
  Copyright terms: Public domain W3C validator