Metamath Proof Explorer


Theorem reldmprds

Description: The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015) (Revised by Thierry Arnoux, 15-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

Ref Expression
Assertion reldmprds Reldom𝑠

Proof

Step Hyp Ref Expression
1 df-prds 𝑠=sV,rVxdomrBaserx/vfv,gvxdomrfxHomrxgx/hBasendxv+ndxfv,gvxdomrfx+rxgxndxfv,gvxdomrfxrxgxScalarndxsndxfBases,gvxdomrfrxgx𝑖ndxfv,gvsxdomrfx𝑖rxgxTopSetndx𝑡TopOpenrndxfg|fgvxdomrfxrxgxdistndxfv,gvsupranxdomrfxdistrxgx0*<Homndxhcompndxav×v,cvd2ndahc,ehaxdomrdx1stax2ndaxcomprxcxex
2 1 reldmmpo Reldom𝑠