Step | Hyp | Ref
| Expression |
1 | | unieq 4881 |
. . . . . . . . . . 11
โข (๐ฅ = โ
โ โช ๐ฅ =
โช โ
) |
2 | | uni0 4901 |
. . . . . . . . . . 11
โข โช โ
= โ
|
3 | 1, 2 | eqtrdi 2793 |
. . . . . . . . . 10
โข (๐ฅ = โ
โ โช ๐ฅ =
โ
) |
4 | 3 | ineq2d 4177 |
. . . . . . . . 9
โข (๐ฅ = โ
โ (๐ โฉ โช ๐ฅ) =
(๐ โฉ
โ
)) |
5 | | in0 4356 |
. . . . . . . . 9
โข (๐ โฉ โ
) =
โ
|
6 | 4, 5 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ฅ = โ
โ (๐ โฉ โช ๐ฅ) =
โ
) |
7 | 6 | fveq2d 6851 |
. . . . . . 7
โข (๐ฅ = โ
โ
(โฏโ(๐ โฉ
โช ๐ฅ)) =
(โฏโโ
)) |
8 | | hash0 14274 |
. . . . . . 7
โข
(โฏโโ
) = 0 |
9 | 7, 8 | eqtrdi 2793 |
. . . . . 6
โข (๐ฅ = โ
โ
(โฏโ(๐ โฉ
โช ๐ฅ)) = 0) |
10 | 9 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = โ
โ
((โฏโ๐) โ
(โฏโ(๐ โฉ
โช ๐ฅ))) = ((โฏโ๐) โ 0)) |
11 | | pweq 4579 |
. . . . . . 7
โข (๐ฅ = โ
โ ๐ซ
๐ฅ = ๐ซ
โ
) |
12 | | pw0 4777 |
. . . . . . 7
โข ๐ซ
โ
= {โ
} |
13 | 11, 12 | eqtrdi 2793 |
. . . . . 6
โข (๐ฅ = โ
โ ๐ซ
๐ฅ =
{โ
}) |
14 | 13 | sumeq1d 15593 |
. . . . 5
โข (๐ฅ = โ
โ ฮฃ๐ โ ๐ซ ๐ฅ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ โฉ
โฉ ๐ ))) = ฮฃ๐ โ {โ
}
((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) |
15 | 10, 14 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = โ
โ
(((โฏโ๐) โ
(โฏโ(๐ โฉ
โช ๐ฅ))) = ฮฃ๐ โ ๐ซ ๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ ((โฏโ๐)
โ 0) = ฮฃ๐
โ {โ
} ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ ))))) |
16 | 15 | ralbidv 3175 |
. . 3
โข (๐ฅ = โ
โ (โ๐ โ Fin
((โฏโ๐) โ
(โฏโ(๐ โฉ
โช ๐ฅ))) = ฮฃ๐ โ ๐ซ ๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ โ๐ โ Fin
((โฏโ๐) โ
0) = ฮฃ๐ โ
{โ
} ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ ))))) |
17 | | unieq 4881 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ โช ๐ฅ = โช
๐ฆ) |
18 | 17 | ineq2d 4177 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (๐ โฉ โช ๐ฅ) = (๐ โฉ โช ๐ฆ)) |
19 | 18 | fveq2d 6851 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (โฏโ(๐ โฉ โช ๐ฅ)) = (โฏโ(๐ โฉ โช ๐ฆ))) |
20 | 19 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฅ))) = ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ)))) |
21 | | pweq 4579 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ๐ซ ๐ฅ = ๐ซ ๐ฆ) |
22 | 21 | sumeq1d 15593 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ฮฃ๐ โ ๐ซ ๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) |
23 | 20, 22 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = ๐ฆ โ (((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฅ))) = ฮฃ๐ โ ๐ซ ๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ ((โฏโ๐)
โ (โฏโ(๐
โฉ โช ๐ฆ))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ ))))) |
24 | 23 | ralbidv 3175 |
. . 3
โข (๐ฅ = ๐ฆ โ (โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฅ)))
= ฮฃ๐ โ ๐ซ
๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ โ๐ โ Fin
((โฏโ๐) โ
(โฏโ(๐ โฉ
โช ๐ฆ))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ ))))) |
25 | | unieq 4881 |
. . . . . . . . 9
โข (๐ฅ = (๐ฆ โช {๐ง}) โ โช ๐ฅ = โช
(๐ฆ โช {๐ง})) |
26 | | uniun 4896 |
. . . . . . . . . 10
โข โช (๐ฆ
โช {๐ง}) = (โช ๐ฆ
โช โช {๐ง}) |
27 | | unisnv 4893 |
. . . . . . . . . . 11
โข โช {๐ง}
= ๐ง |
28 | 27 | uneq2i 4125 |
. . . . . . . . . 10
โข (โช ๐ฆ
โช โช {๐ง}) = (โช ๐ฆ โช ๐ง) |
29 | 26, 28 | eqtri 2765 |
. . . . . . . . 9
โข โช (๐ฆ
โช {๐ง}) = (โช ๐ฆ
โช ๐ง) |
30 | 25, 29 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ โช {๐ง}) โ โช ๐ฅ = (โช
๐ฆ โช ๐ง)) |
31 | 30 | ineq2d 4177 |
. . . . . . 7
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (๐ โฉ โช ๐ฅ) = (๐ โฉ (โช ๐ฆ โช ๐ง))) |
32 | 31 | fveq2d 6851 |
. . . . . 6
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (โฏโ(๐ โฉ โช ๐ฅ)) = (โฏโ(๐ โฉ (โช ๐ฆ
โช ๐ง)))) |
33 | 32 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฅ))) = ((โฏโ๐) โ (โฏโ(๐ โฉ (โช ๐ฆ
โช ๐ง))))) |
34 | | pweq 4579 |
. . . . . 6
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ๐ซ ๐ฅ = ๐ซ (๐ฆ โช {๐ง})) |
35 | 34 | sumeq1d 15593 |
. . . . 5
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ฮฃ๐ โ ๐ซ ๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
= ฮฃ๐ โ ๐ซ
(๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ โฉ
โฉ ๐ )))) |
36 | 33, 35 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฅ))) = ฮฃ๐ โ ๐ซ ๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ ((โฏโ๐)
โ (โฏโ(๐
โฉ (โช ๐ฆ โช ๐ง)))) = ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ ))))) |
37 | 36 | ralbidv 3175 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฅ)))
= ฮฃ๐ โ ๐ซ
๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ โ๐ โ Fin
((โฏโ๐) โ
(โฏโ(๐ โฉ
(โช ๐ฆ โช ๐ง)))) = ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ ))))) |
38 | | unieq 4881 |
. . . . . . . 8
โข (๐ฅ = ๐ด โ โช ๐ฅ = โช
๐ด) |
39 | 38 | ineq2d 4177 |
. . . . . . 7
โข (๐ฅ = ๐ด โ (๐ โฉ โช ๐ฅ) = (๐ โฉ โช ๐ด)) |
40 | 39 | fveq2d 6851 |
. . . . . 6
โข (๐ฅ = ๐ด โ (โฏโ(๐ โฉ โช ๐ฅ)) = (โฏโ(๐ โฉ โช ๐ด))) |
41 | 40 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐ด โ ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฅ))) = ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ด)))) |
42 | | pweq 4579 |
. . . . . 6
โข (๐ฅ = ๐ด โ ๐ซ ๐ฅ = ๐ซ ๐ด) |
43 | 42 | sumeq1d 15593 |
. . . . 5
โข (๐ฅ = ๐ด โ ฮฃ๐ โ ๐ซ ๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
= ฮฃ๐ โ ๐ซ
๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) |
44 | 41, 43 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = ๐ด โ (((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฅ))) = ฮฃ๐ โ ๐ซ ๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ ((โฏโ๐)
โ (โฏโ(๐
โฉ โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ ))))) |
45 | 44 | ralbidv 3175 |
. . 3
โข (๐ฅ = ๐ด โ (โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฅ)))
= ฮฃ๐ โ ๐ซ
๐ฅ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ โ๐ โ Fin
((โฏโ๐) โ
(โฏโ(๐ โฉ
โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ ))))) |
46 | | hashcl 14263 |
. . . . . . 7
โข (๐ โ Fin โ
(โฏโ๐) โ
โ0) |
47 | 46 | nn0cnd 12482 |
. . . . . 6
โข (๐ โ Fin โ
(โฏโ๐) โ
โ) |
48 | 47 | mulid2d 11180 |
. . . . 5
โข (๐ โ Fin โ (1 ยท
(โฏโ๐)) =
(โฏโ๐)) |
49 | | 0ex 5269 |
. . . . . 6
โข โ
โ V |
50 | 48, 47 | eqeltrd 2838 |
. . . . . 6
โข (๐ โ Fin โ (1 ยท
(โฏโ๐)) โ
โ) |
51 | | fveq2 6847 |
. . . . . . . . . . 11
โข (๐ = โ
โ
(โฏโ๐ ) =
(โฏโโ
)) |
52 | 51, 8 | eqtrdi 2793 |
. . . . . . . . . 10
โข (๐ = โ
โ
(โฏโ๐ ) =
0) |
53 | 52 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = โ
โ
(-1โ(โฏโ๐ ))
= (-1โ0)) |
54 | | neg1cn 12274 |
. . . . . . . . . 10
โข -1 โ
โ |
55 | | exp0 13978 |
. . . . . . . . . 10
โข (-1
โ โ โ (-1โ0) = 1) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . 9
โข
(-1โ0) = 1 |
57 | 53, 56 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ = โ
โ
(-1โ(โฏโ๐ ))
= 1) |
58 | | rint0 4956 |
. . . . . . . . 9
โข (๐ = โ
โ (๐ โฉ โฉ ๐ ) =
๐) |
59 | 58 | fveq2d 6851 |
. . . . . . . 8
โข (๐ = โ
โ
(โฏโ(๐ โฉ
โฉ ๐ )) = (โฏโ๐)) |
60 | 57, 59 | oveq12d 7380 |
. . . . . . 7
โข (๐ = โ
โ
((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
= (1 ยท (โฏโ๐))) |
61 | 60 | sumsn 15638 |
. . . . . 6
โข ((โ
โ V โง (1 ยท (โฏโ๐)) โ โ) โ ฮฃ๐ โ {โ
}
((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
= (1 ยท (โฏโ๐))) |
62 | 49, 50, 61 | sylancr 588 |
. . . . 5
โข (๐ โ Fin โ ฮฃ๐ โ {โ
}
((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
= (1 ยท (โฏโ๐))) |
63 | 47 | subid1d 11508 |
. . . . 5
โข (๐ โ Fin โ
((โฏโ๐) โ
0) = (โฏโ๐)) |
64 | 48, 62, 63 | 3eqtr4rd 2788 |
. . . 4
โข (๐ โ Fin โ
((โฏโ๐) โ
0) = ฮฃ๐ โ
{โ
} ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) |
65 | 64 | rgen 3067 |
. . 3
โข
โ๐ โ Fin
((โฏโ๐) โ
0) = ฮฃ๐ โ
{โ
} ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ ))) |
66 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ (โฏโ๐) = (โฏโ๐ฅ)) |
67 | | ineq1 4170 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฅ โ (๐ โฉ โช ๐ฆ) = (๐ฅ โฉ โช ๐ฆ)) |
68 | 67 | fveq2d 6851 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ (โฏโ(๐ โฉ โช ๐ฆ)) = (โฏโ(๐ฅ โฉ โช ๐ฆ))) |
69 | 66, 68 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ = ๐ฅ โ ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ))) = ((โฏโ๐ฅ) โ (โฏโ(๐ฅ โฉ โช ๐ฆ)))) |
70 | | simpl 484 |
. . . . . . . . . . . . . . 15
โข ((๐ = ๐ฅ โง ๐ โ ๐ซ ๐ฆ) โ ๐ = ๐ฅ) |
71 | 70 | ineq1d 4176 |
. . . . . . . . . . . . . 14
โข ((๐ = ๐ฅ โง ๐ โ ๐ซ ๐ฆ) โ (๐ โฉ โฉ ๐ ) = (๐ฅ โฉ โฉ ๐ )) |
72 | 71 | fveq2d 6851 |
. . . . . . . . . . . . 13
โข ((๐ = ๐ฅ โง ๐ โ ๐ซ ๐ฆ) โ (โฏโ(๐ โฉ โฉ ๐ )) = (โฏโ(๐ฅ โฉ โฉ ๐ ))) |
73 | 72 | oveq2d 7378 |
. . . . . . . . . . . 12
โข ((๐ = ๐ฅ โง ๐ โ ๐ซ ๐ฆ) โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ โฉ
โฉ ๐ ))) = ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
โฉ ๐ )))) |
74 | 73 | sumeq2dv 15595 |
. . . . . . . . . . 11
โข (๐ = ๐ฅ โ ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))) |
75 | 69, 74 | eqeq12d 2753 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ ((โฏโ๐ฅ)
โ (โฏโ(๐ฅ
โฉ โช ๐ฆ))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ ))))) |
76 | 75 | rspcva 3582 |
. . . . . . . . 9
โข ((๐ฅ โ Fin โง โ๐ โ Fin
((โฏโ๐) โ
(โฏโ(๐ โฉ
โช ๐ฆ))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) โ ((โฏโ๐ฅ) โ (โฏโ(๐ฅ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))) |
77 | 76 | adantll 713 |
. . . . . . . 8
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) โ ((โฏโ๐ฅ) โ (โฏโ(๐ฅ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))) |
78 | | simpr 486 |
. . . . . . . . . 10
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ๐ฅ โ Fin) |
79 | | inss1 4193 |
. . . . . . . . . 10
โข (๐ฅ โฉ ๐ง) โ ๐ฅ |
80 | | ssfi 9124 |
. . . . . . . . . 10
โข ((๐ฅ โ Fin โง (๐ฅ โฉ ๐ง) โ ๐ฅ) โ (๐ฅ โฉ ๐ง) โ Fin) |
81 | 78, 79, 80 | sylancl 587 |
. . . . . . . . 9
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (๐ฅ โฉ ๐ง) โ Fin) |
82 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ = (๐ฅ โฉ ๐ง) โ (โฏโ๐) = (โฏโ(๐ฅ โฉ ๐ง))) |
83 | | ineq1 4170 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ฅ โฉ ๐ง) โ (๐ โฉ โช ๐ฆ) = ((๐ฅ โฉ ๐ง) โฉ โช ๐ฆ)) |
84 | | in32 4186 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โฉ ๐ง) โฉ โช ๐ฆ) = ((๐ฅ โฉ โช ๐ฆ) โฉ ๐ง) |
85 | | inass 4184 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โฉ โช ๐ฆ)
โฉ ๐ง) = (๐ฅ โฉ (โช ๐ฆ
โฉ ๐ง)) |
86 | 84, 85 | eqtri 2765 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โฉ ๐ง) โฉ โช ๐ฆ) = (๐ฅ โฉ (โช ๐ฆ โฉ ๐ง)) |
87 | 83, 86 | eqtrdi 2793 |
. . . . . . . . . . . . 13
โข (๐ = (๐ฅ โฉ ๐ง) โ (๐ โฉ โช ๐ฆ) = (๐ฅ โฉ (โช ๐ฆ โฉ ๐ง))) |
88 | 87 | fveq2d 6851 |
. . . . . . . . . . . 12
โข (๐ = (๐ฅ โฉ ๐ง) โ (โฏโ(๐ โฉ โช ๐ฆ)) = (โฏโ(๐ฅ โฉ (โช ๐ฆ
โฉ ๐ง)))) |
89 | 82, 88 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ = (๐ฅ โฉ ๐ง) โ ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ))) = ((โฏโ(๐ฅ โฉ ๐ง)) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ โฉ ๐ง))))) |
90 | | ineq1 4170 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ฅ โฉ ๐ง) โ (๐ โฉ โฉ ๐ ) = ((๐ฅ โฉ ๐ง) โฉ โฉ ๐ )) |
91 | | in32 4186 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โฉ ๐ง) โฉ โฉ ๐ ) = ((๐ฅ โฉ โฉ ๐ ) โฉ ๐ง) |
92 | | inass 4184 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โฉ โฉ ๐ )
โฉ ๐ง) = (๐ฅ โฉ (โฉ ๐
โฉ ๐ง)) |
93 | 91, 92 | eqtri 2765 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โฉ ๐ง) โฉ โฉ ๐ ) = (๐ฅ โฉ (โฉ ๐ โฉ ๐ง)) |
94 | 90, 93 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ฅ โฉ ๐ง) โ (๐ โฉ โฉ ๐ ) = (๐ฅ โฉ (โฉ ๐ โฉ ๐ง))) |
95 | 94 | fveq2d 6851 |
. . . . . . . . . . . . 13
โข (๐ = (๐ฅ โฉ ๐ง) โ (โฏโ(๐ โฉ โฉ ๐ )) = (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))) |
96 | 95 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ = (๐ฅ โฉ ๐ง) โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ โฉ
โฉ ๐ ))) = ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง))))) |
97 | 96 | sumeq2sdv 15596 |
. . . . . . . . . . 11
โข (๐ = (๐ฅ โฉ ๐ง) โ ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง))))) |
98 | 89, 97 | eqeq12d 2753 |
. . . . . . . . . 10
โข (๐ = (๐ฅ โฉ ๐ง) โ (((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ ((โฏโ(๐ฅ
โฉ ๐ง)) โ
(โฏโ(๐ฅ โฉ
(โช ๐ฆ โฉ ๐ง)))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))))) |
99 | 98 | rspcva 3582 |
. . . . . . . . 9
โข (((๐ฅ โฉ ๐ง) โ Fin โง โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) โ ((โฏโ(๐ฅ โฉ ๐ง)) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ โฉ ๐ง)))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง))))) |
100 | 81, 99 | sylan 581 |
. . . . . . . 8
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) โ ((โฏโ(๐ฅ โฉ ๐ง)) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ โฉ ๐ง)))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง))))) |
101 | 77, 100 | oveq12d 7380 |
. . . . . . 7
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) โ (((โฏโ๐ฅ) โ (โฏโ(๐ฅ โฉ โช ๐ฆ)))
โ ((โฏโ(๐ฅ
โฉ ๐ง)) โ
(โฏโ(๐ฅ โฉ
(โช ๐ฆ โฉ ๐ง))))) = (ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
โ ฮฃ๐ โ
๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))))) |
102 | | inss1 4193 |
. . . . . . . . . . . . . 14
โข (๐ฅ โฉ โช ๐ฆ)
โ ๐ฅ |
103 | | ssfi 9124 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ Fin โง (๐ฅ โฉ โช ๐ฆ)
โ ๐ฅ) โ (๐ฅ โฉ โช ๐ฆ)
โ Fin) |
104 | 78, 102, 103 | sylancl 587 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (๐ฅ โฉ โช ๐ฆ) โ Fin) |
105 | | hashcl 14263 |
. . . . . . . . . . . . 13
โข ((๐ฅ โฉ โช ๐ฆ)
โ Fin โ (โฏโ(๐ฅ โฉ โช ๐ฆ)) โ
โ0) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ(๐ฅ โฉ โช ๐ฆ))
โ โ0) |
107 | 106 | nn0cnd 12482 |
. . . . . . . . . . 11
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ(๐ฅ โฉ โช ๐ฆ))
โ โ) |
108 | | hashcl 14263 |
. . . . . . . . . . . . 13
โข ((๐ฅ โฉ ๐ง) โ Fin โ (โฏโ(๐ฅ โฉ ๐ง)) โ
โ0) |
109 | 81, 108 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ(๐ฅ โฉ ๐ง)) โ
โ0) |
110 | 109 | nn0cnd 12482 |
. . . . . . . . . . 11
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ(๐ฅ โฉ ๐ง)) โ โ) |
111 | | inss1 4193 |
. . . . . . . . . . . . . 14
โข (๐ฅ โฉ (โช ๐ฆ
โฉ ๐ง)) โ ๐ฅ |
112 | | ssfi 9124 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ Fin โง (๐ฅ โฉ (โช ๐ฆ
โฉ ๐ง)) โ ๐ฅ) โ (๐ฅ โฉ (โช ๐ฆ โฉ ๐ง)) โ Fin) |
113 | 78, 111, 112 | sylancl 587 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (๐ฅ โฉ (โช ๐ฆ โฉ ๐ง)) โ Fin) |
114 | | hashcl 14263 |
. . . . . . . . . . . . 13
โข ((๐ฅ โฉ (โช ๐ฆ
โฉ ๐ง)) โ Fin โ
(โฏโ(๐ฅ โฉ
(โช ๐ฆ โฉ ๐ง))) โ
โ0) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ
โฉ ๐ง))) โ
โ0) |
116 | 115 | nn0cnd 12482 |
. . . . . . . . . . 11
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ
โฉ ๐ง))) โ
โ) |
117 | | hashun3 14291 |
. . . . . . . . . . . . 13
โข (((๐ฅ โฉ โช ๐ฆ)
โ Fin โง (๐ฅ โฉ
๐ง) โ Fin) โ
(โฏโ((๐ฅ โฉ
โช ๐ฆ) โช (๐ฅ โฉ ๐ง))) = (((โฏโ(๐ฅ โฉ โช ๐ฆ)) + (โฏโ(๐ฅ โฉ ๐ง))) โ (โฏโ((๐ฅ โฉ โช ๐ฆ)
โฉ (๐ฅ โฉ ๐ง))))) |
118 | 104, 81, 117 | syl2anc 585 |
. . . . . . . . . . . 12
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ((๐ฅ โฉ โช ๐ฆ)
โช (๐ฅ โฉ ๐ง))) = (((โฏโ(๐ฅ โฉ โช ๐ฆ))
+ (โฏโ(๐ฅ โฉ
๐ง))) โ
(โฏโ((๐ฅ โฉ
โช ๐ฆ) โฉ (๐ฅ โฉ ๐ง))))) |
119 | | indi 4238 |
. . . . . . . . . . . . 13
โข (๐ฅ โฉ (โช ๐ฆ
โช ๐ง)) = ((๐ฅ โฉ โช ๐ฆ)
โช (๐ฅ โฉ ๐ง)) |
120 | 119 | fveq2i 6850 |
. . . . . . . . . . . 12
โข
(โฏโ(๐ฅ
โฉ (โช ๐ฆ โช ๐ง))) = (โฏโ((๐ฅ โฉ โช ๐ฆ) โช (๐ฅ โฉ ๐ง))) |
121 | | inindi 4191 |
. . . . . . . . . . . . . 14
โข (๐ฅ โฉ (โช ๐ฆ
โฉ ๐ง)) = ((๐ฅ โฉ โช ๐ฆ)
โฉ (๐ฅ โฉ ๐ง)) |
122 | 121 | fveq2i 6850 |
. . . . . . . . . . . . 13
โข
(โฏโ(๐ฅ
โฉ (โช ๐ฆ โฉ ๐ง))) = (โฏโ((๐ฅ โฉ โช ๐ฆ) โฉ (๐ฅ โฉ ๐ง))) |
123 | 122 | oveq2i 7373 |
. . . . . . . . . . . 12
โข
(((โฏโ(๐ฅ
โฉ โช ๐ฆ)) + (โฏโ(๐ฅ โฉ ๐ง))) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ
โฉ ๐ง)))) =
(((โฏโ(๐ฅ โฉ
โช ๐ฆ)) + (โฏโ(๐ฅ โฉ ๐ง))) โ (โฏโ((๐ฅ โฉ โช ๐ฆ)
โฉ (๐ฅ โฉ ๐ง)))) |
124 | 118, 120,
123 | 3eqtr4g 2802 |
. . . . . . . . . . 11
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ
โช ๐ง))) =
(((โฏโ(๐ฅ โฉ
โช ๐ฆ)) + (โฏโ(๐ฅ โฉ ๐ง))) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ
โฉ ๐ง))))) |
125 | 107, 110,
116, 124 | assraddsubd 11576 |
. . . . . . . . . 10
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ
โช ๐ง))) =
((โฏโ(๐ฅ โฉ
โช ๐ฆ)) + ((โฏโ(๐ฅ โฉ ๐ง)) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ โฉ ๐ง)))))) |
126 | 125 | oveq2d 7378 |
. . . . . . . . 9
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ((โฏโ๐ฅ) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ
โช ๐ง)))) =
((โฏโ๐ฅ) โ
((โฏโ(๐ฅ โฉ
โช ๐ฆ)) + ((โฏโ(๐ฅ โฉ ๐ง)) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ โฉ ๐ง))))))) |
127 | | hashcl 14263 |
. . . . . . . . . . . 12
โข (๐ฅ โ Fin โ
(โฏโ๐ฅ) โ
โ0) |
128 | 127 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ๐ฅ) โ
โ0) |
129 | 128 | nn0cnd 12482 |
. . . . . . . . . 10
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โฏโ๐ฅ) โ
โ) |
130 | 110, 116 | subcld 11519 |
. . . . . . . . . 10
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ((โฏโ(๐ฅ โฉ ๐ง)) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ โฉ ๐ง)))) โ โ) |
131 | 129, 107,
130 | subsub4d 11550 |
. . . . . . . . 9
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (((โฏโ๐ฅ) โ (โฏโ(๐ฅ โฉ โช ๐ฆ)))
โ ((โฏโ(๐ฅ
โฉ ๐ง)) โ
(โฏโ(๐ฅ โฉ
(โช ๐ฆ โฉ ๐ง))))) = ((โฏโ๐ฅ) โ ((โฏโ(๐ฅ โฉ โช ๐ฆ)) + ((โฏโ(๐ฅ โฉ ๐ง)) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ โฉ ๐ง))))))) |
132 | 126, 131 | eqtr4d 2780 |
. . . . . . . 8
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ((โฏโ๐ฅ) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ
โช ๐ง)))) =
(((โฏโ๐ฅ) โ
(โฏโ(๐ฅ โฉ
โช ๐ฆ))) โ ((โฏโ(๐ฅ โฉ ๐ง)) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ โฉ ๐ง)))))) |
133 | 132 | adantr 482 |
. . . . . . 7
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) โ ((โฏโ๐ฅ) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ
โช ๐ง)))) =
(((โฏโ๐ฅ) โ
(โฏโ(๐ฅ โฉ
โช ๐ฆ))) โ ((โฏโ(๐ฅ โฉ ๐ง)) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ โฉ ๐ง)))))) |
134 | | disjdif 4436 |
. . . . . . . . . . 11
โข
(๐ซ ๐ฆ โฉ
(๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) = โ
|
135 | 134 | a1i 11 |
. . . . . . . . . 10
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (๐ซ ๐ฆ โฉ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) = โ
) |
136 | | ssun1 4137 |
. . . . . . . . . . . . . 14
โข ๐ฆ โ (๐ฆ โช {๐ง}) |
137 | 136 | sspwi 4577 |
. . . . . . . . . . . . 13
โข ๐ซ
๐ฆ โ ๐ซ (๐ฆ โช {๐ง}) |
138 | | undif 4446 |
. . . . . . . . . . . . 13
โข
(๐ซ ๐ฆ โ
๐ซ (๐ฆ โช {๐ง}) โ (๐ซ ๐ฆ โช (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) = ๐ซ (๐ฆ โช {๐ง})) |
139 | 137, 138 | mpbi 229 |
. . . . . . . . . . . 12
โข
(๐ซ ๐ฆ โช
(๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) = ๐ซ (๐ฆ โช {๐ง}) |
140 | 139 | eqcomi 2746 |
. . . . . . . . . . 11
โข ๐ซ
(๐ฆ โช {๐ง}) = (๐ซ ๐ฆ โช (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) |
141 | 140 | a1i 11 |
. . . . . . . . . 10
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ๐ซ (๐ฆ โช {๐ง}) = (๐ซ ๐ฆ โช (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) |
142 | | simpll 766 |
. . . . . . . . . . . 12
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ๐ฆ โ Fin) |
143 | | snfi 8995 |
. . . . . . . . . . . 12
โข {๐ง} โ Fin |
144 | | unfi 9123 |
. . . . . . . . . . . 12
โข ((๐ฆ โ Fin โง {๐ง} โ Fin) โ (๐ฆ โช {๐ง}) โ Fin) |
145 | 142, 143,
144 | sylancl 587 |
. . . . . . . . . . 11
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (๐ฆ โช {๐ง}) โ Fin) |
146 | | pwfi 9129 |
. . . . . . . . . . 11
โข ((๐ฆ โช {๐ง}) โ Fin โ ๐ซ (๐ฆ โช {๐ง}) โ Fin) |
147 | 145, 146 | sylib 217 |
. . . . . . . . . 10
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ๐ซ (๐ฆ โช {๐ง}) โ Fin) |
148 | 54 | a1i 11 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ -1 โ
โ) |
149 | | elpwi 4572 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ซ (๐ฆ โช {๐ง}) โ ๐ โ (๐ฆ โช {๐ง})) |
150 | | ssfi 9124 |
. . . . . . . . . . . . . 14
โข (((๐ฆ โช {๐ง}) โ Fin โง ๐ โ (๐ฆ โช {๐ง})) โ ๐ โ Fin) |
151 | 145, 149,
150 | syl2an 597 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ ๐ โ Fin) |
152 | | hashcl 14263 |
. . . . . . . . . . . . 13
โข (๐ โ Fin โ
(โฏโ๐ ) โ
โ0) |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ (โฏโ๐ ) โ
โ0) |
154 | 148, 153 | expcld 14058 |
. . . . . . . . . . 11
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ (-1โ(โฏโ๐ )) โ
โ) |
155 | | simplr 768 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ ๐ฅ โ Fin) |
156 | | inss1 4193 |
. . . . . . . . . . . . . 14
โข (๐ฅ โฉ โฉ ๐ )
โ ๐ฅ |
157 | | ssfi 9124 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ Fin โง (๐ฅ โฉ โฉ ๐ )
โ ๐ฅ) โ (๐ฅ โฉ โฉ ๐ )
โ Fin) |
158 | 155, 156,
157 | sylancl 587 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ (๐ฅ โฉ โฉ ๐ ) โ Fin) |
159 | | hashcl 14263 |
. . . . . . . . . . . . 13
โข ((๐ฅ โฉ โฉ ๐ )
โ Fin โ (โฏโ(๐ฅ โฉ โฉ ๐ )) โ
โ0) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ (โฏโ(๐ฅ โฉ โฉ ๐ )) โ
โ0) |
161 | 160 | nn0cnd 12482 |
. . . . . . . . . . 11
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ (โฏโ(๐ฅ โฉ โฉ ๐ )) โ
โ) |
162 | 154, 161 | mulcld 11182 |
. . . . . . . . . 10
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
โฉ ๐ ))) โ โ) |
163 | 135, 141,
147, 162 | fsumsplit 15633 |
. . . . . . . . 9
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
= (ฮฃ๐ โ
๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
+ ฮฃ๐ โ
(๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
โฉ ๐ ))))) |
164 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ก โช {๐ง}) โ (โฏโ๐ ) = (โฏโ(๐ก โช {๐ง}))) |
165 | 164 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (๐ = (๐ก โช {๐ง}) โ (-1โ(โฏโ๐ )) =
(-1โ(โฏโ(๐ก
โช {๐ง})))) |
166 | | inteq 4915 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ก โช {๐ง}) โ โฉ ๐ = โฉ
(๐ก โช {๐ง})) |
167 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
โข ๐ง โ V |
168 | 167 | intunsn 4955 |
. . . . . . . . . . . . . . . 16
โข โฉ (๐ก
โช {๐ง}) = (โฉ ๐ก
โฉ ๐ง) |
169 | 166, 168 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ก โช {๐ง}) โ โฉ ๐ = (โฉ
๐ก โฉ ๐ง)) |
170 | 169 | ineq2d 4177 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ก โช {๐ง}) โ (๐ฅ โฉ โฉ ๐ ) = (๐ฅ โฉ (โฉ ๐ก โฉ ๐ง))) |
171 | 170 | fveq2d 6851 |
. . . . . . . . . . . . 13
โข (๐ = (๐ก โช {๐ง}) โ (โฏโ(๐ฅ โฉ โฉ ๐ )) = (โฏโ(๐ฅ โฉ (โฉ ๐ก
โฉ ๐ง)))) |
172 | 165, 171 | oveq12d 7380 |
. . . . . . . . . . . 12
โข (๐ = (๐ก โช {๐ง}) โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
โฉ ๐ ))) = ((-1โ(โฏโ(๐ก โช {๐ง}))) ยท (โฏโ(๐ฅ โฉ (โฉ ๐ก
โฉ ๐ง))))) |
173 | | pwfi 9129 |
. . . . . . . . . . . . 13
โข (๐ฆ โ Fin โ ๐ซ
๐ฆ โ
Fin) |
174 | 142, 173 | sylib 217 |
. . . . . . . . . . . 12
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ๐ซ ๐ฆ โ Fin) |
175 | | eqid 2737 |
. . . . . . . . . . . . 13
โข (๐ข โ ๐ซ ๐ฆ โฆ (๐ข โช {๐ง})) = (๐ข โ ๐ซ ๐ฆ โฆ (๐ข โช {๐ง})) |
176 | | elpwi 4572 |
. . . . . . . . . . . . . . . . 17
โข (๐ข โ ๐ซ ๐ฆ โ ๐ข โ ๐ฆ) |
177 | 176 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ข โ ๐ซ ๐ฆ) โ ๐ข โ ๐ฆ) |
178 | | unss1 4144 |
. . . . . . . . . . . . . . . 16
โข (๐ข โ ๐ฆ โ (๐ข โช {๐ง}) โ (๐ฆ โช {๐ง})) |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ข โ ๐ซ ๐ฆ) โ (๐ข โช {๐ง}) โ (๐ฆ โช {๐ง})) |
180 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
โข ๐ข โ V |
181 | | vsnex 5391 |
. . . . . . . . . . . . . . . . 17
โข {๐ง} โ V |
182 | 180, 181 | unex 7685 |
. . . . . . . . . . . . . . . 16
โข (๐ข โช {๐ง}) โ V |
183 | 182 | elpw 4569 |
. . . . . . . . . . . . . . 15
โข ((๐ข โช {๐ง}) โ ๐ซ (๐ฆ โช {๐ง}) โ (๐ข โช {๐ง}) โ (๐ฆ โช {๐ง})) |
184 | 179, 183 | sylibr 233 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ข โ ๐ซ ๐ฆ) โ (๐ข โช {๐ง}) โ ๐ซ (๐ฆ โช {๐ง})) |
185 | | simpllr 775 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ข โ ๐ซ ๐ฆ) โ ยฌ ๐ง โ ๐ฆ) |
186 | | elpwi 4572 |
. . . . . . . . . . . . . . . 16
โข ((๐ข โช {๐ง}) โ ๐ซ ๐ฆ โ (๐ข โช {๐ง}) โ ๐ฆ) |
187 | | ssun2 4138 |
. . . . . . . . . . . . . . . . . 18
โข {๐ง} โ (๐ข โช {๐ง}) |
188 | 167 | snss 4751 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง โ (๐ข โช {๐ง}) โ {๐ง} โ (๐ข โช {๐ง})) |
189 | 187, 188 | mpbir 230 |
. . . . . . . . . . . . . . . . 17
โข ๐ง โ (๐ข โช {๐ง}) |
190 | 189 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ข โ ๐ซ ๐ฆ) โ ๐ง โ (๐ข โช {๐ง})) |
191 | | ssel 3942 |
. . . . . . . . . . . . . . . 16
โข ((๐ข โช {๐ง}) โ ๐ฆ โ (๐ง โ (๐ข โช {๐ง}) โ ๐ง โ ๐ฆ)) |
192 | 186, 190,
191 | syl2imc 41 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ข โ ๐ซ ๐ฆ) โ ((๐ข โช {๐ง}) โ ๐ซ ๐ฆ โ ๐ง โ ๐ฆ)) |
193 | 185, 192 | mtod 197 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ข โ ๐ซ ๐ฆ) โ ยฌ (๐ข โช {๐ง}) โ ๐ซ ๐ฆ) |
194 | 184, 193 | eldifd 3926 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ข โ ๐ซ ๐ฆ) โ (๐ข โช {๐ง}) โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) |
195 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ) โ ๐ โ ๐ซ (๐ฆ โช {๐ง})) |
196 | 195 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) โ ๐ โ ๐ซ (๐ฆ โช {๐ง})) |
197 | 196 | elpwid 4574 |
. . . . . . . . . . . . . . . 16
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) โ ๐ โ (๐ฆ โช {๐ง})) |
198 | | uncom 4118 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โช {๐ง}) = ({๐ง} โช ๐ฆ) |
199 | 197, 198 | sseqtrdi 3999 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) โ ๐ โ ({๐ง} โช ๐ฆ)) |
200 | | ssundif 4450 |
. . . . . . . . . . . . . . 15
โข (๐ โ ({๐ง} โช ๐ฆ) โ (๐ โ {๐ง}) โ ๐ฆ) |
201 | 199, 200 | sylib 217 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) โ (๐ โ {๐ง}) โ ๐ฆ) |
202 | | vex 3452 |
. . . . . . . . . . . . . . 15
โข ๐ฆ โ V |
203 | 202 | elpw2 5307 |
. . . . . . . . . . . . . 14
โข ((๐ โ {๐ง}) โ ๐ซ ๐ฆ โ (๐ โ {๐ง}) โ ๐ฆ) |
204 | 201, 203 | sylibr 233 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) โ (๐ โ {๐ง}) โ ๐ซ ๐ฆ) |
205 | | elpwunsn 4649 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ) โ ๐ง โ ๐ ) |
206 | 205 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ ๐ง โ ๐ ) |
207 | 206 | snssd 4774 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ {๐ง} โ ๐ ) |
208 | | ssequn2 4148 |
. . . . . . . . . . . . . . . . 17
โข ({๐ง} โ ๐ โ (๐ โช {๐ง}) = ๐ ) |
209 | 207, 208 | sylib 217 |
. . . . . . . . . . . . . . . 16
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ (๐ โช {๐ง}) = ๐ ) |
210 | 209 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ ๐ = (๐ โช {๐ง})) |
211 | | uneq1 4121 |
. . . . . . . . . . . . . . . . 17
โข (๐ข = (๐ โ {๐ง}) โ (๐ข โช {๐ง}) = ((๐ โ {๐ง}) โช {๐ง})) |
212 | | undif1 4440 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ {๐ง}) โช {๐ง}) = (๐ โช {๐ง}) |
213 | 211, 212 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
โข (๐ข = (๐ โ {๐ง}) โ (๐ข โช {๐ง}) = (๐ โช {๐ง})) |
214 | 213 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
โข (๐ข = (๐ โ {๐ง}) โ (๐ = (๐ข โช {๐ง}) โ ๐ = (๐ โช {๐ง}))) |
215 | 210, 214 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ (๐ข = (๐ โ {๐ง}) โ ๐ = (๐ข โช {๐ง}))) |
216 | 176 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ ๐ข โ ๐ฆ) |
217 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ ยฌ ๐ง โ ๐ฆ) |
218 | 216, 217 | ssneldd 3952 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ ยฌ ๐ง โ ๐ข) |
219 | | difsnb 4771 |
. . . . . . . . . . . . . . . . 17
โข (ยฌ
๐ง โ ๐ข โ (๐ข โ {๐ง}) = ๐ข) |
220 | 218, 219 | sylib 217 |
. . . . . . . . . . . . . . . 16
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ (๐ข โ {๐ง}) = ๐ข) |
221 | 220 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ ๐ข = (๐ข โ {๐ง})) |
222 | | difeq1 4080 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ข โช {๐ง}) โ (๐ โ {๐ง}) = ((๐ข โช {๐ง}) โ {๐ง})) |
223 | | difun2 4445 |
. . . . . . . . . . . . . . . . 17
โข ((๐ข โช {๐ง}) โ {๐ง}) = (๐ข โ {๐ง}) |
224 | 222, 223 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ข โช {๐ง}) โ (๐ โ {๐ง}) = (๐ข โ {๐ง})) |
225 | 224 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ข โช {๐ง}) โ (๐ข = (๐ โ {๐ง}) โ ๐ข = (๐ข โ {๐ง}))) |
226 | 221, 225 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ (๐ = (๐ข โช {๐ง}) โ ๐ข = (๐ โ {๐ง}))) |
227 | 215, 226 | impbid 211 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง (๐ข โ ๐ซ ๐ฆ โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ))) โ (๐ข = (๐ โ {๐ง}) โ ๐ = (๐ข โช {๐ง}))) |
228 | 175, 194,
204, 227 | f1o2d 7612 |
. . . . . . . . . . . 12
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (๐ข โ ๐ซ ๐ฆ โฆ (๐ข โช {๐ง})):๐ซ ๐ฆโ1-1-ontoโ(๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) |
229 | | uneq1 4121 |
. . . . . . . . . . . . . 14
โข (๐ข = ๐ก โ (๐ข โช {๐ง}) = (๐ก โช {๐ง})) |
230 | | vex 3452 |
. . . . . . . . . . . . . . 15
โข ๐ก โ V |
231 | 230, 181 | unex 7685 |
. . . . . . . . . . . . . 14
โข (๐ก โช {๐ง}) โ V |
232 | 229, 175,
231 | fvmpt 6953 |
. . . . . . . . . . . . 13
โข (๐ก โ ๐ซ ๐ฆ โ ((๐ข โ ๐ซ ๐ฆ โฆ (๐ข โช {๐ง}))โ๐ก) = (๐ก โช {๐ง})) |
233 | 232 | adantl 483 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ก โ ๐ซ ๐ฆ) โ ((๐ข โ ๐ซ ๐ฆ โฆ (๐ข โช {๐ง}))โ๐ก) = (๐ก โช {๐ง})) |
234 | 195, 162 | sylan2 594 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)) โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
โฉ ๐ ))) โ โ) |
235 | 172, 174,
228, 233, 234 | fsumf1o 15615 |
. . . . . . . . . . 11
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ฮฃ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
= ฮฃ๐ก โ ๐ซ
๐ฆ((-1โ(โฏโ(๐ก โช {๐ง}))) ยท (โฏโ(๐ฅ โฉ (โฉ ๐ก
โฉ ๐ง))))) |
236 | | uneq1 4121 |
. . . . . . . . . . . . . . . 16
โข (๐ก = ๐ โ (๐ก โช {๐ง}) = (๐ โช {๐ง})) |
237 | 236 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
โข (๐ก = ๐ โ (โฏโ(๐ก โช {๐ง})) = (โฏโ(๐ โช {๐ง}))) |
238 | 237 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ก = ๐ โ (-1โ(โฏโ(๐ก โช {๐ง}))) = (-1โ(โฏโ(๐ โช {๐ง})))) |
239 | | inteq 4915 |
. . . . . . . . . . . . . . . . 17
โข (๐ก = ๐ โ โฉ ๐ก = โฉ
๐ ) |
240 | 239 | ineq1d 4176 |
. . . . . . . . . . . . . . . 16
โข (๐ก = ๐ โ (โฉ ๐ก โฉ ๐ง) = (โฉ ๐ โฉ ๐ง)) |
241 | 240 | ineq2d 4177 |
. . . . . . . . . . . . . . 15
โข (๐ก = ๐ โ (๐ฅ โฉ (โฉ ๐ก โฉ ๐ง)) = (๐ฅ โฉ (โฉ ๐ โฉ ๐ง))) |
242 | 241 | fveq2d 6851 |
. . . . . . . . . . . . . 14
โข (๐ก = ๐ โ (โฏโ(๐ฅ โฉ (โฉ ๐ก โฉ ๐ง))) = (โฏโ(๐ฅ โฉ (โฉ ๐ โฉ ๐ง)))) |
243 | 238, 242 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ก = ๐ โ ((-1โ(โฏโ(๐ก โช {๐ง}))) ยท (โฏโ(๐ฅ โฉ (โฉ ๐ก
โฉ ๐ง)))) =
((-1โ(โฏโ(๐
โช {๐ง}))) ยท
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง))))) |
244 | 243 | cbvsumv 15588 |
. . . . . . . . . . . 12
โข
ฮฃ๐ก โ
๐ซ ๐ฆ((-1โ(โฏโ(๐ก โช {๐ง}))) ยท (โฏโ(๐ฅ โฉ (โฉ ๐ก
โฉ ๐ง)))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ(๐ โช {๐ง}))) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))) |
245 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ -1 โ โ) |
246 | | elpwi 4572 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ซ ๐ฆ โ ๐ โ ๐ฆ) |
247 | | ssfi 9124 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ Fin โง ๐ โ ๐ฆ) โ ๐ โ Fin) |
248 | 142, 246,
247 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ ๐ โ Fin) |
249 | 248, 152 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (โฏโ๐ ) โ
โ0) |
250 | 245, 249 | expp1d 14059 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (-1โ((โฏโ๐ ) + 1)) =
((-1โ(โฏโ๐ )) ยท -1)) |
251 | 246 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ ๐ โ ๐ฆ) |
252 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ ยฌ ๐ง โ ๐ฆ) |
253 | 251, 252 | ssneldd 3952 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ ยฌ ๐ง โ ๐ ) |
254 | | hashunsng 14299 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง โ V โ ((๐ โ Fin โง ยฌ ๐ง โ ๐ ) โ (โฏโ(๐ โช {๐ง})) = ((โฏโ๐ ) + 1))) |
255 | 254 | elv 3454 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ Fin โง ยฌ ๐ง โ ๐ ) โ (โฏโ(๐ โช {๐ง})) = ((โฏโ๐ ) + 1)) |
256 | 248, 253,
255 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (โฏโ(๐ โช {๐ง})) = ((โฏโ๐ ) + 1)) |
257 | 256 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (-1โ(โฏโ(๐ โช {๐ง}))) = (-1โ((โฏโ๐ ) + 1))) |
258 | 137 | sseli 3945 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ซ ๐ฆ โ ๐ โ ๐ซ (๐ฆ โช {๐ง})) |
259 | 258, 154 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (-1โ(โฏโ๐ )) โ
โ) |
260 | 245, 259 | mulcomd 11183 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (-1 ยท
(-1โ(โฏโ๐ ))) = ((-1โ(โฏโ๐ )) ยท
-1)) |
261 | 250, 257,
260 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . 16
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (-1โ(โฏโ(๐ โช {๐ง}))) = (-1 ยท
(-1โ(โฏโ๐ )))) |
262 | 259 | mulm1d 11614 |
. . . . . . . . . . . . . . . 16
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (-1 ยท
(-1โ(โฏโ๐ ))) = -(-1โ(โฏโ๐ ))) |
263 | 261, 262 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (-1โ(โฏโ(๐ โช {๐ง}))) = -(-1โ(โฏโ๐ ))) |
264 | 263 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ ((-1โ(โฏโ(๐ โช {๐ง}))) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))) =
(-(-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง))))) |
265 | | inss1 4193 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โฉ (โฉ ๐
โฉ ๐ง)) โ ๐ฅ |
266 | | ssfi 9124 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฅ โ Fin โง (๐ฅ โฉ (โฉ ๐
โฉ ๐ง)) โ ๐ฅ) โ (๐ฅ โฉ (โฉ ๐ โฉ ๐ง)) โ Fin) |
267 | 155, 265,
266 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ (๐ฅ โฉ (โฉ ๐ โฉ ๐ง)) โ Fin) |
268 | | hashcl 14263 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฅ โฉ (โฉ ๐
โฉ ๐ง)) โ Fin โ
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง))) โ
โ0) |
269 | 267, 268 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ (โฏโ(๐ฅ โฉ (โฉ ๐ โฉ ๐ง))) โ
โ0) |
270 | 269 | nn0cnd 12482 |
. . . . . . . . . . . . . . . 16
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ (โฏโ(๐ฅ โฉ (โฉ ๐ โฉ ๐ง))) โ โ) |
271 | 258, 270 | sylan2 594 |
. . . . . . . . . . . . . . 15
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (โฏโ(๐ฅ โฉ (โฉ ๐ โฉ ๐ง))) โ โ) |
272 | 259, 271 | mulneg1d 11615 |
. . . . . . . . . . . . . 14
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ (-(-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง)))) = -((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง))))) |
273 | 264, 272 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ ((-1โ(โฏโ(๐ โช {๐ง}))) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))) =
-((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง))))) |
274 | 273 | sumeq2dv 15595 |
. . . . . . . . . . . 12
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ(๐ โช {๐ง}))) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))) = ฮฃ๐ โ ๐ซ ๐ฆ-((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง))))) |
275 | 244, 274 | eqtrid 2789 |
. . . . . . . . . . 11
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ฮฃ๐ก โ ๐ซ ๐ฆ((-1โ(โฏโ(๐ก โช {๐ง}))) ยท (โฏโ(๐ฅ โฉ (โฉ ๐ก
โฉ ๐ง)))) = ฮฃ๐ โ ๐ซ ๐ฆ-((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง))))) |
276 | 154, 270 | mulcld 11182 |
. . . . . . . . . . . . 13
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ (๐ฆ โช {๐ง})) โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง)))) โ โ) |
277 | 258, 276 | sylan2 594 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง)))) โ โ) |
278 | 174, 277 | fsumneg 15679 |
. . . . . . . . . . 11
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ฮฃ๐ โ ๐ซ ๐ฆ-((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))) = -ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง))))) |
279 | 235, 275,
278 | 3eqtrd 2781 |
. . . . . . . . . 10
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ฮฃ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
= -ฮฃ๐ โ
๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง))))) |
280 | 279 | oveq2d 7378 |
. . . . . . . . 9
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
โฉ ๐ ))) + ฮฃ๐ โ (๐ซ (๐ฆ โช {๐ง}) โ ๐ซ ๐ฆ)((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))) = (ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
+ -ฮฃ๐ โ
๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))))) |
281 | 137 | a1i 11 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ๐ซ ๐ฆ โ ๐ซ (๐ฆ โช {๐ง})) |
282 | 281 | sselda 3949 |
. . . . . . . . . . . 12
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ ๐ โ ๐ซ (๐ฆ โช {๐ง})) |
283 | 282, 162 | syldan 592 |
. . . . . . . . . . 11
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
โฉ ๐ ))) โ โ) |
284 | 174, 283 | fsumcl 15625 |
. . . . . . . . . 10
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
โ โ) |
285 | 282, 276 | syldan 592 |
. . . . . . . . . . 11
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง ๐ โ ๐ซ ๐ฆ) โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
(โฉ ๐ โฉ ๐ง)))) โ โ) |
286 | 174, 285 | fsumcl 15625 |
. . . . . . . . . 10
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))) โ
โ) |
287 | 284, 286 | negsubd 11525 |
. . . . . . . . 9
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
โฉ ๐ ))) + -ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง))))) =
(ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
โ ฮฃ๐ โ
๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))))) |
288 | 163, 280,
287 | 3eqtrd 2781 |
. . . . . . . 8
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
= (ฮฃ๐ โ
๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
โ ฮฃ๐ โ
๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))))) |
289 | 288 | adantr 482 |
. . . . . . 7
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) โ ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
= (ฮฃ๐ โ
๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))
โ ฮฃ๐ โ
๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ (โฉ ๐
โฉ ๐ง)))))) |
290 | 101, 133,
289 | 3eqtr4d 2787 |
. . . . . 6
โข ((((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โง โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) โ ((โฏโ๐ฅ) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ
โช ๐ง)))) = ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))) |
291 | 290 | ex 414 |
. . . . 5
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง ๐ฅ โ Fin) โ (โ๐ โ Fin
((โฏโ๐) โ
(โฏโ(๐ โฉ
โช ๐ฆ))) = ฮฃ๐ โ ๐ซ ๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ ((โฏโ๐ฅ)
โ (โฏโ(๐ฅ
โฉ (โช ๐ฆ โช ๐ง)))) = ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ ))))) |
292 | 291 | ralrimdva 3152 |
. . . 4
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ โ๐ฅ โ Fin
((โฏโ๐ฅ) โ
(โฏโ(๐ฅ โฉ
(โช ๐ฆ โช ๐ง)))) = ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ ))))) |
293 | | ineq1 4170 |
. . . . . . . 8
โข (๐ = ๐ฅ โ (๐ โฉ (โช ๐ฆ โช ๐ง)) = (๐ฅ โฉ (โช ๐ฆ โช ๐ง))) |
294 | 293 | fveq2d 6851 |
. . . . . . 7
โข (๐ = ๐ฅ โ (โฏโ(๐ โฉ (โช ๐ฆ โช ๐ง))) = (โฏโ(๐ฅ โฉ (โช ๐ฆ โช ๐ง)))) |
295 | 66, 294 | oveq12d 7380 |
. . . . . 6
โข (๐ = ๐ฅ โ ((โฏโ๐) โ (โฏโ(๐ โฉ (โช ๐ฆ โช ๐ง)))) = ((โฏโ๐ฅ) โ (โฏโ(๐ฅ โฉ (โช ๐ฆ โช ๐ง))))) |
296 | | ineq1 4170 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ (๐ โฉ โฉ ๐ ) = (๐ฅ โฉ โฉ ๐ )) |
297 | 296 | fveq2d 6851 |
. . . . . . . 8
โข (๐ = ๐ฅ โ (โฏโ(๐ โฉ โฉ ๐ )) = (โฏโ(๐ฅ โฉ โฉ ๐ ))) |
298 | 297 | oveq2d 7378 |
. . . . . . 7
โข (๐ = ๐ฅ โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ โฉ
โฉ ๐ ))) = ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
โฉ ๐ )))) |
299 | 298 | sumeq2sdv 15596 |
. . . . . 6
โข (๐ = ๐ฅ โ ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
= ฮฃ๐ โ ๐ซ
(๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ฅ โฉ
โฉ ๐ )))) |
300 | 295, 299 | eqeq12d 2753 |
. . . . 5
โข (๐ = ๐ฅ โ (((โฏโ๐) โ (โฏโ(๐ โฉ (โช ๐ฆ โช ๐ง)))) = ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ ((โฏโ๐ฅ)
โ (โฏโ(๐ฅ
โฉ (โช ๐ฆ โช ๐ง)))) = ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ ))))) |
301 | 300 | cbvralvw 3228 |
. . . 4
โข
(โ๐ โ
Fin ((โฏโ๐)
โ (โฏโ(๐
โฉ (โช ๐ฆ โช ๐ง)))) = ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ โ๐ฅ โ Fin
((โฏโ๐ฅ) โ
(โฏโ(๐ฅ โฉ
(โช ๐ฆ โช ๐ง)))) = ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ฅ โฉ โฉ ๐ )))) |
302 | 292, 301 | syl6ibr 252 |
. . 3
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โ๐ โ Fin ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ฆ)))
= ฮฃ๐ โ ๐ซ
๐ฆ((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ โ๐ โ Fin
((โฏโ๐) โ
(โฏโ(๐ โฉ
(โช ๐ฆ โช ๐ง)))) = ฮฃ๐ โ ๐ซ (๐ฆ โช {๐ง})((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ ))))) |
303 | 16, 24, 37, 45, 65, 302 | findcard2s 9116 |
. 2
โข (๐ด โ Fin โ โ๐ โ Fin
((โฏโ๐) โ
(โฏโ(๐ โฉ
โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))) |
304 | | fveq2 6847 |
. . . . 5
โข (๐ = ๐ต โ (โฏโ๐) = (โฏโ๐ต)) |
305 | | ineq1 4170 |
. . . . . 6
โข (๐ = ๐ต โ (๐ โฉ โช ๐ด) = (๐ต โฉ โช ๐ด)) |
306 | 305 | fveq2d 6851 |
. . . . 5
โข (๐ = ๐ต โ (โฏโ(๐ โฉ โช ๐ด)) = (โฏโ(๐ต โฉ โช ๐ด))) |
307 | 304, 306 | oveq12d 7380 |
. . . 4
โข (๐ = ๐ต โ ((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ด))) = ((โฏโ๐ต) โ (โฏโ(๐ต โฉ โช ๐ด)))) |
308 | | simpl 484 |
. . . . . . . 8
โข ((๐ = ๐ต โง ๐ โ ๐ซ ๐ด) โ ๐ = ๐ต) |
309 | 308 | ineq1d 4176 |
. . . . . . 7
โข ((๐ = ๐ต โง ๐ โ ๐ซ ๐ด) โ (๐ โฉ โฉ ๐ ) = (๐ต โฉ โฉ ๐ )) |
310 | 309 | fveq2d 6851 |
. . . . . 6
โข ((๐ = ๐ต โง ๐ โ ๐ซ ๐ด) โ (โฏโ(๐ โฉ โฉ ๐ )) = (โฏโ(๐ต โฉ โฉ ๐ ))) |
311 | 310 | oveq2d 7378 |
. . . . 5
โข ((๐ = ๐ต โง ๐ โ ๐ซ ๐ด) โ ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ โฉ
โฉ ๐ ))) = ((-1โ(โฏโ๐ )) ยท
(โฏโ(๐ต โฉ
โฉ ๐ )))) |
312 | 311 | sumeq2dv 15595 |
. . . 4
โข (๐ = ๐ต โ ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
= ฮฃ๐ โ ๐ซ
๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ต โฉ โฉ ๐ )))) |
313 | 307, 312 | eqeq12d 2753 |
. . 3
โข (๐ = ๐ต โ (((โฏโ๐) โ (โฏโ(๐ โฉ โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โ ((โฏโ๐ต)
โ (โฏโ(๐ต
โฉ โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ต โฉ โฉ ๐ ))))) |
314 | 313 | rspccva 3583 |
. 2
โข
((โ๐ โ
Fin ((โฏโ๐)
โ (โฏโ(๐
โฉ โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ โฉ โฉ ๐ )))
โง ๐ต โ Fin) โ
((โฏโ๐ต) โ
(โฏโ(๐ต โฉ
โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ต โฉ โฉ ๐ )))) |
315 | 303, 314 | sylan 581 |
1
โข ((๐ด โ Fin โง ๐ต โ Fin) โ
((โฏโ๐ต) โ
(โฏโ(๐ต โฉ
โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ต โฉ โฉ ๐ )))) |