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

Theorem dmatmulcl 20513
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 dmatid.a . . . 4 𝐴 = (𝑁 Mat 𝑅)
2 eqid 2805 . . . 4 (Base‘𝑅) = (Base‘𝑅)
3 dmatid.b . . . 4 𝐵 = (Base‘𝐴)
4 simpll 774 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 𝑁 ∈ Fin)
5 simplr 776 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 𝑅 ∈ Ring)
653ad2ant1 1156 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 𝑅 ∈ Ring)
7 eqid 2805 . . . . . . 7 (Base‘𝐴) = (Base‘𝐴)
8 simp2 1160 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 𝑥𝑁)
9 simp3 1161 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 𝑦𝑁)
10 dmatid.0 . . . . . . . . . . 11 0 = (0g𝑅)
11 dmatid.d . . . . . . . . . . 11 𝐷 = (𝑁 DMat 𝑅)
121, 7, 10, 11dmatmat 20507 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋𝐷𝑋 ∈ (Base‘𝐴)))
1312imp 395 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑋𝐷) → 𝑋 ∈ (Base‘𝐴))
1413adantrr 699 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 𝑋 ∈ (Base‘𝐴))
15143ad2ant1 1156 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 𝑋 ∈ (Base‘𝐴))
161, 2, 7, 8, 9, 15matecld 20438 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → (𝑥𝑋𝑦) ∈ (Base‘𝑅))
171, 7, 10, 11dmatmat 20507 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑌𝐷𝑌 ∈ (Base‘𝐴)))
1817imp 395 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑌𝐷) → 𝑌 ∈ (Base‘𝐴))
1918adantrl 698 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 𝑌 ∈ (Base‘𝐴))
20193ad2ant1 1156 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 𝑌 ∈ (Base‘𝐴))
211, 2, 7, 8, 9, 20matecld 20438 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → (𝑥𝑌𝑦) ∈ (Base‘𝑅))
22 eqid 2805 . . . . . . 7 (.r𝑅) = (.r𝑅)
232, 22ringcl 18759 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝑥𝑋𝑦) ∈ (Base‘𝑅) ∧ (𝑥𝑌𝑦) ∈ (Base‘𝑅)) → ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)) ∈ (Base‘𝑅))
246, 16, 21, 23syl3anc 1483 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)) ∈ (Base‘𝑅))
252, 10ring0cl 18767 . . . . . . . 8 (𝑅 ∈ Ring → 0 ∈ (Base‘𝑅))
2625adantl 469 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0 ∈ (Base‘𝑅))
2726adantr 468 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 0 ∈ (Base‘𝑅))
28273ad2ant1 1156 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → 0 ∈ (Base‘𝑅))
2924, 28ifcld 4321 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ 𝑥𝑁𝑦𝑁) → if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ) ∈ (Base‘𝑅))
301, 2, 3, 4, 5, 29matbas2d 20435 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) ∈ 𝐵)
31 eqidd 2806 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )))
32 eqeq12 2818 . . . . . . . . 9 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥 = 𝑦𝑖 = 𝑗))
33 oveq12 6880 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥𝑋𝑦) = (𝑖𝑋𝑗))
34 oveq12 6880 . . . . . . . . . 10 ((𝑥 = 𝑖𝑦 = 𝑗) → (𝑥𝑌𝑦) = (𝑖𝑌𝑗))
3533, 34oveq12d 6889 . . . . . . . . 9 ((𝑥 = 𝑖𝑦 = 𝑗) → ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)) = ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)))
3632, 35ifbieq1d 4299 . . . . . . . 8 ((𝑥 = 𝑖𝑦 = 𝑗) → if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ) = if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ))
3736adantl 469 . . . . . . 7 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) ∧ (𝑥 = 𝑖𝑦 = 𝑗)) → if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ) = if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ))
38 simplrl 786 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → 𝑖𝑁)
39 simplrr 787 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → 𝑗𝑁)
40 ovex 6903 . . . . . . . . 9 ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)) ∈ V
4110fvexi 6419 . . . . . . . . 9 0 ∈ V
4240, 41ifex 4324 . . . . . . . 8 if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ) ∈ V
4342a1i 11 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ) ∈ V)
4431, 37, 38, 39, 43ovmpt2d 7015 . . . . . 6 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ))
45 ifnefalse 4288 . . . . . . 7 (𝑖𝑗 → if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ) = 0 )
4645adantl 469 . . . . . 6 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → if(𝑖 = 𝑗, ((𝑖𝑋𝑗)(.r𝑅)(𝑖𝑌𝑗)), 0 ) = 0 )
4744, 46eqtrd 2839 . . . . 5 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 )
4847ex 399 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖𝑗 → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 ))
4948ralrimivva 3158 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 ))
50 oveq 6877 . . . . . . 7 (𝑚 = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) → (𝑖𝑚𝑗) = (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗))
5150eqeq1d 2807 . . . . . 6 (𝑚 = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) → ((𝑖𝑚𝑗) = 0 ↔ (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 ))
5251imbi2d 331 . . . . 5 (𝑚 = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) → ((𝑖𝑗 → (𝑖𝑚𝑗) = 0 ) ↔ (𝑖𝑗 → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 )))
53522ralbidv 3176 . . . 4 (𝑚 = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) → (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑚𝑗) = 0 ) ↔ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 )))
5453elrab 3558 . . 3 ((𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) ∈ {𝑚𝐵 ∣ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑚𝑗) = 0 )} ↔ ((𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) ∈ 𝐵 ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖(𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 ))𝑗) = 0 )))
5530, 49, 54sylanbrc 574 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )) ∈ {𝑚𝐵 ∣ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑚𝑗) = 0 )})
561, 3, 10, 11dmatmul 20510 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → (𝑋(.r𝐴)𝑌) = (𝑥𝑁, 𝑦𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r𝑅)(𝑥𝑌𝑦)), 0 )))
571, 3, 10, 11dmatval 20505 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐷 = {𝑚𝐵 ∣ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑚𝑗) = 0 )})
5857adantr 468 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → 𝐷 = {𝑚𝐵 ∣ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑚𝑗) = 0 )})
5955, 56, 583eltr4d 2899 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐷𝑌𝐷)) → (𝑋(.r𝐴)𝑌) ∈ 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2158  wne 2977  wral 3095  {crab 3099  Vcvv 3390  ifcif 4276  cfv 6098  (class class class)co 6871  cmpt2 6873  Fincfn 8189  Basecbs 16064  .rcmulr 16150  0gc0g 16301  Ringcrg 18745   Mat cmat 20419   DMat cdmat 20501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-inf2 8782  ax-cnex 10274  ax-resscn 10275  ax-1cn 10276  ax-icn 10277  ax-addcl 10278  ax-addrcl 10279  ax-mulcl 10280  ax-mulrcl 10281  ax-mulcom 10282  ax-addass 10283  ax-mulass 10284  ax-distr 10285  ax-i2m1 10286  ax-1ne0 10287  ax-1rid 10288  ax-rnegex 10289  ax-rrecex 10290  ax-cnre 10291  ax-pre-lttri 10292  ax-pre-lttrn 10293  ax-pre-ltadd 10294  ax-pre-mulgt0 10295
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-nel 3081  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-ot 4376  df-uni 4627  df-int 4666  df-iun 4710  df-iin 4711  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-se 5268  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-isom 6107  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-of 7124  df-om 7293  df-1st 7395  df-2nd 7396  df-supp 7527  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-oadd 7797  df-er 7976  df-map 8091  df-ixp 8143  df-en 8190  df-dom 8191  df-sdom 8192  df-fin 8193  df-fsupp 8512  df-sup 8584  df-oi 8651  df-card 9045  df-pnf 10358  df-mnf 10359  df-xr 10360  df-ltxr 10361  df-le 10362  df-sub 10550  df-neg 10551  df-nn 11303  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-z 11640  df-dec 11756  df-uz 11901  df-fz 12546  df-fzo 12686  df-seq 13021  df-hash 13334  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16171  df-hom 16173  df-cco 16174  df-0g 16303  df-gsum 16304  df-prds 16309  df-pws 16311  df-mre 16447  df-mrc 16448  df-acs 16450  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-grp 17626  df-minusg 17627  df-mulg 17742  df-cntz 17947  df-cmn 18392  df-abl 18393  df-mgp 18688  df-ur 18700  df-ring 18747  df-sra 19377  df-rgmod 19378  df-dsmm 20282  df-frlm 20297  df-mamu 20396  df-mat 20420  df-dmat 20503
This theorem is referenced by:  dmatsrng  20514
  Copyright terms: Public domain W3C validator