Theorem coaval

Description: Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	homdmcoa.o	⊢ · = ( compa ‘ 𝐶 )
	homdmcoa.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
	homdmcoa.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	homdmcoa.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
	coaval.x	⊢ ∙ = ( comp ‘ 𝐶 )
Assertion	coaval	⊢ ( 𝜑 → ( 𝐺 · 𝐹 ) = ⟨ 𝑋 , 𝑍 , ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		homdmcoa.o	⊢ · = ( compa ‘ 𝐶 )
2		homdmcoa.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
3		homdmcoa.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4		homdmcoa.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
5		coaval.x	⊢ ∙ = ( comp ‘ 𝐶 )
6		eqid	⊢ ( Arrow ‘ 𝐶 ) = ( Arrow ‘ 𝐶 )
7	1 6 5	coafval	⊢ · = ( 𝑔 ∈ ( Arrow ‘ 𝐶 ) , 𝑓 ∈ { ℎ ∈ ( Arrow ‘ 𝐶 ) ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ↦ ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ∙ ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩ )
8	6 2	homarw	⊢ ( 𝑌 𝐻 𝑍 ) ⊆ ( Arrow ‘ 𝐶 )
9	8 4	sselid	⊢ ( 𝜑 → 𝐺 ∈ ( Arrow ‘ 𝐶 ) )
10		fveqeq2	⊢ ( ℎ = 𝐹 → ( ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) ↔ ( coda ‘ 𝐹 ) = ( doma ‘ 𝑔 ) ) )
11	6 2	homarw	⊢ ( 𝑋 𝐻 𝑌 ) ⊆ ( Arrow ‘ 𝐶 )
12	3	adantr	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
13	11 12	sselid	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝐹 ∈ ( Arrow ‘ 𝐶 ) )
14	2	homacd	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( coda ‘ 𝐹 ) = 𝑌 )
15	12 14	syl	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( coda ‘ 𝐹 ) = 𝑌 )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
17	16	fveq2d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( doma ‘ 𝑔 ) = ( doma ‘ 𝐺 ) )
18	4	adantr	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
19	2	homadm	⊢ ( 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) → ( doma ‘ 𝐺 ) = 𝑌 )
20	18 19	syl	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( doma ‘ 𝐺 ) = 𝑌 )
21	17 20	eqtrd	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( doma ‘ 𝑔 ) = 𝑌 )
22	15 21	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( coda ‘ 𝐹 ) = ( doma ‘ 𝑔 ) )
23	10 13 22	elrabd	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝐹 ∈ { ℎ ∈ ( Arrow ‘ 𝐶 ) ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } )
24		otex	⊢ ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ∙ ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩ ∈ V
25	24	a1i	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ∙ ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩ ∈ V )
26		simprr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
27	26	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( doma ‘ 𝑓 ) = ( doma ‘ 𝐹 ) )
28	2	homadm	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( doma ‘ 𝐹 ) = 𝑋 )
29	12 28	syl	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( doma ‘ 𝐹 ) = 𝑋 )
30	29	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( doma ‘ 𝐹 ) = 𝑋 )
31	27 30	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( doma ‘ 𝑓 ) = 𝑋 )
32	16	fveq2d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( coda ‘ 𝑔 ) = ( coda ‘ 𝐺 ) )
33	2	homacd	⊢ ( 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) → ( coda ‘ 𝐺 ) = 𝑍 )
34	18 33	syl	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( coda ‘ 𝐺 ) = 𝑍 )
35	32 34	eqtrd	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( coda ‘ 𝑔 ) = 𝑍 )
36	35	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( coda ‘ 𝑔 ) = 𝑍 )
37	21	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( doma ‘ 𝑔 ) = 𝑌 )
38	31 37	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
39	38 36	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ∙ ( coda ‘ 𝑔 ) ) = ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) )
40		simprl	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑔 = 𝐺 )
41	40	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 2nd ‘ 𝑔 ) = ( 2nd ‘ 𝐺 ) )
42	26	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 2nd ‘ 𝑓 ) = ( 2nd ‘ 𝐹 ) )
43	39 41 42	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ∙ ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) = ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) )
44	31 36 43	oteq123d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ∙ ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩ = ⟨ 𝑋 , 𝑍 , ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) ⟩ )
45	9 23 25 44	ovmpodv2	⊢ ( 𝜑 → ( · = ( 𝑔 ∈ ( Arrow ‘ 𝐶 ) , 𝑓 ∈ { ℎ ∈ ( Arrow ‘ 𝐶 ) ∣ ( coda ‘ ℎ ) = ( doma ‘ 𝑔 ) } ↦ ⟨ ( doma ‘ 𝑓 ) , ( coda ‘ 𝑔 ) , ( ( 2nd ‘ 𝑔 ) ( ⟨ ( doma ‘ 𝑓 ) , ( doma ‘ 𝑔 ) ⟩ ∙ ( coda ‘ 𝑔 ) ) ( 2nd ‘ 𝑓 ) ) ⟩ ) → ( 𝐺 · 𝐹 ) = ⟨ 𝑋 , 𝑍 , ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) ⟩ ) )
46	7 45	mpi	⊢ ( 𝜑 → ( 𝐺 · 𝐹 ) = ⟨ 𝑋 , 𝑍 , ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) ⟩ )