Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง (๐ด โ Fin โง ๐ต โ Fin)) โ (๐ด โ Fin โง ๐ต โ Fin)) |
2 | | hashxp 14340 |
. . . 4
โข ((๐ด โ Fin โง ๐ต โ Fin) โ
(โฏโ(๐ด ร
๐ต)) = ((โฏโ๐ด) ยท (โฏโ๐ต))) |
3 | 1, 2 | syl 17 |
. . 3
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง (๐ด โ Fin โง ๐ต โ Fin)) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยท (โฏโ๐ต))) |
4 | | nn0ssre 12422 |
. . . . . . 7
โข
โ0 โ โ |
5 | | hashcl 14262 |
. . . . . . 7
โข (๐ด โ Fin โ
(โฏโ๐ด) โ
โ0) |
6 | 4, 5 | sselid 3943 |
. . . . . 6
โข (๐ด โ Fin โ
(โฏโ๐ด) โ
โ) |
7 | | hashcl 14262 |
. . . . . . 7
โข (๐ต โ Fin โ
(โฏโ๐ต) โ
โ0) |
8 | 4, 7 | sselid 3943 |
. . . . . 6
โข (๐ต โ Fin โ
(โฏโ๐ต) โ
โ) |
9 | 6, 8 | anim12i 614 |
. . . . 5
โข ((๐ด โ Fin โง ๐ต โ Fin) โ
((โฏโ๐ด) โ
โ โง (โฏโ๐ต) โ โ)) |
10 | 1, 9 | syl 17 |
. . . 4
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง (๐ด โ Fin โง ๐ต โ Fin)) โ ((โฏโ๐ด) โ โ โง
(โฏโ๐ต) โ
โ)) |
11 | | rexmul 13196 |
. . . 4
โข
(((โฏโ๐ด)
โ โ โง (โฏโ๐ต) โ โ) โ
((โฏโ๐ด)
ยทe (โฏโ๐ต)) = ((โฏโ๐ด) ยท (โฏโ๐ต))) |
12 | 10, 11 | syl 17 |
. . 3
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง (๐ด โ Fin โง ๐ต โ Fin)) โ ((โฏโ๐ด) ยทe
(โฏโ๐ต)) =
((โฏโ๐ด) ยท
(โฏโ๐ต))) |
13 | 3, 12 | eqtr4d 2776 |
. 2
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง (๐ด โ Fin โง ๐ต โ Fin)) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |
14 | | simpr 486 |
. . . . . . . . . 10
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ ๐ต = โ
) |
15 | 14 | xpeq2d 5664 |
. . . . . . . . 9
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ (๐ด ร ๐ต) = (๐ด ร โ
)) |
16 | | xp0 6111 |
. . . . . . . . 9
โข (๐ด ร โ
) =
โ
|
17 | 15, 16 | eqtrdi 2789 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ (๐ด ร ๐ต) = โ
) |
18 | 17 | fveq2d 6847 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ (โฏโ(๐ด ร ๐ต)) =
(โฏโโ
)) |
19 | | hash0 14273 |
. . . . . . 7
โข
(โฏโโ
) = 0 |
20 | 18, 19 | eqtrdi 2789 |
. . . . . 6
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ (โฏโ(๐ด ร ๐ต)) = 0) |
21 | | simpl 484 |
. . . . . . . . . 10
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ ๐ด โ ๐) |
22 | | hashinf 14241 |
. . . . . . . . . 10
โข ((๐ด โ ๐ โง ยฌ ๐ด โ Fin) โ (โฏโ๐ด) = +โ) |
23 | 21, 22 | sylan 581 |
. . . . . . . . 9
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โ (โฏโ๐ด) = +โ) |
24 | 23 | adantr 482 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ (โฏโ๐ด) = +โ) |
25 | 14 | fveq2d 6847 |
. . . . . . . . 9
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ (โฏโ๐ต) =
(โฏโโ
)) |
26 | 25, 19 | eqtrdi 2789 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ (โฏโ๐ต) = 0) |
27 | 24, 26 | oveq12d 7376 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ ((โฏโ๐ด) ยทe
(โฏโ๐ต)) =
(+โ ยทe 0)) |
28 | | pnfxr 11214 |
. . . . . . . 8
โข +โ
โ โ* |
29 | | xmul01 13192 |
. . . . . . . 8
โข (+โ
โ โ* โ (+โ ยทe 0) =
0) |
30 | 28, 29 | ax-mp 5 |
. . . . . . 7
โข (+โ
ยทe 0) = 0 |
31 | 27, 30 | eqtrdi 2789 |
. . . . . 6
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ ((โฏโ๐ด) ยทe
(โฏโ๐ต)) =
0) |
32 | 20, 31 | eqtr4d 2776 |
. . . . 5
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต = โ
) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |
33 | | simpr 486 |
. . . . . . . . 9
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ ๐ต โ ๐) |
34 | 33 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ ๐ต โ ๐) |
35 | | hashxrcl 14263 |
. . . . . . . 8
โข (๐ต โ ๐ โ (โฏโ๐ต) โ
โ*) |
36 | 34, 35 | syl 17 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ (โฏโ๐ต) โ
โ*) |
37 | | hashgt0 14294 |
. . . . . . . 8
โข ((๐ต โ ๐ โง ๐ต โ โ
) โ 0 <
(โฏโ๐ต)) |
38 | 34, 37 | sylancom 589 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ 0 <
(โฏโ๐ต)) |
39 | | xmulpnf2 13200 |
. . . . . . 7
โข
(((โฏโ๐ต)
โ โ* โง 0 < (โฏโ๐ต)) โ (+โ ยทe
(โฏโ๐ต)) =
+โ) |
40 | 36, 38, 39 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ (+โ
ยทe (โฏโ๐ต)) = +โ) |
41 | 23 | adantr 482 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ (โฏโ๐ด) = +โ) |
42 | 41 | oveq1d 7373 |
. . . . . 6
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ ((โฏโ๐ด) ยทe
(โฏโ๐ต)) =
(+โ ยทe (โฏโ๐ต))) |
43 | 21 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ ๐ด โ ๐) |
44 | 43, 34 | xpexd 7686 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ (๐ด ร ๐ต) โ V) |
45 | | simplr 768 |
. . . . . . . . . 10
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ ยฌ ๐ด โ Fin) |
46 | | 0fin 9118 |
. . . . . . . . . . . 12
โข โ
โ Fin |
47 | | eleq1 2822 |
. . . . . . . . . . . 12
โข (๐ด = โ
โ (๐ด โ Fin โ โ
โ Fin)) |
48 | 46, 47 | mpbiri 258 |
. . . . . . . . . . 11
โข (๐ด = โ
โ ๐ด โ Fin) |
49 | 48 | necon3bi 2967 |
. . . . . . . . . 10
โข (ยฌ
๐ด โ Fin โ ๐ด โ โ
) |
50 | 45, 49 | syl 17 |
. . . . . . . . 9
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ ๐ด โ โ
) |
51 | | simpr 486 |
. . . . . . . . 9
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ ๐ต โ โ
) |
52 | | ioran 983 |
. . . . . . . . . . 11
โข (ยฌ
(๐ด = โ
โจ ๐ต = โ
) โ (ยฌ ๐ด = โ
โง ยฌ ๐ต = โ
)) |
53 | | xpeq0 6113 |
. . . . . . . . . . . 12
โข ((๐ด ร ๐ต) = โ
โ (๐ด = โ
โจ ๐ต = โ
)) |
54 | 53 | necon3abii 2987 |
. . . . . . . . . . 11
โข ((๐ด ร ๐ต) โ โ
โ ยฌ (๐ด = โ
โจ ๐ต = โ
)) |
55 | | df-ne 2941 |
. . . . . . . . . . . 12
โข (๐ด โ โ
โ ยฌ ๐ด = โ
) |
56 | | df-ne 2941 |
. . . . . . . . . . . 12
โข (๐ต โ โ
โ ยฌ ๐ต = โ
) |
57 | 55, 56 | anbi12i 628 |
. . . . . . . . . . 11
โข ((๐ด โ โ
โง ๐ต โ โ
) โ (ยฌ
๐ด = โ
โง ยฌ
๐ต =
โ
)) |
58 | 52, 54, 57 | 3bitr4i 303 |
. . . . . . . . . 10
โข ((๐ด ร ๐ต) โ โ
โ (๐ด โ โ
โง ๐ต โ โ
)) |
59 | 58 | biimpri 227 |
. . . . . . . . 9
โข ((๐ด โ โ
โง ๐ต โ โ
) โ (๐ด ร ๐ต) โ โ
) |
60 | 50, 51, 59 | syl2anc 585 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ (๐ด ร ๐ต) โ โ
) |
61 | 45 | intnanrd 491 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ ยฌ (๐ด โ Fin โง ๐ต โ Fin)) |
62 | | pm4.61 406 |
. . . . . . . . 9
โข (ยฌ
((๐ด ร ๐ต) โ โ
โ (๐ด โ Fin โง ๐ต โ Fin)) โ ((๐ด ร ๐ต) โ โ
โง ยฌ (๐ด โ Fin โง ๐ต โ Fin))) |
63 | | xpfir 9213 |
. . . . . . . . . . 11
โข (((๐ด ร ๐ต) โ Fin โง (๐ด ร ๐ต) โ โ
) โ (๐ด โ Fin โง ๐ต โ Fin)) |
64 | 63 | ex 414 |
. . . . . . . . . 10
โข ((๐ด ร ๐ต) โ Fin โ ((๐ด ร ๐ต) โ โ
โ (๐ด โ Fin โง ๐ต โ Fin))) |
65 | 64 | con3i 154 |
. . . . . . . . 9
โข (ยฌ
((๐ด ร ๐ต) โ โ
โ (๐ด โ Fin โง ๐ต โ Fin)) โ ยฌ
(๐ด ร ๐ต) โ Fin) |
66 | 62, 65 | sylbir 234 |
. . . . . . . 8
โข (((๐ด ร ๐ต) โ โ
โง ยฌ (๐ด โ Fin โง ๐ต โ Fin)) โ ยฌ
(๐ด ร ๐ต) โ Fin) |
67 | 60, 61, 66 | syl2anc 585 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ ยฌ (๐ด ร ๐ต) โ Fin) |
68 | | hashinf 14241 |
. . . . . . 7
โข (((๐ด ร ๐ต) โ V โง ยฌ (๐ด ร ๐ต) โ Fin) โ (โฏโ(๐ด ร ๐ต)) = +โ) |
69 | 44, 67, 68 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ (โฏโ(๐ด ร ๐ต)) = +โ) |
70 | 40, 42, 69 | 3eqtr4rd 2784 |
. . . . 5
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โง ๐ต โ โ
) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |
71 | | exmidne 2950 |
. . . . . 6
โข (๐ต = โ
โจ ๐ต โ โ
) |
72 | 71 | a1i 11 |
. . . . 5
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โ (๐ต = โ
โจ ๐ต โ โ
)) |
73 | 32, 70, 72 | mpjaodan 958 |
. . . 4
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ด โ Fin) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |
74 | 73 | adantlr 714 |
. . 3
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ (๐ด โ Fin โง ๐ต โ Fin)) โง ยฌ ๐ด โ Fin) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |
75 | | simpr 486 |
. . . . . . . . . 10
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ ๐ด = โ
) |
76 | 75 | xpeq1d 5663 |
. . . . . . . . 9
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ (๐ด ร ๐ต) = (โ
ร ๐ต)) |
77 | | 0xp 5731 |
. . . . . . . . 9
โข (โ
ร ๐ต) =
โ
|
78 | 76, 77 | eqtrdi 2789 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ (๐ด ร ๐ต) = โ
) |
79 | 78 | fveq2d 6847 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ (โฏโ(๐ด ร ๐ต)) =
(โฏโโ
)) |
80 | 79, 19 | eqtrdi 2789 |
. . . . . 6
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ (โฏโ(๐ด ร ๐ต)) = 0) |
81 | 75 | fveq2d 6847 |
. . . . . . . . 9
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ (โฏโ๐ด) =
(โฏโโ
)) |
82 | 81, 19 | eqtrdi 2789 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ (โฏโ๐ด) = 0) |
83 | | hashinf 14241 |
. . . . . . . . . 10
โข ((๐ต โ ๐ โง ยฌ ๐ต โ Fin) โ (โฏโ๐ต) = +โ) |
84 | 33, 83 | sylan 581 |
. . . . . . . . 9
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โ (โฏโ๐ต) = +โ) |
85 | 84 | adantr 482 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ (โฏโ๐ต) = +โ) |
86 | 82, 85 | oveq12d 7376 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ ((โฏโ๐ด) ยทe
(โฏโ๐ต)) = (0
ยทe +โ)) |
87 | | xmul02 13193 |
. . . . . . . 8
โข (+โ
โ โ* โ (0 ยทe +โ) =
0) |
88 | 28, 87 | ax-mp 5 |
. . . . . . 7
โข (0
ยทe +โ) = 0 |
89 | 86, 88 | eqtrdi 2789 |
. . . . . 6
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ ((โฏโ๐ด) ยทe
(โฏโ๐ต)) =
0) |
90 | 80, 89 | eqtr4d 2776 |
. . . . 5
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด = โ
) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |
91 | | hashxrcl 14263 |
. . . . . . . 8
โข (๐ด โ ๐ โ (โฏโ๐ด) โ
โ*) |
92 | 91 | ad3antrrr 729 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ (โฏโ๐ด) โ
โ*) |
93 | | hashgt0 14294 |
. . . . . . . 8
โข ((๐ด โ ๐ โง ๐ด โ โ
) โ 0 <
(โฏโ๐ด)) |
94 | 93 | ad4ant14 751 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ 0 <
(โฏโ๐ด)) |
95 | | xmulpnf1 13199 |
. . . . . . 7
โข
(((โฏโ๐ด)
โ โ* โง 0 < (โฏโ๐ด)) โ ((โฏโ๐ด) ยทe +โ) =
+โ) |
96 | 92, 94, 95 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ ((โฏโ๐ด) ยทe +โ)
= +โ) |
97 | 84 | adantr 482 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ (โฏโ๐ต) = +โ) |
98 | 97 | oveq2d 7374 |
. . . . . 6
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ ((โฏโ๐ด) ยทe
(โฏโ๐ต)) =
((โฏโ๐ด)
ยทe +โ)) |
99 | 21 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ ๐ด โ ๐) |
100 | 33 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ ๐ต โ ๐) |
101 | 99, 100 | xpexd 7686 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ (๐ด ร ๐ต) โ V) |
102 | | simpr 486 |
. . . . . . . . 9
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ ๐ด โ โ
) |
103 | | simplr 768 |
. . . . . . . . . 10
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ ยฌ ๐ต โ Fin) |
104 | | eleq1 2822 |
. . . . . . . . . . . 12
โข (๐ต = โ
โ (๐ต โ Fin โ โ
โ Fin)) |
105 | 46, 104 | mpbiri 258 |
. . . . . . . . . . 11
โข (๐ต = โ
โ ๐ต โ Fin) |
106 | 105 | necon3bi 2967 |
. . . . . . . . . 10
โข (ยฌ
๐ต โ Fin โ ๐ต โ โ
) |
107 | 103, 106 | syl 17 |
. . . . . . . . 9
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ ๐ต โ โ
) |
108 | 102, 107,
59 | syl2anc 585 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ (๐ด ร ๐ต) โ โ
) |
109 | 103 | intnand 490 |
. . . . . . . 8
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ ยฌ (๐ด โ Fin โง ๐ต โ Fin)) |
110 | 108, 109,
66 | syl2anc 585 |
. . . . . . 7
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ ยฌ (๐ด ร ๐ต) โ Fin) |
111 | 101, 110,
68 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ (โฏโ(๐ด ร ๐ต)) = +โ) |
112 | 96, 98, 111 | 3eqtr4rd 2784 |
. . . . 5
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โง ๐ด โ โ
) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |
113 | | exmidne 2950 |
. . . . . 6
โข (๐ด = โ
โจ ๐ด โ โ
) |
114 | 113 | a1i 11 |
. . . . 5
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โ (๐ด = โ
โจ ๐ด โ โ
)) |
115 | 90, 112, 114 | mpjaodan 958 |
. . . 4
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ ๐ต โ Fin) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |
116 | 115 | adantlr 714 |
. . 3
โข ((((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ (๐ด โ Fin โง ๐ต โ Fin)) โง ยฌ ๐ต โ Fin) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |
117 | | simpr 486 |
. . . 4
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ (๐ด โ Fin โง ๐ต โ Fin)) โ ยฌ (๐ด โ Fin โง ๐ต โ Fin)) |
118 | | ianor 981 |
. . . 4
โข (ยฌ
(๐ด โ Fin โง ๐ต โ Fin) โ (ยฌ ๐ด โ Fin โจ ยฌ ๐ต โ Fin)) |
119 | 117, 118 | sylib 217 |
. . 3
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ (๐ด โ Fin โง ๐ต โ Fin)) โ (ยฌ ๐ด โ Fin โจ ยฌ ๐ต โ Fin)) |
120 | 74, 116, 119 | mpjaodan 958 |
. 2
โข (((๐ด โ ๐ โง ๐ต โ ๐) โง ยฌ (๐ด โ Fin โง ๐ต โ Fin)) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |
121 | | exmidd 895 |
. 2
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ ((๐ด โ Fin โง ๐ต โ Fin) โจ ยฌ (๐ด โ Fin โง ๐ต โ Fin))) |
122 | 13, 120, 121 | mpjaodan 958 |
1
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยทe (โฏโ๐ต))) |