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 |
โข ( ๐ โ ( โจ ๐พ , ๐ฟ โฉ ( โจ โจ ๐ , ๐ โฉ , โจ ๐ , ๐ โฉ โฉ ๐ โจ ๐
, ๐ โฉ ) โจ ๐น , ๐บ โฉ ) = โจ ( ๐พ ( โจ ๐ , ๐ โฉ ยท ๐
) ๐น ) , ( ๐ฟ ( โจ ๐ , ๐ โฉ โ ๐ ) ๐บ ) โฉ ) |