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

Metamath Proof Explorer

Theorem ressvsca

Description: .s is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses resssca.1 ⊢ H = G ↾ 𝑠 A
ressvsca.2 ⊢ · ˙ = ⋅ G
Assertion ressvsca ⊢ A ∈ V → · ˙ = ⋅ H

Proof

Step Hyp Ref Expression
1 resssca.1 ⊢ H = G ↾ 𝑠 A
2 ressvsca.2 ⊢ · ˙ = ⋅ G
3 vscaid ⊢ ⋅ 𝑠 = Slot ⋅ ndx
4 vscandxnbasendx ⊢ ⋅ ndx ≠ Base ndx
5 1 2 3 4 resseqnbas ⊢ A ∈ V → · ˙ = ⋅ H