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 ) )