Metamath Proof Explorer


Theorem ressmulr

Description: .r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Hypotheses ressmulr.1 S=R𝑠A
ressmulr.2 ·˙=R
Assertion ressmulr AV·˙=S

Proof

Step Hyp Ref Expression
1 ressmulr.1 S=R𝑠A
2 ressmulr.2 ·˙=R
3 mulrid 𝑟=Slotndx
4 basendxnmulrndx Basendxndx
5 4 necomi ndxBasendx
6 1 2 3 5 resseqnbas AV·˙=S