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

Metamath Proof Explorer

Theorem cofuval2

Description: Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses cofuval2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
cofuval2.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
cofuval2.x ⊢ ( 𝜑 → 𝐻 ( 𝐷 Func 𝐸 ) 𝐾 )
Assertion cofuval2 ( 𝜑 → ( ⟨ 𝐻 , 𝐾 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐻 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ )

Proof

Step Hyp Ref Expression
1 cofuval2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 cofuval2.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3 cofuval2.x ⊢ ( 𝜑 → 𝐻 ( 𝐷 Func 𝐸 ) 𝐾 )
4 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
5 2 4 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
6 df-br ⊢ ( 𝐻 ( 𝐷 Func 𝐸 ) 𝐾 ↔ ⟨ 𝐻 , 𝐾 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
7 3 6 sylib ⊢ ( 𝜑 → ⟨ 𝐻 , 𝐾 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
8 1 5 7 cofuval ⊢ ( 𝜑 → ( ⟨ 𝐻 , 𝐾 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( ( 1st ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ) ) ⟩ )
9 relfunc ⊢ Rel ( 𝐷 Func 𝐸 )
10 brrelex12 ⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐻 ( 𝐷 Func 𝐸 ) 𝐾 ) → ( 𝐻 ∈ V ∧ 𝐾 ∈ V ) )
11 9 3 10 sylancr ⊢ ( 𝜑 → ( 𝐻 ∈ V ∧ 𝐾 ∈ V ) )
12 op1stg ⊢ ( ( 𝐻 ∈ V ∧ 𝐾 ∈ V ) → ( 1st ‘ ⟨ 𝐻 , 𝐾 ⟩ ) = 𝐻 )
13 11 12 syl ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐻 , 𝐾 ⟩ ) = 𝐻 )
14 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
15 brrelex12 ⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
16 14 2 15 sylancr ⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
17 op1stg ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
18 16 17 syl ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
19 13 18 coeq12d ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝐻 ∘ 𝐹 ) )
20 op2ndg ⊢ ( ( 𝐻 ∈ V ∧ 𝐾 ∈ V ) → ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) = 𝐾 )
21 11 20 syl ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) = 𝐾 )
22 21 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) = 𝐾 )
23 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
24 23 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
25 23 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
26 22 24 25 oveq123d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) )
27 op2ndg ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
28 16 27 syl ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
29 28 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
30 29 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
31 26 30 coeq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) )
32 31 mpoeq3dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) )
33 19 32 opeq12d ⊢ ( 𝜑 → ⟨ ( ( 1st ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ) ) ⟩ = ⟨ ( 𝐻 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ )
34 8 33 eqtrd ⊢ ( 𝜑 → ( ⟨ 𝐻 , 𝐾 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐻 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ )