Step | Hyp | Ref
| Expression |
1 | | xpcco2.t |
. . 3
โข ๐ = (๐ถ รc ๐ท) |
2 | | xpcco2.x |
. . . 4
โข ๐ = (Baseโ๐ถ) |
3 | | xpcco2.y |
. . . 4
โข ๐ = (Baseโ๐ท) |
4 | 1, 2, 3 | xpcbas 18071 |
. . 3
โข (๐ ร ๐) = (Baseโ๐) |
5 | | eqid 2733 |
. . 3
โข (Hom
โ๐) = (Hom
โ๐) |
6 | | xpcco2.o1 |
. . 3
โข ยท =
(compโ๐ถ) |
7 | | xpcco2.o2 |
. . 3
โข โ =
(compโ๐ท) |
8 | | xpcco2.o |
. . 3
โข ๐ = (compโ๐) |
9 | | xpcco2.m |
. . . 4
โข (๐ โ ๐ โ ๐) |
10 | | xpcco2.n |
. . . 4
โข (๐ โ ๐ โ ๐) |
11 | 9, 10 | opelxpd 5672 |
. . 3
โข (๐ โ โจ๐, ๐โฉ โ (๐ ร ๐)) |
12 | | xpcco2.p |
. . . 4
โข (๐ โ ๐ โ ๐) |
13 | | xpcco2.q |
. . . 4
โข (๐ โ ๐ โ ๐) |
14 | 12, 13 | opelxpd 5672 |
. . 3
โข (๐ โ โจ๐, ๐โฉ โ (๐ ร ๐)) |
15 | | xpcco2.r |
. . . 4
โข (๐ โ ๐
โ ๐) |
16 | | xpcco2.s |
. . . 4
โข (๐ โ ๐ โ ๐) |
17 | 15, 16 | opelxpd 5672 |
. . 3
โข (๐ โ โจ๐
, ๐โฉ โ (๐ ร ๐)) |
18 | | xpcco2.f |
. . . . 5
โข (๐ โ ๐น โ (๐๐ป๐)) |
19 | | xpcco2.g |
. . . . 5
โข (๐ โ ๐บ โ (๐๐ฝ๐)) |
20 | 18, 19 | opelxpd 5672 |
. . . 4
โข (๐ โ โจ๐น, ๐บโฉ โ ((๐๐ป๐) ร (๐๐ฝ๐))) |
21 | | xpcco2.h |
. . . . 5
โข ๐ป = (Hom โ๐ถ) |
22 | | xpcco2.j |
. . . . 5
โข ๐ฝ = (Hom โ๐ท) |
23 | 1, 2, 3, 21, 22, 9, 10, 12, 13, 5 | xpchom2 18079 |
. . . 4
โข (๐ โ (โจ๐, ๐โฉ(Hom โ๐)โจ๐, ๐โฉ) = ((๐๐ป๐) ร (๐๐ฝ๐))) |
24 | 20, 23 | eleqtrrd 2837 |
. . 3
โข (๐ โ โจ๐น, ๐บโฉ โ (โจ๐, ๐โฉ(Hom โ๐)โจ๐, ๐โฉ)) |
25 | | xpcco2.k |
. . . . 5
โข (๐ โ ๐พ โ (๐๐ป๐
)) |
26 | | xpcco2.l |
. . . . 5
โข (๐ โ ๐ฟ โ (๐๐ฝ๐)) |
27 | 25, 26 | opelxpd 5672 |
. . . 4
โข (๐ โ โจ๐พ, ๐ฟโฉ โ ((๐๐ป๐
) ร (๐๐ฝ๐))) |
28 | 1, 2, 3, 21, 22, 12, 13, 15, 16, 5 | xpchom2 18079 |
. . . 4
โข (๐ โ (โจ๐, ๐โฉ(Hom โ๐)โจ๐
, ๐โฉ) = ((๐๐ป๐
) ร (๐๐ฝ๐))) |
29 | 27, 28 | eleqtrrd 2837 |
. . 3
โข (๐ โ โจ๐พ, ๐ฟโฉ โ (โจ๐, ๐โฉ(Hom โ๐)โจ๐
, ๐โฉ)) |
30 | 1, 4, 5, 6, 7, 8, 11, 14, 17, 24, 29 | xpcco 18076 |
. 2
โข (๐ โ (โจ๐พ, ๐ฟโฉ(โจโจ๐, ๐โฉ, โจ๐, ๐โฉโฉ๐โจ๐
, ๐โฉ)โจ๐น, ๐บโฉ) = โจ((1st
โโจ๐พ, ๐ฟโฉ)(โจ(1st
โโจ๐, ๐โฉ), (1st
โโจ๐, ๐โฉ)โฉ ยท (1st
โโจ๐
, ๐โฉ))(1st
โโจ๐น, ๐บโฉ)), ((2nd
โโจ๐พ, ๐ฟโฉ)(โจ(2nd
โโจ๐, ๐โฉ), (2nd
โโจ๐, ๐โฉ)โฉ โ (2nd
โโจ๐
, ๐โฉ))(2nd
โโจ๐น, ๐บโฉ))โฉ) |
31 | | op1stg 7934 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ โ ๐) โ (1st โโจ๐, ๐โฉ) = ๐) |
32 | 9, 10, 31 | syl2anc 585 |
. . . . . 6
โข (๐ โ (1st
โโจ๐, ๐โฉ) = ๐) |
33 | | op1stg 7934 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ โ ๐) โ (1st โโจ๐, ๐โฉ) = ๐) |
34 | 12, 13, 33 | syl2anc 585 |
. . . . . 6
โข (๐ โ (1st
โโจ๐, ๐โฉ) = ๐) |
35 | 32, 34 | opeq12d 4839 |
. . . . 5
โข (๐ โ โจ(1st
โโจ๐, ๐โฉ), (1st
โโจ๐, ๐โฉ)โฉ = โจ๐, ๐โฉ) |
36 | | op1stg 7934 |
. . . . . 6
โข ((๐
โ ๐ โง ๐ โ ๐) โ (1st โโจ๐
, ๐โฉ) = ๐
) |
37 | 15, 16, 36 | syl2anc 585 |
. . . . 5
โข (๐ โ (1st
โโจ๐
, ๐โฉ) = ๐
) |
38 | 35, 37 | oveq12d 7376 |
. . . 4
โข (๐ โ (โจ(1st
โโจ๐, ๐โฉ), (1st
โโจ๐, ๐โฉ)โฉ ยท (1st
โโจ๐
, ๐โฉ)) = (โจ๐, ๐โฉ ยท ๐
)) |
39 | | op1stg 7934 |
. . . . 5
โข ((๐พ โ (๐๐ป๐
) โง ๐ฟ โ (๐๐ฝ๐)) โ (1st โโจ๐พ, ๐ฟโฉ) = ๐พ) |
40 | 25, 26, 39 | syl2anc 585 |
. . . 4
โข (๐ โ (1st
โโจ๐พ, ๐ฟโฉ) = ๐พ) |
41 | | op1stg 7934 |
. . . . 5
โข ((๐น โ (๐๐ป๐) โง ๐บ โ (๐๐ฝ๐)) โ (1st โโจ๐น, ๐บโฉ) = ๐น) |
42 | 18, 19, 41 | syl2anc 585 |
. . . 4
โข (๐ โ (1st
โโจ๐น, ๐บโฉ) = ๐น) |
43 | 38, 40, 42 | oveq123d 7379 |
. . 3
โข (๐ โ ((1st
โโจ๐พ, ๐ฟโฉ)(โจ(1st
โโจ๐, ๐โฉ), (1st
โโจ๐, ๐โฉ)โฉ ยท (1st
โโจ๐
, ๐โฉ))(1st
โโจ๐น, ๐บโฉ)) = (๐พ(โจ๐, ๐โฉ ยท ๐
)๐น)) |
44 | | op2ndg 7935 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ โ ๐) โ (2nd โโจ๐, ๐โฉ) = ๐) |
45 | 9, 10, 44 | syl2anc 585 |
. . . . . 6
โข (๐ โ (2nd
โโจ๐, ๐โฉ) = ๐) |
46 | | op2ndg 7935 |
. . . . . . 7
โข ((๐ โ ๐ โง ๐ โ ๐) โ (2nd โโจ๐, ๐โฉ) = ๐) |
47 | 12, 13, 46 | syl2anc 585 |
. . . . . 6
โข (๐ โ (2nd
โโจ๐, ๐โฉ) = ๐) |
48 | 45, 47 | opeq12d 4839 |
. . . . 5
โข (๐ โ โจ(2nd
โโจ๐, ๐โฉ), (2nd
โโจ๐, ๐โฉ)โฉ = โจ๐, ๐โฉ) |
49 | | op2ndg 7935 |
. . . . . 6
โข ((๐
โ ๐ โง ๐ โ ๐) โ (2nd โโจ๐
, ๐โฉ) = ๐) |
50 | 15, 16, 49 | syl2anc 585 |
. . . . 5
โข (๐ โ (2nd
โโจ๐
, ๐โฉ) = ๐) |
51 | 48, 50 | oveq12d 7376 |
. . . 4
โข (๐ โ (โจ(2nd
โโจ๐, ๐โฉ), (2nd
โโจ๐, ๐โฉ)โฉ โ (2nd
โโจ๐
, ๐โฉ)) = (โจ๐, ๐โฉ โ ๐)) |
52 | | op2ndg 7935 |
. . . . 5
โข ((๐พ โ (๐๐ป๐
) โง ๐ฟ โ (๐๐ฝ๐)) โ (2nd โโจ๐พ, ๐ฟโฉ) = ๐ฟ) |
53 | 25, 26, 52 | syl2anc 585 |
. . . 4
โข (๐ โ (2nd
โโจ๐พ, ๐ฟโฉ) = ๐ฟ) |
54 | | op2ndg 7935 |
. . . . 5
โข ((๐น โ (๐๐ป๐) โง ๐บ โ (๐๐ฝ๐)) โ (2nd โโจ๐น, ๐บโฉ) = ๐บ) |
55 | 18, 19, 54 | syl2anc 585 |
. . . 4
โข (๐ โ (2nd
โโจ๐น, ๐บโฉ) = ๐บ) |
56 | 51, 53, 55 | oveq123d 7379 |
. . 3
โข (๐ โ ((2nd
โโจ๐พ, ๐ฟโฉ)(โจ(2nd
โโจ๐, ๐โฉ), (2nd
โโจ๐, ๐โฉ)โฉ โ (2nd
โโจ๐
, ๐โฉ))(2nd
โโจ๐น, ๐บโฉ)) = (๐ฟ(โจ๐, ๐โฉ โ ๐)๐บ)) |
57 | 43, 56 | opeq12d 4839 |
. 2
โข (๐ โ โจ((1st
โโจ๐พ, ๐ฟโฉ)(โจ(1st
โโจ๐, ๐โฉ), (1st
โโจ๐, ๐โฉ)โฉ ยท (1st
โโจ๐
, ๐โฉ))(1st
โโจ๐น, ๐บโฉ)), ((2nd
โโจ๐พ, ๐ฟโฉ)(โจ(2nd
โโจ๐, ๐โฉ), (2nd
โโจ๐, ๐โฉ)โฉ โ (2nd
โโจ๐
, ๐โฉ))(2nd
โโจ๐น, ๐บโฉ))โฉ = โจ(๐พ(โจ๐, ๐โฉ ยท ๐
)๐น), (๐ฟ(โจ๐, ๐โฉ โ ๐)๐บ)โฉ) |
58 | 30, 57 | eqtrd 2773 |
1
โข (๐ โ (โจ๐พ, ๐ฟโฉ(โจโจ๐, ๐โฉ, โจ๐, ๐โฉโฉ๐โจ๐
, ๐โฉ)โจ๐น, ๐บโฉ) = โจ(๐พ(โจ๐, ๐โฉ ยท ๐
)๐น), (๐ฟ(โจ๐, ๐โฉ โ ๐)๐บ)โฉ) |