Metamath Proof Explorer
Description: The functionalization of the involution component of a structure.
(Contributed by Mario Carneiro, 6Oct2015)


Ref 
Expression 

Hypotheses 
staffval.b 
⊢ 𝐵 = ( Base ‘ 𝑅 ) 


staffval.i 
⊢ ∗ = ( *_{𝑟} ‘ 𝑅 ) 


staffval.f 
⊢ ∙ = ( *_{rf} ‘ 𝑅 ) 

Assertion 
stafval 
⊢ ( 𝐴 ∈ 𝐵 → ( ∙ ‘ 𝐴 ) = ( ∗ ‘ 𝐴 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

staffval.b 
⊢ 𝐵 = ( Base ‘ 𝑅 ) 
2 

staffval.i 
⊢ ∗ = ( *_{𝑟} ‘ 𝑅 ) 
3 

staffval.f 
⊢ ∙ = ( *_{rf} ‘ 𝑅 ) 
4 

fveq2 
⊢ ( 𝑥 = 𝐴 → ( ∗ ‘ 𝑥 ) = ( ∗ ‘ 𝐴 ) ) 
5 
1 2 3

staffval 
⊢ ∙ = ( 𝑥 ∈ 𝐵 ↦ ( ∗ ‘ 𝑥 ) ) 
6 

fvex 
⊢ ( ∗ ‘ 𝐴 ) ∈ V 
7 
4 5 6

fvmpt 
⊢ ( 𝐴 ∈ 𝐵 → ( ∙ ‘ 𝐴 ) = ( ∗ ‘ 𝐴 ) ) 