This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ V → · ˙ = ⋅ S

Proof

Step Hyp Ref Expression
1 ressmulr.1 ⊢ S = R ↾ 𝑠 A
2 ressmulr.2 ⊢ · ˙ = ⋅ R
3 mulridx ⊢ ⋅ 𝑟 = Slot ⋅ ndx
4 basendxnmulrndx ⊢ Base ndx ≠ ⋅ ndx
5 4 necomi ⊢ ⋅ ndx ≠ Base ndx
6 1 2 3 5 resseqnbas ⊢ A ∈ V → · ˙ = ⋅ S