Step | Hyp | Ref
| Expression |
1 | | ssid 3971 |
. 2
โข ๐ด โ ๐ด |
2 | | ablfac1eulem.2 |
. . 3
โข (๐ โ ๐ด โ Fin) |
3 | | sseq1 3974 |
. . . . . 6
โข (๐ฆ = โ
โ (๐ฆ โ ๐ด โ โ
โ ๐ด)) |
4 | | difeq1 4080 |
. . . . . . . . . . . . 13
โข (๐ฆ = โ
โ (๐ฆ โ {๐}) = (โ
โ {๐})) |
5 | | 0dif 4366 |
. . . . . . . . . . . . 13
โข (โ
โ {๐}) =
โ
|
6 | 4, 5 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข (๐ฆ = โ
โ (๐ฆ โ {๐}) = โ
) |
7 | 6 | reseq2d 5942 |
. . . . . . . . . . 11
โข (๐ฆ = โ
โ (๐ โพ (๐ฆ โ {๐})) = (๐ โพ โ
)) |
8 | | res0 5946 |
. . . . . . . . . . 11
โข (๐ โพ โ
) =
โ
|
9 | 7, 8 | eqtrdi 2793 |
. . . . . . . . . 10
โข (๐ฆ = โ
โ (๐ โพ (๐ฆ โ {๐})) = โ
) |
10 | 9 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ฆ = โ
โ (๐บ DProd (๐ โพ (๐ฆ โ {๐}))) = (๐บ DProd โ
)) |
11 | 10 | fveq2d 6851 |
. . . . . . . 8
โข (๐ฆ = โ
โ
(โฏโ(๐บ DProd
(๐ โพ (๐ฆ โ {๐})))) = (โฏโ(๐บ DProd โ
))) |
12 | 11 | breq2d 5122 |
. . . . . . 7
โข (๐ฆ = โ
โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) โ ๐ โฅ (โฏโ(๐บ DProd โ
)))) |
13 | 12 | notbid 318 |
. . . . . 6
โข (๐ฆ = โ
โ (ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd โ
)))) |
14 | 3, 13 | imbi12d 345 |
. . . . 5
โข (๐ฆ = โ
โ ((๐ฆ โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐}))))) โ (โ
โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd โ
))))) |
15 | 14 | imbi2d 341 |
. . . 4
โข (๐ฆ = โ
โ ((๐ โ (๐ฆ โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))))) โ (๐ โ (โ
โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd โ
)))))) |
16 | | sseq1 3974 |
. . . . . 6
โข (๐ฆ = ๐ง โ (๐ฆ โ ๐ด โ ๐ง โ ๐ด)) |
17 | | difeq1 4080 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ง โ (๐ฆ โ {๐}) = (๐ง โ {๐})) |
18 | 17 | reseq2d 5942 |
. . . . . . . . . 10
โข (๐ฆ = ๐ง โ (๐ โพ (๐ฆ โ {๐})) = (๐ โพ (๐ง โ {๐}))) |
19 | 18 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ฆ = ๐ง โ (๐บ DProd (๐ โพ (๐ฆ โ {๐}))) = (๐บ DProd (๐ โพ (๐ง โ {๐})))) |
20 | 19 | fveq2d 6851 |
. . . . . . . 8
โข (๐ฆ = ๐ง โ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) = (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐}))))) |
21 | 20 | breq2d 5122 |
. . . . . . 7
โข (๐ฆ = ๐ง โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) โ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))))) |
22 | 21 | notbid 318 |
. . . . . 6
โข (๐ฆ = ๐ง โ (ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))))) |
23 | 16, 22 | imbi12d 345 |
. . . . 5
โข (๐ฆ = ๐ง โ ((๐ฆ โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐}))))) โ (๐ง โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐}))))))) |
24 | 23 | imbi2d 341 |
. . . 4
โข (๐ฆ = ๐ง โ ((๐ โ (๐ฆ โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))))) โ (๐ โ (๐ง โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))))))) |
25 | | sseq1 3974 |
. . . . . 6
โข (๐ฆ = (๐ง โช {๐}) โ (๐ฆ โ ๐ด โ (๐ง โช {๐}) โ ๐ด)) |
26 | | difeq1 4080 |
. . . . . . . . . . 11
โข (๐ฆ = (๐ง โช {๐}) โ (๐ฆ โ {๐}) = ((๐ง โช {๐}) โ {๐})) |
27 | 26 | reseq2d 5942 |
. . . . . . . . . 10
โข (๐ฆ = (๐ง โช {๐}) โ (๐ โพ (๐ฆ โ {๐})) = (๐ โพ ((๐ง โช {๐}) โ {๐}))) |
28 | 27 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ฆ = (๐ง โช {๐}) โ (๐บ DProd (๐ โพ (๐ฆ โ {๐}))) = (๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))) |
29 | 28 | fveq2d 6851 |
. . . . . . . 8
โข (๐ฆ = (๐ง โช {๐}) โ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) = (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐}))))) |
30 | 29 | breq2d 5122 |
. . . . . . 7
โข (๐ฆ = (๐ง โช {๐}) โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) โ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))))) |
31 | 30 | notbid 318 |
. . . . . 6
โข (๐ฆ = (๐ง โช {๐}) โ (ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))))) |
32 | 25, 31 | imbi12d 345 |
. . . . 5
โข (๐ฆ = (๐ง โช {๐}) โ ((๐ฆ โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐}))))) โ ((๐ง โช {๐}) โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐}))))))) |
33 | 32 | imbi2d 341 |
. . . 4
โข (๐ฆ = (๐ง โช {๐}) โ ((๐ โ (๐ฆ โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))))) โ (๐ โ ((๐ง โช {๐}) โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))))))) |
34 | | sseq1 3974 |
. . . . . 6
โข (๐ฆ = ๐ด โ (๐ฆ โ ๐ด โ ๐ด โ ๐ด)) |
35 | | difeq1 4080 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ด โ (๐ฆ โ {๐}) = (๐ด โ {๐})) |
36 | 35 | reseq2d 5942 |
. . . . . . . . . 10
โข (๐ฆ = ๐ด โ (๐ โพ (๐ฆ โ {๐})) = (๐ โพ (๐ด โ {๐}))) |
37 | 36 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ฆ = ๐ด โ (๐บ DProd (๐ โพ (๐ฆ โ {๐}))) = (๐บ DProd (๐ โพ (๐ด โ {๐})))) |
38 | 37 | fveq2d 6851 |
. . . . . . . 8
โข (๐ฆ = ๐ด โ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) = (โฏโ(๐บ DProd (๐ โพ (๐ด โ {๐}))))) |
39 | 38 | breq2d 5122 |
. . . . . . 7
โข (๐ฆ = ๐ด โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) โ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ด โ {๐})))))) |
40 | 39 | notbid 318 |
. . . . . 6
โข (๐ฆ = ๐ด โ (ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ด โ {๐})))))) |
41 | 34, 40 | imbi12d 345 |
. . . . 5
โข (๐ฆ = ๐ด โ ((๐ฆ โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐}))))) โ (๐ด โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ด โ {๐}))))))) |
42 | 41 | imbi2d 341 |
. . . 4
โข (๐ฆ = ๐ด โ ((๐ โ (๐ฆ โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ฆ โ {๐})))))) โ (๐ โ (๐ด โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ด โ {๐})))))))) |
43 | | ablfac1eulem.1 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
44 | | nprmdvds1 16589 |
. . . . . . 7
โข (๐ โ โ โ ยฌ
๐ โฅ
1) |
45 | 43, 44 | syl 17 |
. . . . . 6
โข (๐ โ ยฌ ๐ โฅ 1) |
46 | | ablfac1.g |
. . . . . . . . . . 11
โข (๐ โ ๐บ โ Abel) |
47 | | ablgrp 19574 |
. . . . . . . . . . 11
โข (๐บ โ Abel โ ๐บ โ Grp) |
48 | | eqid 2737 |
. . . . . . . . . . . 12
โข
(0gโ๐บ) = (0gโ๐บ) |
49 | 48 | dprd0 19817 |
. . . . . . . . . . 11
โข (๐บ โ Grp โ (๐บdom DProd โ
โง (๐บ DProd โ
) =
{(0gโ๐บ)})) |
50 | 46, 47, 49 | 3syl 18 |
. . . . . . . . . 10
โข (๐ โ (๐บdom DProd โ
โง (๐บ DProd โ
) =
{(0gโ๐บ)})) |
51 | 50 | simprd 497 |
. . . . . . . . 9
โข (๐ โ (๐บ DProd โ
) =
{(0gโ๐บ)}) |
52 | 51 | fveq2d 6851 |
. . . . . . . 8
โข (๐ โ (โฏโ(๐บ DProd โ
)) =
(โฏโ{(0gโ๐บ)})) |
53 | | fvex 6860 |
. . . . . . . . 9
โข
(0gโ๐บ) โ V |
54 | | hashsng 14276 |
. . . . . . . . 9
โข
((0gโ๐บ) โ V โ
(โฏโ{(0gโ๐บ)}) = 1) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . 8
โข
(โฏโ{(0gโ๐บ)}) = 1 |
56 | 52, 55 | eqtrdi 2793 |
. . . . . . 7
โข (๐ โ (โฏโ(๐บ DProd โ
)) =
1) |
57 | 56 | breq2d 5122 |
. . . . . 6
โข (๐ โ (๐ โฅ (โฏโ(๐บ DProd โ
)) โ ๐ โฅ 1)) |
58 | 45, 57 | mtbird 325 |
. . . . 5
โข (๐ โ ยฌ ๐ โฅ (โฏโ(๐บ DProd โ
))) |
59 | 58 | a1d 25 |
. . . 4
โข (๐ โ (โ
โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd โ
)))) |
60 | | ssun1 4137 |
. . . . . . . . . 10
โข ๐ง โ (๐ง โช {๐}) |
61 | | sstr 3957 |
. . . . . . . . . 10
โข ((๐ง โ (๐ง โช {๐}) โง (๐ง โช {๐}) โ ๐ด) โ ๐ง โ ๐ด) |
62 | 60, 61 | mpan 689 |
. . . . . . . . 9
โข ((๐ง โช {๐}) โ ๐ด โ ๐ง โ ๐ด) |
63 | 62 | imim1i 63 |
. . . . . . . 8
โข ((๐ง โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐}))))) โ ((๐ง โช {๐}) โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))))) |
64 | | ablfac1eu.1 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐บdom DProd ๐ โง (๐บ DProd ๐) = ๐ต)) |
65 | 64 | simpld 496 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐บdom DProd ๐) |
66 | | ablfac1eu.2 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ dom ๐ = ๐ด) |
67 | 65, 66 | dprdf2 19793 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐:๐ดโถ(SubGrpโ๐บ)) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐:๐ดโถ(SubGrpโ๐บ)) |
69 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ง โช {๐}) โ ๐ด) |
70 | 69 | ssdifssd 4107 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ((๐ง โช {๐}) โ {๐}) โ ๐ด) |
71 | 68, 70 | fssresd 6714 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ โพ ((๐ง โช {๐}) โ {๐})):((๐ง โช {๐}) โ {๐})โถ(SubGrpโ๐บ)) |
72 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ยฌ ๐ โ ๐ง) |
73 | | disjsn 4677 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ง โฉ {๐}) = โ
โ ยฌ ๐ โ ๐ง) |
74 | 72, 73 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ง โฉ {๐}) = โ
) |
75 | 74 | difeq1d 4086 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ((๐ง โฉ {๐}) โ {๐}) = (โ
โ {๐})) |
76 | | difindir 4247 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ง โฉ {๐}) โ {๐}) = ((๐ง โ {๐}) โฉ ({๐} โ {๐})) |
77 | 75, 76, 5 | 3eqtr3g 2800 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ((๐ง โ {๐}) โฉ ({๐} โ {๐})) = โ
) |
78 | | difundir 4245 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ง โช {๐}) โ {๐}) = ((๐ง โ {๐}) โช ({๐} โ {๐})) |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ((๐ง โช {๐}) โ {๐}) = ((๐ง โ {๐}) โช ({๐} โ {๐}))) |
80 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
โข
(LSSumโ๐บ) =
(LSSumโ๐บ) |
81 | 65 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐บdom DProd ๐) |
82 | 66 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ dom ๐ = ๐ด) |
83 | 81, 82, 70 | dprdres 19814 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บdom DProd (๐ โพ ((๐ง โช {๐}) โ {๐})) โง (๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐}))) โ (๐บ DProd ๐))) |
84 | 83 | simpld 496 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐บdom DProd (๐ โพ ((๐ง โช {๐}) โ {๐}))) |
85 | 71, 77, 79, 80, 84 | dprdsplit 19834 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐}))) = ((๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐})))(LSSumโ๐บ)(๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))))) |
86 | 85 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))) = (โฏโ((๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐})))(LSSumโ๐บ)(๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐})))))) |
87 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
โข
(Cntzโ๐บ) =
(Cntzโ๐บ) |
88 | 71 | fdmd 6684 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ dom (๐ โพ ((๐ง โช {๐}) โ {๐})) = ((๐ง โช {๐}) โ {๐})) |
89 | | ssdif 4104 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง โ (๐ง โช {๐}) โ (๐ง โ {๐}) โ ((๐ง โช {๐}) โ {๐})) |
90 | 60, 89 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ง โ {๐}) โ ((๐ง โช {๐}) โ {๐})) |
91 | 84, 88, 90 | dprdres 19814 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บdom DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐})) โง (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) โ (๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐}))))) |
92 | 91 | simpld 496 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐บdom DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) |
93 | | dprdsubg 19810 |
. . . . . . . . . . . . . . . . 17
โข (๐บdom DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐})) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) โ (SubGrpโ๐บ)) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) โ (SubGrpโ๐บ)) |
95 | | ssun2 4138 |
. . . . . . . . . . . . . . . . . . . 20
โข {๐} โ (๐ง โช {๐}) |
96 | | ssdif 4104 |
. . . . . . . . . . . . . . . . . . . 20
โข ({๐} โ (๐ง โช {๐}) โ ({๐} โ {๐}) โ ((๐ง โช {๐}) โ {๐})) |
97 | 95, 96 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ({๐} โ {๐}) โ ((๐ง โช {๐}) โ {๐})) |
98 | 84, 88, 97 | dprdres 19814 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บdom DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐})) โง (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))) โ (๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐}))))) |
99 | 98 | simpld 496 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐บdom DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))) |
100 | | dprdsubg 19810 |
. . . . . . . . . . . . . . . . 17
โข (๐บdom DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐})) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))) โ (SubGrpโ๐บ)) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))) โ (SubGrpโ๐บ)) |
102 | 84, 88, 90, 97, 77, 48 | dprddisj2 19825 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ((๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) โฉ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐})))) = {(0gโ๐บ)}) |
103 | 84, 88, 90, 97, 77, 87 | dprdcntz2 19824 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) โ ((Cntzโ๐บ)โ(๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))))) |
104 | | ablfac1.f |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ต โ Fin) |
105 | 104 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐ต โ Fin) |
106 | | ablfac1.b |
. . . . . . . . . . . . . . . . . 18
โข ๐ต = (Baseโ๐บ) |
107 | 106 | dprdssv 19802 |
. . . . . . . . . . . . . . . . 17
โข (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) โ ๐ต |
108 | | ssfi 9124 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ Fin โง (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) โ ๐ต) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) โ Fin) |
109 | 105, 107,
108 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) โ Fin) |
110 | 106 | dprdssv 19802 |
. . . . . . . . . . . . . . . . 17
โข (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))) โ ๐ต |
111 | | ssfi 9124 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ Fin โง (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))) โ ๐ต) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))) โ Fin) |
112 | 105, 110,
111 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))) โ Fin) |
113 | 80, 48, 87, 94, 101, 102, 103, 109, 112 | lsmhash 19494 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (โฏโ((๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐})))(LSSumโ๐บ)(๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))))) = ((โฏโ(๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐})))) ยท (โฏโ(๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐})))))) |
114 | 90 | resabs1d 5973 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐})) = (๐ โพ (๐ง โ {๐}))) |
115 | 114 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐}))) = (๐บ DProd (๐ โพ (๐ง โ {๐})))) |
116 | 115 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (โฏโ(๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐})))) = (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐}))))) |
117 | 97 | resabs1d 5973 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐})) = (๐ โพ ({๐} โ {๐}))) |
118 | 117 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))) = (๐บ DProd (๐ โพ ({๐} โ {๐})))) |
119 | 118 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (โฏโ(๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐})))) = (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))) |
120 | 116, 119 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ((โฏโ(๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ (๐ง โ {๐})))) ยท (โฏโ(๐บ DProd ((๐ โพ ((๐ง โช {๐}) โ {๐})) โพ ({๐} โ {๐}))))) = ((โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) ยท (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))))) |
121 | 86, 113, 120 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))) = ((โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) ยท (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))))) |
122 | 121 | breq2d 5122 |
. . . . . . . . . . . . 13
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))) โ ๐ โฅ ((โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) ยท (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))))) |
123 | 43 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐ โ โ) |
124 | 106 | dprdssv 19802 |
. . . . . . . . . . . . . . . . 17
โข (๐บ DProd (๐ โพ (๐ง โ {๐}))) โ ๐ต |
125 | | ssfi 9124 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ Fin โง (๐บ DProd (๐ โพ (๐ง โ {๐}))) โ ๐ต) โ (๐บ DProd (๐ โพ (๐ง โ {๐}))) โ Fin) |
126 | 105, 124,
125 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บ DProd (๐ โพ (๐ง โ {๐}))) โ Fin) |
127 | | hashcl 14263 |
. . . . . . . . . . . . . . . 16
โข ((๐บ DProd (๐ โพ (๐ง โ {๐}))) โ Fin โ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) โ
โ0) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) โ
โ0) |
129 | 128 | nn0zd 12532 |
. . . . . . . . . . . . . 14
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) โ โค) |
130 | 106 | dprdssv 19802 |
. . . . . . . . . . . . . . . . 17
โข (๐บ DProd (๐ โพ ({๐} โ {๐}))) โ ๐ต |
131 | | ssfi 9124 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ Fin โง (๐บ DProd (๐ โพ ({๐} โ {๐}))) โ ๐ต) โ (๐บ DProd (๐ โพ ({๐} โ {๐}))) โ Fin) |
132 | 105, 130,
131 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐บ DProd (๐ โพ ({๐} โ {๐}))) โ Fin) |
133 | | hashcl 14263 |
. . . . . . . . . . . . . . . 16
โข ((๐บ DProd (๐ โพ ({๐} โ {๐}))) โ Fin โ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))) โ
โ0) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))) โ
โ0) |
135 | 134 | nn0zd 12532 |
. . . . . . . . . . . . . 14
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))) โ โค) |
136 | | euclemma 16596 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง
(โฏโ(๐บ DProd
(๐ โพ (๐ง โ {๐})))) โ โค โง
(โฏโ(๐บ DProd
(๐ โพ ({๐} โ {๐})))) โ โค) โ (๐ โฅ ((โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) ยท (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))) โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) โจ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))))) |
137 | 123, 129,
135, 136 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ โฅ ((โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) ยท (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))) โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) โจ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))))) |
138 | 122, 137 | bitrd 279 |
. . . . . . . . . . . 12
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))) โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) โจ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))))) |
139 | 45 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ ยฌ ๐ โฅ 1) |
140 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ ๐ = ๐) |
141 | 140 | sneqd 4603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ {๐} = {๐}) |
142 | 141 | difeq1d 4086 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ ({๐} โ {๐}) = ({๐} โ {๐})) |
143 | | difid 4335 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ({๐} โ {๐}) = โ
|
144 | 142, 143 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ ({๐} โ {๐}) = โ
) |
145 | 144 | reseq2d 5942 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ (๐ โพ ({๐} โ {๐})) = (๐ โพ โ
)) |
146 | 145, 8 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ (๐ โพ ({๐} โ {๐})) = โ
) |
147 | 146 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ (๐บ DProd (๐ โพ ({๐} โ {๐}))) = (๐บ DProd โ
)) |
148 | 51 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ (๐บ DProd โ
) =
{(0gโ๐บ)}) |
149 | 147, 148 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ (๐บ DProd (๐ โพ ({๐} โ {๐}))) = {(0gโ๐บ)}) |
150 | 149 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))) =
(โฏโ{(0gโ๐บ)})) |
151 | 150, 55 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))) = 1) |
152 | 151 | breq2d 5122 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))) โ ๐ โฅ 1)) |
153 | 139, 152 | mtbird 325 |
. . . . . . . . . . . . . 14
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ = ๐) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))) |
154 | | ablfac1.1 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ด โ โ) |
155 | 154 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐ด โ โ) |
156 | 69 | unssbd 4153 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ {๐} โ ๐ด) |
157 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ๐ โ V |
158 | 157 | snss 4751 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ด โ {๐} โ ๐ด) |
159 | 156, 158 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐ โ ๐ด) |
160 | 155, 159 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐ โ โ) |
161 | | ablfac1eu.3 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ
โ0) |
162 | 159, 161 | syldan 592 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ๐ถ โ
โ0) |
163 | | prmdvdsexpr 16600 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ โง ๐ถ โ โ0)
โ (๐ โฅ (๐โ๐ถ) โ ๐ = ๐)) |
164 | 123, 160,
162, 163 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ โฅ (๐โ๐ถ) โ ๐ = ๐)) |
165 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ ๐ = ๐) |
166 | 164, 165 | syl6ib 251 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ โฅ (๐โ๐ถ) โ ๐ = ๐)) |
167 | 166 | necon3ad 2957 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ โ ๐ โ ยฌ ๐ โฅ (๐โ๐ถ))) |
168 | 167 | imp 408 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ ยฌ ๐ โฅ (๐โ๐ถ)) |
169 | | disjsn2 4678 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ โ ({๐} โฉ {๐}) = โ
) |
170 | 169 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ ({๐} โฉ {๐}) = โ
) |
171 | | disj3 4418 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (({๐} โฉ {๐}) = โ
โ {๐} = ({๐} โ {๐})) |
172 | 170, 171 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ {๐} = ({๐} โ {๐})) |
173 | 172 | reseq2d 5942 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ (๐ โพ {๐}) = (๐ โพ ({๐} โ {๐}))) |
174 | 173 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ (๐บ DProd (๐ โพ {๐})) = (๐บ DProd (๐ โพ ({๐} โ {๐})))) |
175 | 65 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ ๐บdom DProd ๐) |
176 | 66 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ dom ๐ = ๐ด) |
177 | 159 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ ๐ โ ๐ด) |
178 | 175, 176,
177 | dpjlem 19837 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ (๐บ DProd (๐ โพ {๐})) = (๐โ๐)) |
179 | 174, 178 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ (๐บ DProd (๐ โพ ({๐} โ {๐}))) = (๐โ๐)) |
180 | 179 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))) = (โฏโ(๐โ๐))) |
181 | | ablfac1eu.4 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (๐โ๐ถ)) |
182 | 159, 181 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (โฏโ(๐โ๐)) = (๐โ๐ถ)) |
183 | 182 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ (โฏโ(๐โ๐)) = (๐โ๐ถ)) |
184 | 180, 183 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))) = (๐โ๐ถ)) |
185 | 184 | breq2d 5122 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐})))) โ ๐ โฅ (๐โ๐ถ))) |
186 | 168, 185 | mtbird 325 |
. . . . . . . . . . . . . 14
โข (((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โง ๐ โ ๐) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))) |
187 | 153, 186 | pm2.61dane 3033 |
. . . . . . . . . . . . 13
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))) |
188 | | orel2 890 |
. . . . . . . . . . . . 13
โข (ยฌ
๐ โฅ
(โฏโ(๐บ DProd
(๐ โพ ({๐} โ {๐})))) โ ((๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) โจ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))) โ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))))) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ ((๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) โจ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ({๐} โ {๐}))))) โ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))))) |
190 | 138, 189 | sylbid 239 |
. . . . . . . . . . 11
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))) โ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))))) |
191 | 190 | con3d 152 |
. . . . . . . . . 10
โข ((๐ โง (ยฌ ๐ โ ๐ง โง (๐ง โช {๐}) โ ๐ด)) โ (ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))))) |
192 | 191 | expr 458 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ โ ๐ง) โ ((๐ง โช {๐}) โ ๐ด โ (ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))) โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐}))))))) |
193 | 192 | a2d 29 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ โ ๐ง) โ (((๐ง โช {๐}) โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐}))))) โ ((๐ง โช {๐}) โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐}))))))) |
194 | 63, 193 | syl5 34 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ โ ๐ง) โ ((๐ง โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐}))))) โ ((๐ง โช {๐}) โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐}))))))) |
195 | 194 | expcom 415 |
. . . . . 6
โข (ยฌ
๐ โ ๐ง โ (๐ โ ((๐ง โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐}))))) โ ((๐ง โช {๐}) โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))))))) |
196 | 195 | adantl 483 |
. . . . 5
โข ((๐ง โ Fin โง ยฌ ๐ โ ๐ง) โ (๐ โ ((๐ง โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐}))))) โ ((๐ง โช {๐}) โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))))))) |
197 | 196 | a2d 29 |
. . . 4
โข ((๐ง โ Fin โง ยฌ ๐ โ ๐ง) โ ((๐ โ (๐ง โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ง โ {๐})))))) โ (๐ โ ((๐ง โช {๐}) โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ ((๐ง โช {๐}) โ {๐})))))))) |
198 | 15, 24, 33, 42, 59, 197 | findcard2s 9116 |
. . 3
โข (๐ด โ Fin โ (๐ โ (๐ด โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ด โ {๐}))))))) |
199 | 2, 198 | mpcom 38 |
. 2
โข (๐ โ (๐ด โ ๐ด โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ด โ {๐})))))) |
200 | 1, 199 | mpi 20 |
1
โข (๐ โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ด โ {๐}))))) |