Step | Hyp | Ref
| Expression |
1 | | comfffval.o |
. . . 4
โข ๐ =
(compfโ๐ถ) |
2 | | comfffval.b |
. . . 4
โข ๐ต = (Baseโ๐ถ) |
3 | | comfffval.h |
. . . 4
โข ๐ป = (Hom โ๐ถ) |
4 | | comfffval.x |
. . . 4
โข ยท =
(compโ๐ถ) |
5 | 1, 2, 3, 4 | comfffval 17538 |
. . 3
โข ๐ = (๐ฅ โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ฅ)๐ป๐ง), ๐ โ (๐ปโ๐ฅ) โฆ (๐(๐ฅ ยท ๐ง)๐))) |
6 | 5 | a1i 11 |
. 2
โข (๐ โ ๐ = (๐ฅ โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ฅ)๐ป๐ง), ๐ โ (๐ปโ๐ฅ) โฆ (๐(๐ฅ ยท ๐ง)๐)))) |
7 | | simprl 769 |
. . . . . 6
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ ๐ฅ = โจ๐, ๐โฉ) |
8 | 7 | fveq2d 6843 |
. . . . 5
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ (2nd โ๐ฅ) = (2nd
โโจ๐, ๐โฉ)) |
9 | | comffval.x |
. . . . . . 7
โข (๐ โ ๐ โ ๐ต) |
10 | | comffval.y |
. . . . . . 7
โข (๐ โ ๐ โ ๐ต) |
11 | | op2ndg 7926 |
. . . . . . 7
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (2nd โโจ๐, ๐โฉ) = ๐) |
12 | 9, 10, 11 | syl2anc 584 |
. . . . . 6
โข (๐ โ (2nd
โโจ๐, ๐โฉ) = ๐) |
13 | 12 | adantr 481 |
. . . . 5
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ (2nd โโจ๐, ๐โฉ) = ๐) |
14 | 8, 13 | eqtrd 2777 |
. . . 4
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ (2nd โ๐ฅ) = ๐) |
15 | | simprr 771 |
. . . 4
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ ๐ง = ๐) |
16 | 14, 15 | oveq12d 7369 |
. . 3
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ ((2nd โ๐ฅ)๐ป๐ง) = (๐๐ป๐)) |
17 | 7 | fveq2d 6843 |
. . . 4
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ (๐ปโ๐ฅ) = (๐ปโโจ๐, ๐โฉ)) |
18 | | df-ov 7354 |
. . . 4
โข (๐๐ป๐) = (๐ปโโจ๐, ๐โฉ) |
19 | 17, 18 | eqtr4di 2795 |
. . 3
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ (๐ปโ๐ฅ) = (๐๐ป๐)) |
20 | 7, 15 | oveq12d 7369 |
. . . 4
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ (๐ฅ ยท ๐ง) = (โจ๐, ๐โฉ ยท ๐)) |
21 | 20 | oveqd 7368 |
. . 3
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ (๐(๐ฅ ยท ๐ง)๐) = (๐(โจ๐, ๐โฉ ยท ๐)๐)) |
22 | 16, 19, 21 | mpoeq123dv 7426 |
. 2
โข ((๐ โง (๐ฅ = โจ๐, ๐โฉ โง ๐ง = ๐)) โ (๐ โ ((2nd โ๐ฅ)๐ป๐ง), ๐ โ (๐ปโ๐ฅ) โฆ (๐(๐ฅ ยท ๐ง)๐)) = (๐ โ (๐๐ป๐), ๐ โ (๐๐ป๐) โฆ (๐(โจ๐, ๐โฉ ยท ๐)๐))) |
23 | 9, 10 | opelxpd 5669 |
. 2
โข (๐ โ โจ๐, ๐โฉ โ (๐ต ร ๐ต)) |
24 | | comffval.z |
. 2
โข (๐ โ ๐ โ ๐ต) |
25 | | ovex 7384 |
. . . 4
โข (๐๐ป๐) โ V |
26 | | ovex 7384 |
. . . 4
โข (๐๐ป๐) โ V |
27 | 25, 26 | mpoex 8004 |
. . 3
โข (๐ โ (๐๐ป๐), ๐ โ (๐๐ป๐) โฆ (๐(โจ๐, ๐โฉ ยท ๐)๐)) โ V |
28 | 27 | a1i 11 |
. 2
โข (๐ โ (๐ โ (๐๐ป๐), ๐ โ (๐๐ป๐) โฆ (๐(โจ๐, ๐โฉ ยท ๐)๐)) โ V) |
29 | 6, 22, 23, 24, 28 | ovmpod 7501 |
1
โข (๐ โ (โจ๐, ๐โฉ๐๐) = (๐ โ (๐๐ป๐), ๐ โ (๐๐ป๐) โฆ (๐(โจ๐, ๐โฉ ยท ๐)๐))) |