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

Metamath Proof Explorer

Theorem estrchom

Description: The morphisms between extensible structures are mappings between their base sets. (Contributed by AV, 7-Mar-2020)

Ref Expression
Hypotheses estrcbas.c 
|- C = ( ExtStrCat ` U )
estrcbas.u 
|- ( ph -> U e. V )
estrchomfval.h 
|- H = ( Hom ` C )
estrchom.x 
|- ( ph -> X e. U )
estrchom.y 
|- ( ph -> Y e. U )
estrchom.a 
|- A = ( Base ` X )
estrchom.b 
|- B = ( Base ` Y )
Assertion estrchom 
|- ( ph -> ( X H Y ) = ( B ^m A ) )

Proof

Step Hyp Ref Expression
1 estrcbas.c 
 |-  C = ( ExtStrCat ` U )
2 estrcbas.u 
 |-  ( ph -> U e. V )
3 estrchomfval.h 
 |-  H = ( Hom ` C )
4 estrchom.x 
 |-  ( ph -> X e. U )
5 estrchom.y 
 |-  ( ph -> Y e. U )
6 estrchom.a 
 |-  A = ( Base ` X )
7 estrchom.b 
 |-  B = ( Base ` Y )
8 1 2 3 estrchomfval 
 |-  ( ph -> H = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
9 fveq2 
 |-  ( y = Y -> ( Base ` y ) = ( Base ` Y ) )
10 fveq2 
 |-  ( x = X -> ( Base ` x ) = ( Base ` X ) )
11 9 10 oveqan12rd 
 |-  ( ( x = X /\ y = Y ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( ( Base ` Y ) ^m ( Base ` X ) ) )
12 7 6 oveq12i 
 |-  ( B ^m A ) = ( ( Base ` Y ) ^m ( Base ` X ) )
13 11 12 eqtr4di 
 |-  ( ( x = X /\ y = Y ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( B ^m A ) )
14 13 adantl 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( B ^m A ) )
15 ovexd 
 |-  ( ph -> ( B ^m A ) e. _V )
16 8 14 4 5 15 ovmpod 
 |-  ( ph -> ( X H Y ) = ( B ^m A ) )