Metamath Proof Explorer


Theorem xpcco2

Description: Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses xpcco2.t โŠข ๐‘‡ = ( ๐ถ ร—c ๐ท )
xpcco2.x โŠข ๐‘‹ = ( Base โ€˜ ๐ถ )
xpcco2.y โŠข ๐‘Œ = ( Base โ€˜ ๐ท )
xpcco2.h โŠข ๐ป = ( Hom โ€˜ ๐ถ )
xpcco2.j โŠข ๐ฝ = ( Hom โ€˜ ๐ท )
xpcco2.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ ๐‘‹ )
xpcco2.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ๐‘Œ )
xpcco2.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ ๐‘‹ )
xpcco2.q โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ ๐‘Œ )
xpcco2.o1 โŠข ยท = ( comp โ€˜ ๐ถ )
xpcco2.o2 โŠข โˆ™ = ( comp โ€˜ ๐ท )
xpcco2.o โŠข ๐‘‚ = ( comp โ€˜ ๐‘‡ )
xpcco2.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ ๐‘‹ )
xpcco2.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ ๐‘Œ )
xpcco2.f โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐‘€ ๐ป ๐‘ƒ ) )
xpcco2.g โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ ( ๐‘ ๐ฝ ๐‘„ ) )
xpcco2.k โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ ( ๐‘ƒ ๐ป ๐‘… ) )
xpcco2.l โŠข ( ๐œ‘ โ†’ ๐ฟ โˆˆ ( ๐‘„ ๐ฝ ๐‘† ) )
Assertion xpcco2 ( ๐œ‘ โ†’ ( โŸจ ๐พ , ๐ฟ โŸฉ ( โŸจ โŸจ ๐‘€ , ๐‘ โŸฉ , โŸจ ๐‘ƒ , ๐‘„ โŸฉ โŸฉ ๐‘‚ โŸจ ๐‘… , ๐‘† โŸฉ ) โŸจ ๐น , ๐บ โŸฉ ) = โŸจ ( ๐พ ( โŸจ ๐‘€ , ๐‘ƒ โŸฉ ยท ๐‘… ) ๐น ) , ( ๐ฟ ( โŸจ ๐‘ , ๐‘„ โŸฉ โˆ™ ๐‘† ) ๐บ ) โŸฉ )

Proof

