Metamath Proof Explorer

Theorem estrcco

Description: Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020)

Ref Expression
Hypotheses estrcbas.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
estrcbas.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
estrcco.o ⊢ · = ( comp ‘ 𝐶 )
estrcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
estrcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
estrcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
estrcco.a ⊢ 𝐴 = ( Base ‘ 𝑋 )
estrcco.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
estrcco.d ⊢ 𝐷 = ( Base ‘ 𝑍 )
estrcco.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
estrcco.g ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐷 )
Assertion estrcco ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 estrcbas.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2 estrcbas.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 estrcco.o ⊢ · = ( comp ‘ 𝐶 )
4 estrcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
5 estrcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
6 estrcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
7 estrcco.a ⊢ 𝐴 = ( Base ‘ 𝑋 )
8 estrcco.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
9 estrcco.d ⊢ 𝐷 = ( Base ‘ 𝑍 )
10 estrcco.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
11 estrcco.g ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐷 )
12 1 2 3 estrccofval ⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
13 fveq2 ⊢ ( 𝑧 = 𝑍 → ( Base ‘ 𝑧 ) = ( Base ‘ 𝑍 ) )
14 13 adantl ⊢ ( ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) → ( Base ‘ 𝑧 ) = ( Base ‘ 𝑍 ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( Base ‘ 𝑧 ) = ( Base ‘ 𝑍 ) )
16 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ )
17 16 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑣 ) = ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
18 op2ndg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
19 4 5 18 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
21 17 20 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑣 ) = 𝑌 )
22 21 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( Base ‘ ( 2nd ‘ 𝑣 ) ) = ( Base ‘ 𝑌 ) )
23 15 22 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) = ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) )
24 16 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ 𝑣 ) = ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
25 24 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( Base ‘ ( 1st ‘ 𝑣 ) ) = ( Base ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
26 op1stg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
27 4 5 26 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
28 27 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( Base ‘ 𝑋 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( Base ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( Base ‘ 𝑋 ) )
30 25 29 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( Base ‘ ( 1st ‘ 𝑣 ) ) = ( Base ‘ 𝑋 ) )
31 22 30 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) = ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
32 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∘ 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
33 23 31 32 mpoeq123dv ⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) , 𝑓 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
34 4 5 opelxpd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑈 × 𝑈 ) )
35 ovex ⊢ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ∈ V
36 ovex ⊢ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∈ V
37 35 36 mpoex ⊢ ( 𝑔 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) , 𝑓 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ∈ V
38 37 a1i ⊢ ( 𝜑 → ( 𝑔 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) , 𝑓 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ∈ V )
39 12 33 34 6 38 ovmpod ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) = ( 𝑔 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) , 𝑓 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
40 simpl ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) → 𝑔 = 𝐺 )
41 simpr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
42 40 41 coeq12d ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) → ( 𝑔 ∘ 𝑓 ) = ( 𝐺 ∘ 𝐹 ) )
43 42 adantl ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝑔 ∘ 𝑓 ) = ( 𝐺 ∘ 𝐹 ) )
44 8 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑌 ) )
45 44 eqcomd ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = 𝐵 )
46 9 a1i ⊢ ( 𝜑 → 𝐷 = ( Base ‘ 𝑍 ) )
47 46 eqcomd ⊢ ( 𝜑 → ( Base ‘ 𝑍 ) = 𝐷 )
48 45 47 feq23d ⊢ ( 𝜑 → ( 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) ↔ 𝐺 : 𝐵 ⟶ 𝐷 ) )
49 11 48 mpbird ⊢ ( 𝜑 → 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) )
50 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑍 ) ∈ V )
51 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) ∈ V )
52 50 51 elmapd ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ↔ 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) ) )
53 49 52 mpbird ⊢ ( 𝜑 → 𝐺 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) )
54 7 a1i ⊢ ( 𝜑 → 𝐴 = ( Base ‘ 𝑋 ) )
55 54 eqcomd ⊢ ( 𝜑 → ( Base ‘ 𝑋 ) = 𝐴 )
56 55 45 feq23d ⊢ ( 𝜑 → ( 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) )
57 10 56 mpbird ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
58 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑋 ) ∈ V )
59 51 58 elmapd ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ↔ 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) )
60 57 59 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
61 coexg ⊢ ( ( 𝐺 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) → ( 𝐺 ∘ 𝐹 ) ∈ V )
62 53 60 61 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ V )
63 39 43 53 60 62 ovmpod ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )