Metamath Proof Explorer

Theorem sectco

Description: Composition of two sections. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses sectco.b 
|- B = ( Base ` C )
sectco.o 
|- .x. = ( comp ` C )
sectco.s 
|- S = ( Sect ` C )
sectco.c 
|- ( ph -> C e. Cat )
sectco.x 
|- ( ph -> X e. B )
sectco.y 
|- ( ph -> Y e. B )
sectco.z 
|- ( ph -> Z e. B )
sectco.1 
|- ( ph -> F ( X S Y ) G )
sectco.2 
|- ( ph -> H ( Y S Z ) K )
Assertion sectco 
|- ( ph -> ( H ( <. X , Y >. .x. Z ) F ) ( X S Z ) ( G ( <. Z , Y >. .x. X ) K ) )

Proof

Step Hyp Ref Expression
1 sectco.b 
 |-  B = ( Base ` C )
2 sectco.o 
 |-  .x. = ( comp ` C )
3 sectco.s 
 |-  S = ( Sect ` C )
4 sectco.c 
 |-  ( ph -> C e. Cat )
5 sectco.x 
 |-  ( ph -> X e. B )
6 sectco.y 
 |-  ( ph -> Y e. B )
7 sectco.z 
 |-  ( ph -> Z e. B )
8 sectco.1 
 |-  ( ph -> F ( X S Y ) G )
9 sectco.2 
 |-  ( ph -> H ( Y S Z ) K )
10 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
11 eqid 
 |-  ( Id ` C ) = ( Id ` C )
12 1 10 2 11 3 4 5 6 issect 
 |-  ( ph -> ( F ( X S Y ) G <-> ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) /\ ( G ( <. X , Y >. .x. X ) F ) = ( ( Id ` C ) ` X ) ) ) )
13 8 12 mpbid 
 |-  ( ph -> ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) /\ ( G ( <. X , Y >. .x. X ) F ) = ( ( Id ` C ) ` X ) ) )
14 13 simp1d 
 |-  ( ph -> F e. ( X ( Hom ` C ) Y ) )
15 1 10 2 11 3 4 6 7 issect 
 |-  ( ph -> ( H ( Y S Z ) K <-> ( H e. ( Y ( Hom ` C ) Z ) /\ K e. ( Z ( Hom ` C ) Y ) /\ ( K ( <. Y , Z >. .x. Y ) H ) = ( ( Id ` C ) ` Y ) ) ) )
16 9 15 mpbid 
 |-  ( ph -> ( H e. ( Y ( Hom ` C ) Z ) /\ K e. ( Z ( Hom ` C ) Y ) /\ ( K ( <. Y , Z >. .x. Y ) H ) = ( ( Id ` C ) ` Y ) ) )
17 16 simp1d 
 |-  ( ph -> H e. ( Y ( Hom ` C ) Z ) )
18 1 10 2 4 5 6 7 14 17 catcocl 
 |-  ( ph -> ( H ( <. X , Y >. .x. Z ) F ) e. ( X ( Hom ` C ) Z ) )
19 16 simp2d 
 |-  ( ph -> K e. ( Z ( Hom ` C ) Y ) )
20 13 simp2d 
 |-  ( ph -> G e. ( Y ( Hom ` C ) X ) )
21 1 10 2 4 5 7 6 18 19 5 20 catass 
 |-  ( ph -> ( ( G ( <. Z , Y >. .x. X ) K ) ( <. X , Z >. .x. X ) ( H ( <. X , Y >. .x. Z ) F ) ) = ( G ( <. X , Y >. .x. X ) ( K ( <. X , Z >. .x. Y ) ( H ( <. X , Y >. .x. Z ) F ) ) ) )
22 16 simp3d 
 |-  ( ph -> ( K ( <. Y , Z >. .x. Y ) H ) = ( ( Id ` C ) ` Y ) )
23 22 oveq1d 
 |-  ( ph -> ( ( K ( <. Y , Z >. .x. Y ) H ) ( <. X , Y >. .x. Y ) F ) = ( ( ( Id ` C ) ` Y ) ( <. X , Y >. .x. Y ) F ) )
24 1 10 2 4 5 6 7 14 17 6 19 catass 
 |-  ( ph -> ( ( K ( <. Y , Z >. .x. Y ) H ) ( <. X , Y >. .x. Y ) F ) = ( K ( <. X , Z >. .x. Y ) ( H ( <. X , Y >. .x. Z ) F ) ) )
25 1 10 11 4 5 2 6 14 catlid 
 |-  ( ph -> ( ( ( Id ` C ) ` Y ) ( <. X , Y >. .x. Y ) F ) = F )
26 23 24 25 3eqtr3d 
 |-  ( ph -> ( K ( <. X , Z >. .x. Y ) ( H ( <. X , Y >. .x. Z ) F ) ) = F )
27 26 oveq2d 
 |-  ( ph -> ( G ( <. X , Y >. .x. X ) ( K ( <. X , Z >. .x. Y ) ( H ( <. X , Y >. .x. Z ) F ) ) ) = ( G ( <. X , Y >. .x. X ) F ) )
28 13 simp3d 
 |-  ( ph -> ( G ( <. X , Y >. .x. X ) F ) = ( ( Id ` C ) ` X ) )
29 21 27 28 3eqtrd 
 |-  ( ph -> ( ( G ( <. Z , Y >. .x. X ) K ) ( <. X , Z >. .x. X ) ( H ( <. X , Y >. .x. Z ) F ) ) = ( ( Id ` C ) ` X ) )
30 1 10 2 4 7 6 5 19 20 catcocl 
 |-  ( ph -> ( G ( <. Z , Y >. .x. X ) K ) e. ( Z ( Hom ` C ) X ) )
31 1 10 2 11 3 4 5 7 18 30 issect2 
 |-  ( ph -> ( ( H ( <. X , Y >. .x. Z ) F ) ( X S Z ) ( G ( <. Z , Y >. .x. X ) K ) <-> ( ( G ( <. Z , Y >. .x. X ) K ) ( <. X , Z >. .x. X ) ( H ( <. X , Y >. .x. Z ) F ) ) = ( ( Id ` C ) ` X ) ) )
32 29 31 mpbird 
 |-  ( ph -> ( H ( <. X , Y >. .x. Z ) F ) ( X S Z ) ( G ( <. Z , Y >. .x. X ) K ) )