Step | Hyp | Ref
| Expression |
1 | | comfeq.3 |
. . . . . 6
โข (๐ โ ๐ต = (Baseโ๐ถ)) |
2 | 1 | sqxpeqd 5663 |
. . . . 5
โข (๐ โ (๐ต ร ๐ต) = ((Baseโ๐ถ) ร (Baseโ๐ถ))) |
3 | | eqidd 2738 |
. . . . 5
โข (๐ โ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) = (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐))) |
4 | 2, 1, 3 | mpoeq123dv 7426 |
. . . 4
โข (๐ โ (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐))) = (๐ข โ ((Baseโ๐ถ) ร (Baseโ๐ถ)), ๐ง โ (Baseโ๐ถ) โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)))) |
5 | | eqid 2737 |
. . . . 5
โข
(compfโ๐ถ) = (compfโ๐ถ) |
6 | | eqid 2737 |
. . . . 5
โข
(Baseโ๐ถ) =
(Baseโ๐ถ) |
7 | | comfeq.h |
. . . . 5
โข ๐ป = (Hom โ๐ถ) |
8 | | comfeq.1 |
. . . . 5
โข ยท =
(compโ๐ถ) |
9 | 5, 6, 7, 8 | comfffval 17538 |
. . . 4
โข
(compfโ๐ถ) = (๐ข โ ((Baseโ๐ถ) ร (Baseโ๐ถ)), ๐ง โ (Baseโ๐ถ) โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐))) |
10 | 4, 9 | eqtr4di 2795 |
. . 3
โข (๐ โ (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐))) = (compfโ๐ถ)) |
11 | | eqid 2737 |
. . . . . . . 8
โข (Hom
โ๐ท) = (Hom
โ๐ท) |
12 | | comfeq.5 |
. . . . . . . . 9
โข (๐ โ (Homf
โ๐ถ) =
(Homf โ๐ท)) |
13 | 12 | 3ad2ant1 1133 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ (Homf
โ๐ถ) =
(Homf โ๐ท)) |
14 | | xp2nd 7946 |
. . . . . . . . . 10
โข (๐ข โ (๐ต ร ๐ต) โ (2nd โ๐ข) โ ๐ต) |
15 | 14 | 3ad2ant2 1134 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ (2nd โ๐ข) โ ๐ต) |
16 | 1 | 3ad2ant1 1133 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ ๐ต = (Baseโ๐ถ)) |
17 | 15, 16 | eleqtrd 2840 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ (2nd โ๐ข) โ (Baseโ๐ถ)) |
18 | | simp3 1138 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ ๐ง โ ๐ต) |
19 | 18, 16 | eleqtrd 2840 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ ๐ง โ (Baseโ๐ถ)) |
20 | 6, 7, 11, 13, 17, 19 | homfeqval 17537 |
. . . . . . 7
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ ((2nd โ๐ข)๐ป๐ง) = ((2nd โ๐ข)(Hom โ๐ท)๐ง)) |
21 | | xp1st 7945 |
. . . . . . . . . . . 12
โข (๐ข โ (๐ต ร ๐ต) โ (1st โ๐ข) โ ๐ต) |
22 | 21 | 3ad2ant2 1134 |
. . . . . . . . . . 11
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ (1st โ๐ข) โ ๐ต) |
23 | 22, 16 | eleqtrd 2840 |
. . . . . . . . . 10
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ (1st โ๐ข) โ (Baseโ๐ถ)) |
24 | 6, 7, 11, 13, 23, 17 | homfeqval 17537 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ ((1st โ๐ข)๐ป(2nd โ๐ข)) = ((1st โ๐ข)(Hom โ๐ท)(2nd โ๐ข))) |
25 | | df-ov 7354 |
. . . . . . . . 9
โข
((1st โ๐ข)๐ป(2nd โ๐ข)) = (๐ปโโจ(1st โ๐ข), (2nd โ๐ข)โฉ) |
26 | | df-ov 7354 |
. . . . . . . . 9
โข
((1st โ๐ข)(Hom โ๐ท)(2nd โ๐ข)) = ((Hom โ๐ท)โโจ(1st โ๐ข), (2nd โ๐ข)โฉ) |
27 | 24, 25, 26 | 3eqtr3g 2800 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ (๐ปโโจ(1st โ๐ข), (2nd โ๐ข)โฉ) = ((Hom โ๐ท)โโจ(1st
โ๐ข), (2nd
โ๐ข)โฉ)) |
28 | | 1st2nd2 7952 |
. . . . . . . . . 10
โข (๐ข โ (๐ต ร ๐ต) โ ๐ข = โจ(1st โ๐ข), (2nd โ๐ข)โฉ) |
29 | 28 | 3ad2ant2 1134 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ ๐ข = โจ(1st โ๐ข), (2nd โ๐ข)โฉ) |
30 | 29 | fveq2d 6843 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ (๐ปโ๐ข) = (๐ปโโจ(1st โ๐ข), (2nd โ๐ข)โฉ)) |
31 | 29 | fveq2d 6843 |
. . . . . . . 8
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ ((Hom โ๐ท)โ๐ข) = ((Hom โ๐ท)โโจ(1st โ๐ข), (2nd โ๐ข)โฉ)) |
32 | 27, 30, 31 | 3eqtr4d 2787 |
. . . . . . 7
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ (๐ปโ๐ข) = ((Hom โ๐ท)โ๐ข)) |
33 | | eqidd 2738 |
. . . . . . 7
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ (๐(๐ข โ ๐ง)๐) = (๐(๐ข โ ๐ง)๐)) |
34 | 20, 32, 33 | mpoeq123dv 7426 |
. . . . . 6
โข ((๐ โง ๐ข โ (๐ต ร ๐ต) โง ๐ง โ ๐ต) โ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐)) = (๐ โ ((2nd โ๐ข)(Hom โ๐ท)๐ง), ๐ โ ((Hom โ๐ท)โ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) |
35 | 34 | mpoeq3dva 7428 |
. . . . 5
โข (๐ โ (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) = (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)(Hom โ๐ท)๐ง), ๐ โ ((Hom โ๐ท)โ๐ข) โฆ (๐(๐ข โ ๐ง)๐)))) |
36 | | comfeq.4 |
. . . . . . 7
โข (๐ โ ๐ต = (Baseโ๐ท)) |
37 | 36 | sqxpeqd 5663 |
. . . . . 6
โข (๐ โ (๐ต ร ๐ต) = ((Baseโ๐ท) ร (Baseโ๐ท))) |
38 | | eqidd 2738 |
. . . . . 6
โข (๐ โ (๐ โ ((2nd โ๐ข)(Hom โ๐ท)๐ง), ๐ โ ((Hom โ๐ท)โ๐ข) โฆ (๐(๐ข โ ๐ง)๐)) = (๐ โ ((2nd โ๐ข)(Hom โ๐ท)๐ง), ๐ โ ((Hom โ๐ท)โ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) |
39 | 37, 36, 38 | mpoeq123dv 7426 |
. . . . 5
โข (๐ โ (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)(Hom โ๐ท)๐ง), ๐ โ ((Hom โ๐ท)โ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) = (๐ข โ ((Baseโ๐ท) ร (Baseโ๐ท)), ๐ง โ (Baseโ๐ท) โฆ (๐ โ ((2nd โ๐ข)(Hom โ๐ท)๐ง), ๐ โ ((Hom โ๐ท)โ๐ข) โฆ (๐(๐ข โ ๐ง)๐)))) |
40 | 35, 39 | eqtrd 2777 |
. . . 4
โข (๐ โ (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) = (๐ข โ ((Baseโ๐ท) ร (Baseโ๐ท)), ๐ง โ (Baseโ๐ท) โฆ (๐ โ ((2nd โ๐ข)(Hom โ๐ท)๐ง), ๐ โ ((Hom โ๐ท)โ๐ข) โฆ (๐(๐ข โ ๐ง)๐)))) |
41 | | eqid 2737 |
. . . . 5
โข
(compfโ๐ท) = (compfโ๐ท) |
42 | | eqid 2737 |
. . . . 5
โข
(Baseโ๐ท) =
(Baseโ๐ท) |
43 | | comfeq.2 |
. . . . 5
โข โ =
(compโ๐ท) |
44 | 41, 42, 11, 43 | comfffval 17538 |
. . . 4
โข
(compfโ๐ท) = (๐ข โ ((Baseโ๐ท) ร (Baseโ๐ท)), ๐ง โ (Baseโ๐ท) โฆ (๐ โ ((2nd โ๐ข)(Hom โ๐ท)๐ง), ๐ โ ((Hom โ๐ท)โ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) |
45 | 40, 44 | eqtr4di 2795 |
. . 3
โข (๐ โ (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) = (compfโ๐ท)) |
46 | 10, 45 | eqeq12d 2753 |
. 2
โข (๐ โ ((๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐))) = (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) โ
(compfโ๐ถ) = (compfโ๐ท))) |
47 | | ovex 7384 |
. . . . . 6
โข
((2nd โ๐ข)๐ป๐ง) โ V |
48 | | fvex 6852 |
. . . . . 6
โข (๐ปโ๐ข) โ V |
49 | 47, 48 | mpoex 8004 |
. . . . 5
โข (๐ โ ((2nd
โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) โ V |
50 | 49 | rgen2w 3067 |
. . . 4
โข
โ๐ข โ
(๐ต ร ๐ต)โ๐ง โ ๐ต (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) โ V |
51 | | mpo2eqb 7482 |
. . . 4
โข
(โ๐ข โ
(๐ต ร ๐ต)โ๐ง โ ๐ต (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) โ V โ ((๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐))) = (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) โ โ๐ข โ (๐ต ร ๐ต)โ๐ง โ ๐ต (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) = (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐)))) |
52 | 50, 51 | ax-mp 5 |
. . 3
โข ((๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐))) = (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) โ โ๐ข โ (๐ต ร ๐ต)โ๐ง โ ๐ต (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) = (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) |
53 | | vex 3447 |
. . . . . . . . 9
โข ๐ฅ โ V |
54 | | vex 3447 |
. . . . . . . . 9
โข ๐ฆ โ V |
55 | 53, 54 | op2ndd 7924 |
. . . . . . . 8
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ (2nd โ๐ข) = ๐ฆ) |
56 | 55 | oveq1d 7366 |
. . . . . . 7
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ ((2nd โ๐ข)๐ป๐ง) = (๐ฆ๐ป๐ง)) |
57 | | fveq2 6839 |
. . . . . . . . 9
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ (๐ปโ๐ข) = (๐ปโโจ๐ฅ, ๐ฆโฉ)) |
58 | | df-ov 7354 |
. . . . . . . . 9
โข (๐ฅ๐ป๐ฆ) = (๐ปโโจ๐ฅ, ๐ฆโฉ) |
59 | 57, 58 | eqtr4di 2795 |
. . . . . . . 8
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ (๐ปโ๐ข) = (๐ฅ๐ป๐ฆ)) |
60 | | oveq1 7358 |
. . . . . . . . . 10
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ (๐ข ยท ๐ง) = (โจ๐ฅ, ๐ฆโฉ ยท ๐ง)) |
61 | 60 | oveqd 7368 |
. . . . . . . . 9
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ (๐(๐ข ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐)) |
62 | | oveq1 7358 |
. . . . . . . . . 10
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ (๐ข โ ๐ง) = (โจ๐ฅ, ๐ฆโฉ โ ๐ง)) |
63 | 62 | oveqd 7368 |
. . . . . . . . 9
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ (๐(๐ข โ ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐)) |
64 | 61, 63 | eqeq12d 2753 |
. . . . . . . 8
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ ((๐(๐ข ยท ๐ง)๐) = (๐(๐ข โ ๐ง)๐) โ (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐))) |
65 | 59, 64 | raleqbidv 3317 |
. . . . . . 7
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ (โ๐ โ (๐ปโ๐ข)(๐(๐ข ยท ๐ง)๐) = (๐(๐ข โ ๐ง)๐) โ โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐))) |
66 | 56, 65 | raleqbidv 3317 |
. . . . . 6
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ (โ๐ โ ((2nd โ๐ข)๐ป๐ง)โ๐ โ (๐ปโ๐ข)(๐(๐ข ยท ๐ง)๐) = (๐(๐ข โ ๐ง)๐) โ โ๐ โ (๐ฆ๐ป๐ง)โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐))) |
67 | | ovex 7384 |
. . . . . . . 8
โข (๐(๐ข ยท ๐ง)๐) โ V |
68 | 67 | rgen2w 3067 |
. . . . . . 7
โข
โ๐ โ
((2nd โ๐ข)๐ป๐ง)โ๐ โ (๐ปโ๐ข)(๐(๐ข ยท ๐ง)๐) โ V |
69 | | mpo2eqb 7482 |
. . . . . . 7
โข
(โ๐ โ
((2nd โ๐ข)๐ป๐ง)โ๐ โ (๐ปโ๐ข)(๐(๐ข ยท ๐ง)๐) โ V โ ((๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) = (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐)) โ โ๐ โ ((2nd โ๐ข)๐ป๐ง)โ๐ โ (๐ปโ๐ข)(๐(๐ข ยท ๐ง)๐) = (๐(๐ข โ ๐ง)๐))) |
70 | 68, 69 | ax-mp 5 |
. . . . . 6
โข ((๐ โ ((2nd
โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) = (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐)) โ โ๐ โ ((2nd โ๐ข)๐ป๐ง)โ๐ โ (๐ปโ๐ข)(๐(๐ข ยท ๐ง)๐) = (๐(๐ข โ ๐ง)๐)) |
71 | | ralcom 3270 |
. . . . . 6
โข
(โ๐ โ
(๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐) โ โ๐ โ (๐ฆ๐ป๐ง)โ๐ โ (๐ฅ๐ป๐ฆ)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐)) |
72 | 66, 70, 71 | 3bitr4g 313 |
. . . . 5
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ ((๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) = (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐)) โ โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐))) |
73 | 72 | ralbidv 3172 |
. . . 4
โข (๐ข = โจ๐ฅ, ๐ฆโฉ โ (โ๐ง โ ๐ต (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) = (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐)) โ โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐))) |
74 | 73 | ralxp 5795 |
. . 3
โข
(โ๐ข โ
(๐ต ร ๐ต)โ๐ง โ ๐ต (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐)) = (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐)) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐)) |
75 | 52, 74 | bitri 274 |
. 2
โข ((๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข ยท ๐ง)๐))) = (๐ข โ (๐ต ร ๐ต), ๐ง โ ๐ต โฆ (๐ โ ((2nd โ๐ข)๐ป๐ง), ๐ โ (๐ปโ๐ข) โฆ (๐(๐ข โ ๐ง)๐))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐)) |
76 | 46, 75 | bitr3di 285 |
1
โข (๐ โ
((compfโ๐ถ) = (compfโ๐ท) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ฅ, ๐ฆโฉ โ ๐ง)๐))) |