fucco

Description: Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucco.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucco.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fucco.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	fucco.o	⊢ · = ( comp ‘ 𝐷 )
	fucco.x	⊢ ∙ = ( comp ‘ 𝑄 )
	fucco.f	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
	fucco.g	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
Assertion	fucco	⊢ ( 𝜑 → ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucco.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fucco.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3		fucco.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
4		fucco.o	⊢ · = ( comp ‘ 𝐷 )
5		fucco.x	⊢ ∙ = ( comp ‘ 𝑄 )
6		fucco.f	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
7		fucco.g	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
8		eqid	⊢ ( 𝐶 Func 𝐷 ) = ( 𝐶 Func 𝐷 )
9	2	natrcl	⊢ ( 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
10	6 9	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
11	10	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
12		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
13	11 12	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
14	13	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
15	13	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
16	1 8 2 3 4 14 15 5	fuccofval	⊢ ( 𝜑 → ∙ = ( 𝑣 ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
17		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) → ( 1^st ‘ 𝑣 ) ∈ V )
18		simprl	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) → 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ )
19	18	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) → ( 1^st ‘ 𝑣 ) = ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
20		op1stg	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
21	10 20	syl	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
22	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
23	19 22	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) → ( 1^st ‘ 𝑣 ) = 𝐹 )
24		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2^nd ‘ 𝑣 ) ∈ V )
25	18	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ )
26	25	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2^nd ‘ 𝑣 ) = ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
27		op2ndg	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
28	10 27	syl	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
29	28	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
30	26 29	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2^nd ‘ 𝑣 ) = 𝐺 )
31		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
32		simprr	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) → ℎ = 𝐻 )
33	32	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ℎ = 𝐻 )
34	31 33	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑔 𝑁 ℎ ) = ( 𝐺 𝑁 𝐻 ) )
35		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
36	35 31	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 𝑁 𝑔 ) = ( 𝐹 𝑁 𝐺 ) )
37	35	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 1^st ‘ 𝑓 ) = ( 1^st ‘ 𝐹 ) )
38	37	fveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) )
39	31	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 1^st ‘ 𝑔 ) = ( 1^st ‘ 𝐺 ) )
40	39	fveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) )
41	38 40	opeq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ )
42	33	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 1^st ‘ ℎ ) = ( 1^st ‘ 𝐻 ) )
43	42	fveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) )
44	41 43	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
45	44	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) = ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) )
46	45	mpteq2dv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
47	34 36 46	mpoeq123dv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
48	24 30 47	csbied2	⊢ ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
49	17 23 48	csbied2	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ ℎ = 𝐻 ) ) → ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
50		opelxpi	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) )
51	10 50	syl	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) )
52	2	natrcl	⊢ ( 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) )
53	7 52	syl	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) )
54	53	simprd	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐶 Func 𝐷 ) )
55		ovex	⊢ ( 𝐺 𝑁 𝐻 ) ∈ V
56		ovex	⊢ ( 𝐹 𝑁 𝐺 ) ∈ V
57	55 56	mpoex	⊢ ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ V
58	57	a1i	⊢ ( 𝜑 → ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ V )
59	16 49 51 54 58	ovmpod	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
60		simprl	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → 𝑏 = 𝑆 )
61	60	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → ( 𝑏 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
62		simprr	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → 𝑎 = 𝑅 )
63	62	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑥 ) )
64	61 63	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) = ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) )
65	64	mpteq2dv	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝑆 ∧ 𝑎 = 𝑅 ) ) → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
66	3	fvexi	⊢ 𝐴 ∈ V
67	66	mptex	⊢ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) ∈ V
68	67	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) ∈ V )
69	59 65 7 6 68	ovmpod	⊢ ( 𝜑 → ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem fucco

Proof