comfeqval

Description: Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	comfeqval.b	\|- B = ( Base ` C )
	comfeqval.h	\|- H = ( Hom ` C )
	comfeqval.1	\|- .x. = ( comp ` C )
	comfeqval.2	\|- .xb = ( comp ` D )
	comfeqval.3	\|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
	comfeqval.4	\|- ( ph -> ( comf ` C ) = ( comf ` D ) )
	comfeqval.x	\|- ( ph -> X e. B )
	comfeqval.y	\|- ( ph -> Y e. B )
	comfeqval.z	\|- ( ph -> Z e. B )
	comfeqval.f	\|- ( ph -> F e. ( X H Y ) )
	comfeqval.g	\|- ( ph -> G e. ( Y H Z ) )
Assertion	comfeqval	\|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G ( <. X , Y >. .xb Z ) F ) )

Proof

Step	Hyp	Ref	Expression
1		comfeqval.b	\|- B = ( Base ` C )
2		comfeqval.h	\|- H = ( Hom ` C )
3		comfeqval.1	\|- .x. = ( comp ` C )
4		comfeqval.2	\|- .xb = ( comp ` D )
5		comfeqval.3	\|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
6		comfeqval.4	\|- ( ph -> ( comf ` C ) = ( comf ` D ) )
7		comfeqval.x	\|- ( ph -> X e. B )
8		comfeqval.y	\|- ( ph -> Y e. B )
9		comfeqval.z	\|- ( ph -> Z e. B )
10		comfeqval.f	\|- ( ph -> F e. ( X H Y ) )
11		comfeqval.g	\|- ( ph -> G e. ( Y H Z ) )
12	6	oveqd	\|- ( ph -> ( <. X , Y >. ( comf ` C ) Z ) = ( <. X , Y >. ( comf ` D ) Z ) )
13	12	oveqd	\|- ( ph -> ( G ( <. X , Y >. ( comf ` C ) Z ) F ) = ( G ( <. X , Y >. ( comf ` D ) Z ) F ) )
14		eqid	\|- ( comf ` C ) = ( comf ` C )
15	14 1 2 3 7 8 9 10 11	comfval	\|- ( ph -> ( G ( <. X , Y >. ( comf ` C ) Z ) F ) = ( G ( <. X , Y >. .x. Z ) F ) )
16		eqid	\|- ( comf ` D ) = ( comf ` D )
17		eqid	\|- ( Base ` D ) = ( Base ` D )
18		eqid	\|- ( Hom ` D ) = ( Hom ` D )
19	5	homfeqbas	\|- ( ph -> ( Base ` C ) = ( Base ` D ) )
20	1 19	syl5eq	\|- ( ph -> B = ( Base ` D ) )
21	7 20	eleqtrd	\|- ( ph -> X e. ( Base ` D ) )
22	8 20	eleqtrd	\|- ( ph -> Y e. ( Base ` D ) )
23	9 20	eleqtrd	\|- ( ph -> Z e. ( Base ` D ) )
24	1 2 18 5 7 8	homfeqval	\|- ( ph -> ( X H Y ) = ( X ( Hom ` D ) Y ) )
25	10 24	eleqtrd	\|- ( ph -> F e. ( X ( Hom ` D ) Y ) )
26	1 2 18 5 8 9	homfeqval	\|- ( ph -> ( Y H Z ) = ( Y ( Hom ` D ) Z ) )
27	11 26	eleqtrd	\|- ( ph -> G e. ( Y ( Hom ` D ) Z ) )
28	16 17 18 4 21 22 23 25 27	comfval	\|- ( ph -> ( G ( <. X , Y >. ( comf ` D ) Z ) F ) = ( G ( <. X , Y >. .xb Z ) F ) )
29	13 15 28	3eqtr3d	\|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G ( <. X , Y >. .xb Z ) F ) )

Metamath Proof Explorer

Theorem comfeqval

Proof