Metamath Proof Explorer

Theorem fucoaltvallem

Description: Lemma for fucoaltval . (Contributed by Zhi Wang, 14-Sep-2026) (New usage is discouraged.)

Ref Expression
Hypotheses fucoaltfunc.q ⊢ Q = C FuncCat E
fucoaltval.l No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
fucoaltval.c ⊢ φ → C ∈ Cat
fucoaltval.e ⊢ φ → E ∈ Cat
fucoaltval.k ⊢ φ → K ∈ Q Func Q
fucoaltval.f ⊢ φ → F ∈ C Func E
fucoaltval.g ⊢ φ → G ∈ C Func E
fucoaltval.a ⊢ φ → A ∈ F C Nat E G
fucoaltval.i ⊢ I = id func ⁡ C
fucoaltval.j ⊢ J = Id ⁡ C FuncCat C
fucoaltvallem.t ⊢ T = C FuncCat E × c C FuncCat C
Assertion fucoaltvallem ⊢ φ → A F I 2 nd ⁡ K ∘ func L G I J ⁡ I = F 2 nd ⁡ K G ⁡ A

Proof

Step Hyp Ref Expression
1 fucoaltfunc.q ⊢ Q = C FuncCat E
2 fucoaltval.l Could not format L = ( <. C , C >. o.F E ) : No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
3 fucoaltval.c ⊢ φ → C ∈ Cat
4 fucoaltval.e ⊢ φ → E ∈ Cat
5 fucoaltval.k ⊢ φ → K ∈ Q Func Q
6 fucoaltval.f ⊢ φ → F ∈ C Func E
7 fucoaltval.g ⊢ φ → G ∈ C Func E
8 fucoaltval.a ⊢ φ → A ∈ F C Nat E G
9 fucoaltval.i ⊢ I = id func ⁡ C
10 fucoaltval.j ⊢ J = Id ⁡ C FuncCat C
11 fucoaltvallem.t ⊢ T = C FuncCat E × c C FuncCat C
12 df-ov ⊢ A F I 2 nd ⁡ K ∘ func L G I J ⁡ I = F I 2 nd ⁡ K ∘ func L G I ⁡ A J ⁡ I
13 11 xpcfucbas ⊢ C Func E × C Func C = Base T
14 11 1 3 3 4 fucofunca Could not format ( ph -> ( <. C , C >. o.F E ) e. ( T Func Q ) ) : No typesetting found for |- ( ph -> ( <. C , C >. o.F E ) e. ( T Func Q ) ) with typecode |-
15 2 14 eqeltrid ⊢ φ → L ∈ T Func Q
16 9 idfucl ⊢ C ∈ Cat → I ∈ C Func C
17 3 16 syl ⊢ φ → I ∈ C Func C
18 6 17 opelxpd ⊢ φ → F I ∈ C Func E × C Func C
19 7 17 opelxpd ⊢ φ → G I ∈ C Func E × C Func C
20 eqid ⊢ Hom ⁡ T = Hom ⁡ T
21 eqid ⊢ C FuncCat C = C FuncCat C
22 21 fucbas ⊢ C Func C = Base C FuncCat C
23 eqid ⊢ C Nat C = C Nat C
24 21 23 fuchom ⊢ C Nat C = Hom ⁡ C FuncCat C
25 21 3 3 fuccat ⊢ φ → C FuncCat C ∈ Cat
26 22 24 10 25 17 catidcl ⊢ φ → J ⁡ I ∈ I C Nat C I
27 8 26 opelxpd ⊢ φ → A J ⁡ I ∈ F C Nat E G × I C Nat C I
28 11 6 17 7 17 20 xpcfuchom2 ⊢ φ → F I Hom ⁡ T G I = F C Nat E G × I C Nat C I
29 27 28 eleqtrrd ⊢ φ → A J ⁡ I ∈ F I Hom ⁡ T G I
30 13 15 5 18 19 20 29 cofu2 ⊢ φ → F I 2 nd ⁡ K ∘ func L G I ⁡ A J ⁡ I = 1 st ⁡ L ⁡ F I 2 nd ⁡ K 1 st ⁡ L ⁡ G I ⁡ F I 2 nd ⁡ L G I ⁡ A J ⁡ I
31 df-ov ⊢ F 1 st ⁡ L I = 1 st ⁡ L ⁡ F I
32 2 eqcomi Could not format ( <. C , C >. o.F E ) = L : No typesetting found for |- ( <. C , C >. o.F E ) = L with typecode |-
33 32 fveq2i Could not format ( 1st ` ( <. C , C >. o.F E ) ) = ( 1st ` L ) : No typesetting found for |- ( 1st ` ( <. C , C >. o.F E ) ) = ( 1st ` L ) with typecode |-
34 33 a1i Could not format ( ph -> ( 1st ` ( <. C , C >. o.F E ) ) = ( 1st ` L ) ) : No typesetting found for |- ( ph -> ( 1st ` ( <. C , C >. o.F E ) ) = ( 1st ` L ) ) with typecode |-
35 34 17 6 fuco11b ⊢ φ → F 1 st ⁡ L I = F ∘ func I
36 6 9 cofurid ⊢ φ → F ∘ func I = F
37 35 36 eqtrd ⊢ φ → F 1 st ⁡ L I = F
38 31 37 eqtr3id ⊢ φ → 1 st ⁡ L ⁡ F I = F
39 df-ov ⊢ G 1 st ⁡ L I = 1 st ⁡ L ⁡ G I
40 34 17 7 fuco11b ⊢ φ → G 1 st ⁡ L I = G ∘ func I
41 7 9 cofurid ⊢ φ → G ∘ func I = G
42 40 41 eqtrd ⊢ φ → G 1 st ⁡ L I = G
43 39 42 eqtr3id ⊢ φ → 1 st ⁡ L ⁡ G I = G
44 38 43 oveq12d ⊢ φ → 1 st ⁡ L ⁡ F I 2 nd ⁡ K 1 st ⁡ L ⁡ G I = F 2 nd ⁡ K G
45 df-ov ⊢ A F I 2 nd ⁡ L G I J ⁡ I = F I 2 nd ⁡ L G I ⁡ A J ⁡ I
46 32 fveq2i Could not format ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) : No typesetting found for |- ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) with typecode |-
47 46 a1i Could not format ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) ) : No typesetting found for |- ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) ) with typecode |-
48 47 21 10 9 3 8 fucoridid ⊢ φ → A F I 2 nd ⁡ L G I J ⁡ I = A
49 45 48 eqtr3id ⊢ φ → F I 2 nd ⁡ L G I ⁡ A J ⁡ I = A
50 44 49 fveq12d ⊢ φ → 1 st ⁡ L ⁡ F I 2 nd ⁡ K 1 st ⁡ L ⁡ G I ⁡ F I 2 nd ⁡ L G I ⁡ A J ⁡ I = F 2 nd ⁡ K G ⁡ A
51 30 50 eqtrd ⊢ φ → F I 2 nd ⁡ K ∘ func L G I ⁡ A J ⁡ I = F 2 nd ⁡ K G ⁡ A
52 12 51 eqtrid ⊢ φ → A F I 2 nd ⁡ K ∘ func L G I J ⁡ I = F 2 nd ⁡ K G ⁡ A