Step Hyp Ref Expression
1 xpcco2.t โŠข ๐‘‡ = ( ๐ถ ร—c ๐ท )
2 xpcco2.x โŠข ๐‘‹ = ( Base โ€˜ ๐ถ )
3 xpcco2.y โŠข ๐‘Œ = ( Base โ€˜ ๐ท )
4 xpcco2.h โŠข ๐ป = ( Hom โ€˜ ๐ถ )
5 xpcco2.j โŠข ๐ฝ = ( Hom โ€˜ ๐ท )
6 xpcco2.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ ๐‘‹ )
7 xpcco2.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ๐‘Œ )
8 xpcco2.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ ๐‘‹ )
9 xpcco2.q โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ ๐‘Œ )
10 xpcco2.o1 โŠข ยท = ( comp โ€˜ ๐ถ )
11 xpcco2.o2 โŠข โˆ™ = ( comp โ€˜ ๐ท )
12 xpcco2.o โŠข ๐‘‚ = ( comp โ€˜ ๐‘‡ )
13 xpcco2.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ ๐‘‹ )
14 xpcco2.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ ๐‘Œ )
15 xpcco2.f โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐‘€ ๐ป ๐‘ƒ ) )
16 xpcco2.g โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ ( ๐‘ ๐ฝ ๐‘„ ) )
17 xpcco2.k โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ ( ๐‘ƒ ๐ป ๐‘… ) )
18 xpcco2.l โŠข ( ๐œ‘ โ†’ ๐ฟ โˆˆ ( ๐‘„ ๐ฝ ๐‘† ) )
19 1 2 3 xpcbas โŠข ( ๐‘‹ ร— ๐‘Œ ) = ( Base โ€˜ ๐‘‡ )
20 eqid โŠข ( Hom โ€˜ ๐‘‡ ) = ( Hom โ€˜ ๐‘‡ )
21 6 7 opelxpd โŠข ( ๐œ‘ โ†’ โŸจ ๐‘€ , ๐‘ โŸฉ โˆˆ ( ๐‘‹ ร— ๐‘Œ ) )
22 8 9 opelxpd โŠข ( ๐œ‘ โ†’ โŸจ ๐‘ƒ , ๐‘„ โŸฉ โˆˆ ( ๐‘‹ ร— ๐‘Œ ) )
23 13 14 opelxpd โŠข ( ๐œ‘ โ†’ โŸจ ๐‘… , ๐‘† โŸฉ โˆˆ ( ๐‘‹ ร— ๐‘Œ ) )
24 15 16 opelxpd โŠข ( ๐œ‘ โ†’ โŸจ ๐น , ๐บ โŸฉ โˆˆ ( ( ๐‘€ ๐ป ๐‘ƒ ) ร— ( ๐‘ ๐ฝ ๐‘„ ) ) )
25 1 2 3 4 5 6 7 8 9 20 xpchom2 โŠข ( ๐œ‘ โ†’ ( โŸจ ๐‘€ , ๐‘ โŸฉ ( Hom โ€˜ ๐‘‡ ) โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) = ( ( ๐‘€ ๐ป ๐‘ƒ ) ร— ( ๐‘ ๐ฝ ๐‘„ ) ) )
26 24 25 eleqtrrd โŠข ( ๐œ‘ โ†’ โŸจ ๐น , ๐บ โŸฉ โˆˆ ( โŸจ ๐‘€ , ๐‘ โŸฉ ( Hom โ€˜ ๐‘‡ ) โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) )
27 17 18 opelxpd โŠข ( ๐œ‘ โ†’ โŸจ ๐พ , ๐ฟ โŸฉ โˆˆ ( ( ๐‘ƒ ๐ป ๐‘… ) ร— ( ๐‘„ ๐ฝ ๐‘† ) ) )
28 1 2 3 4 5 8 9 13 14 20 xpchom2 โŠข ( ๐œ‘ โ†’ ( โŸจ ๐‘ƒ , ๐‘„ โŸฉ ( Hom โ€˜ ๐‘‡ ) โŸจ ๐‘… , ๐‘† โŸฉ ) = ( ( ๐‘ƒ ๐ป ๐‘… ) ร— ( ๐‘„ ๐ฝ ๐‘† ) ) )
29 27 28 eleqtrrd โŠข ( ๐œ‘ โ†’ โŸจ ๐พ , ๐ฟ โŸฉ โˆˆ ( โŸจ ๐‘ƒ , ๐‘„ โŸฉ ( Hom โ€˜ ๐‘‡ ) โŸจ ๐‘… , ๐‘† โŸฉ ) )
30 1 19 20 10 11 12 21 22 23 26 29 xpcco โŠข ( ๐œ‘ โ†’ ( โŸจ ๐พ , ๐ฟ โŸฉ ( โŸจ โŸจ ๐‘€ , ๐‘ โŸฉ , โŸจ ๐‘ƒ , ๐‘„ โŸฉ โŸฉ ๐‘‚ โŸจ ๐‘… , ๐‘† โŸฉ ) โŸจ ๐น , ๐บ โŸฉ ) = โŸจ ( ( 1st โ€˜ โŸจ ๐พ , ๐ฟ โŸฉ ) ( โŸจ ( 1st โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) , ( 1st โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) โŸฉ ยท ( 1st โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) ) ( 1st โ€˜ โŸจ ๐น , ๐บ โŸฉ ) ) , ( ( 2nd โ€˜ โŸจ ๐พ , ๐ฟ โŸฉ ) ( โŸจ ( 2nd โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) , ( 2nd โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) โŸฉ โˆ™ ( 2nd โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) ) ( 2nd โ€˜ โŸจ ๐น , ๐บ โŸฉ ) ) โŸฉ )
31 op1stg โŠข ( ( ๐‘€ โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ ๐‘Œ ) โ†’ ( 1st โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) = ๐‘€ )
32 6 7 31 syl2anc โŠข ( ๐œ‘ โ†’ ( 1st โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) = ๐‘€ )
33 op1stg โŠข ( ( ๐‘ƒ โˆˆ ๐‘‹ โˆง ๐‘„ โˆˆ ๐‘Œ ) โ†’ ( 1st โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) = ๐‘ƒ )
34 8 9 33 syl2anc โŠข ( ๐œ‘ โ†’ ( 1st โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) = ๐‘ƒ )
35 32 34 opeq12d โŠข ( ๐œ‘ โ†’ โŸจ ( 1st โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) , ( 1st โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) โŸฉ = โŸจ ๐‘€ , ๐‘ƒ โŸฉ )
36 op1stg โŠข ( ( ๐‘… โˆˆ ๐‘‹ โˆง ๐‘† โˆˆ ๐‘Œ ) โ†’ ( 1st โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) = ๐‘… )
37 13 14 36 syl2anc โŠข ( ๐œ‘ โ†’ ( 1st โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) = ๐‘… )
38 35 37 oveq12d โŠข ( ๐œ‘ โ†’ ( โŸจ ( 1st โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) , ( 1st โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) โŸฉ ยท ( 1st โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) ) = ( โŸจ ๐‘€ , ๐‘ƒ โŸฉ ยท ๐‘… ) )
39 op1stg โŠข ( ( ๐พ โˆˆ ( ๐‘ƒ ๐ป ๐‘… ) โˆง ๐ฟ โˆˆ ( ๐‘„ ๐ฝ ๐‘† ) ) โ†’ ( 1st โ€˜ โŸจ ๐พ , ๐ฟ โŸฉ ) = ๐พ )
40 17 18 39 syl2anc โŠข ( ๐œ‘ โ†’ ( 1st โ€˜ โŸจ ๐พ , ๐ฟ โŸฉ ) = ๐พ )
41 op1stg โŠข ( ( ๐น โˆˆ ( ๐‘€ ๐ป ๐‘ƒ ) โˆง ๐บ โˆˆ ( ๐‘ ๐ฝ ๐‘„ ) ) โ†’ ( 1st โ€˜ โŸจ ๐น , ๐บ โŸฉ ) = ๐น )
42 15 16 41 syl2anc โŠข ( ๐œ‘ โ†’ ( 1st โ€˜ โŸจ ๐น , ๐บ โŸฉ ) = ๐น )
43 38 40 42 oveq123d โŠข ( ๐œ‘ โ†’ ( ( 1st โ€˜ โŸจ ๐พ , ๐ฟ โŸฉ ) ( โŸจ ( 1st โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) , ( 1st โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) โŸฉ ยท ( 1st โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) ) ( 1st โ€˜ โŸจ ๐น , ๐บ โŸฉ ) ) = ( ๐พ ( โŸจ ๐‘€ , ๐‘ƒ โŸฉ ยท ๐‘… ) ๐น ) )
44 op2ndg โŠข ( ( ๐‘€ โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ ๐‘Œ ) โ†’ ( 2nd โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) = ๐‘ )
45 6 7 44 syl2anc โŠข ( ๐œ‘ โ†’ ( 2nd โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) = ๐‘ )
46 op2ndg โŠข ( ( ๐‘ƒ โˆˆ ๐‘‹ โˆง ๐‘„ โˆˆ ๐‘Œ ) โ†’ ( 2nd โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) = ๐‘„ )
47 8 9 46 syl2anc โŠข ( ๐œ‘ โ†’ ( 2nd โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) = ๐‘„ )
48 45 47 opeq12d โŠข ( ๐œ‘ โ†’ โŸจ ( 2nd โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) , ( 2nd โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) โŸฉ = โŸจ ๐‘ , ๐‘„ โŸฉ )
49 op2ndg โŠข ( ( ๐‘… โˆˆ ๐‘‹ โˆง ๐‘† โˆˆ ๐‘Œ ) โ†’ ( 2nd โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) = ๐‘† )
50 13 14 49 syl2anc โŠข ( ๐œ‘ โ†’ ( 2nd โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) = ๐‘† )
51 48 50 oveq12d โŠข ( ๐œ‘ โ†’ ( โŸจ ( 2nd โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) , ( 2nd โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) โŸฉ โˆ™ ( 2nd โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) ) = ( โŸจ ๐‘ , ๐‘„ โŸฉ โˆ™ ๐‘† ) )
52 op2ndg โŠข ( ( ๐พ โˆˆ ( ๐‘ƒ ๐ป ๐‘… ) โˆง ๐ฟ โˆˆ ( ๐‘„ ๐ฝ ๐‘† ) ) โ†’ ( 2nd โ€˜ โŸจ ๐พ , ๐ฟ โŸฉ ) = ๐ฟ )
53 17 18 52 syl2anc โŠข ( ๐œ‘ โ†’ ( 2nd โ€˜ โŸจ ๐พ , ๐ฟ โŸฉ ) = ๐ฟ )
54 op2ndg โŠข ( ( ๐น โˆˆ ( ๐‘€ ๐ป ๐‘ƒ ) โˆง ๐บ โˆˆ ( ๐‘ ๐ฝ ๐‘„ ) ) โ†’ ( 2nd โ€˜ โŸจ ๐น , ๐บ โŸฉ ) = ๐บ )
55 15 16 54 syl2anc โŠข ( ๐œ‘ โ†’ ( 2nd โ€˜ โŸจ ๐น , ๐บ โŸฉ ) = ๐บ )
56 51 53 55 oveq123d โŠข ( ๐œ‘ โ†’ ( ( 2nd โ€˜ โŸจ ๐พ , ๐ฟ โŸฉ ) ( โŸจ ( 2nd โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) , ( 2nd โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) โŸฉ โˆ™ ( 2nd โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) ) ( 2nd โ€˜ โŸจ ๐น , ๐บ โŸฉ ) ) = ( ๐ฟ ( โŸจ ๐‘ , ๐‘„ โŸฉ โˆ™ ๐‘† ) ๐บ ) )
57 43 56 opeq12d โŠข ( ๐œ‘ โ†’ โŸจ ( ( 1st โ€˜ โŸจ ๐พ , ๐ฟ โŸฉ ) ( โŸจ ( 1st โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) , ( 1st โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) โŸฉ ยท ( 1st โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) ) ( 1st โ€˜ โŸจ ๐น , ๐บ โŸฉ ) ) , ( ( 2nd โ€˜ โŸจ ๐พ , ๐ฟ โŸฉ ) ( โŸจ ( 2nd โ€˜ โŸจ ๐‘€ , ๐‘ โŸฉ ) , ( 2nd โ€˜ โŸจ ๐‘ƒ , ๐‘„ โŸฉ ) โŸฉ โˆ™ ( 2nd โ€˜ โŸจ ๐‘… , ๐‘† โŸฉ ) ) ( 2nd โ€˜ โŸจ ๐น , ๐บ โŸฉ ) ) โŸฉ = โŸจ ( ๐พ ( โŸจ ๐‘€ , ๐‘ƒ โŸฉ ยท ๐‘… ) ๐น ) , ( ๐ฟ ( โŸจ ๐‘ , ๐‘„ โŸฉ โˆ™ ๐‘† ) ๐บ ) โŸฉ )
58 30 57 eqtrd โŠข ( ๐œ‘ โ†’ ( โŸจ ๐พ , ๐ฟ โŸฉ ( โŸจ โŸจ ๐‘€ , ๐‘ โŸฉ , โŸจ ๐‘ƒ , ๐‘„ โŸฉ โŸฉ ๐‘‚ โŸจ ๐‘… , ๐‘† โŸฉ ) โŸจ ๐น , ๐บ โŸฉ ) = โŸจ ( ๐พ ( โŸจ ๐‘€ , ๐‘ƒ โŸฉ ยท ๐‘… ) ๐น ) , ( ๐ฟ ( โŸจ ๐‘ , ๐‘„ โŸฉ โˆ™ ๐‘† ) ๐บ ) โŸฉ )