Step | Hyp | Ref
| Expression |
1 | | fvex 6856 |
. . . . . . . . 9
β’
(BaseβπΊ)
β V |
2 | 1 | rabex 5290 |
. . . . . . . 8
β’ {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} β V |
3 | | simp2l 1200 |
. . . . . . . . . . 11
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π¦ β (SubGrpβπΊ)) |
4 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(BaseβπΊ) =
(BaseβπΊ) |
5 | 4 | subgss 18934 |
. . . . . . . . . . 11
β’ (π¦ β (SubGrpβπΊ) β π¦ β (BaseβπΊ)) |
6 | 3, 5 | syl 17 |
. . . . . . . . . 10
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π¦ β (BaseβπΊ)) |
7 | | simpl2l 1227 |
. . . . . . . . . . . 12
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π¦) β π¦ β (SubGrpβπΊ)) |
8 | | simp3l 1202 |
. . . . . . . . . . . . . . 15
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (β―βπ¦) = π) |
9 | | simp1r 1199 |
. . . . . . . . . . . . . . . 16
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π β β) |
10 | 9 | nnnn0d 12478 |
. . . . . . . . . . . . . . 15
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π β
β0) |
11 | 8, 10 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (β―βπ¦) β
β0) |
12 | | vex 3448 |
. . . . . . . . . . . . . . 15
β’ π¦ β V |
13 | | hashclb 14264 |
. . . . . . . . . . . . . . 15
β’ (π¦ β V β (π¦ β Fin β
(β―βπ¦) β
β0)) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (π¦ β Fin β
(β―βπ¦) β
β0) |
15 | 11, 14 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π¦ β Fin) |
16 | 15 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π¦) β π¦ β Fin) |
17 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π¦) β π§ β π¦) |
18 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(odβπΊ) =
(odβπΊ) |
19 | 18 | odsubdvds 19358 |
. . . . . . . . . . . 12
β’ ((π¦ β (SubGrpβπΊ) β§ π¦ β Fin β§ π§ β π¦) β ((odβπΊ)βπ§) β₯ (β―βπ¦)) |
20 | 7, 16, 17, 19 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π¦) β ((odβπΊ)βπ§) β₯ (β―βπ¦)) |
21 | 8 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π¦) β (β―βπ¦) = π) |
22 | 20, 21 | breqtrd 5132 |
. . . . . . . . . 10
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π¦) β ((odβπΊ)βπ§) β₯ π) |
23 | 6, 22 | ssrabdv 4032 |
. . . . . . . . 9
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π¦ β {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π}) |
24 | | simp2r 1201 |
. . . . . . . . . . 11
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π₯ β (SubGrpβπΊ)) |
25 | 4 | subgss 18934 |
. . . . . . . . . . 11
β’ (π₯ β (SubGrpβπΊ) β π₯ β (BaseβπΊ)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π₯ β (BaseβπΊ)) |
27 | | simpl2r 1228 |
. . . . . . . . . . . 12
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π₯) β π₯ β (SubGrpβπΊ)) |
28 | | simp3r 1203 |
. . . . . . . . . . . . . . 15
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (β―βπ₯) = π) |
29 | 28, 10 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (β―βπ₯) β
β0) |
30 | | vex 3448 |
. . . . . . . . . . . . . . 15
β’ π₯ β V |
31 | | hashclb 14264 |
. . . . . . . . . . . . . . 15
β’ (π₯ β V β (π₯ β Fin β
(β―βπ₯) β
β0)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (π₯ β Fin β
(β―βπ₯) β
β0) |
33 | 29, 32 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π₯ β Fin) |
34 | 33 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π₯) β π₯ β Fin) |
35 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π₯) β π§ β π₯) |
36 | 18 | odsubdvds 19358 |
. . . . . . . . . . . 12
β’ ((π₯ β (SubGrpβπΊ) β§ π₯ β Fin β§ π§ β π₯) β ((odβπΊ)βπ§) β₯ (β―βπ₯)) |
37 | 27, 34, 35, 36 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π₯) β ((odβπΊ)βπ§) β₯ (β―βπ₯)) |
38 | 28 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π₯) β (β―βπ₯) = π) |
39 | 37, 38 | breqtrd 5132 |
. . . . . . . . . 10
β’ ((((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β§ π§ β π₯) β ((odβπΊ)βπ§) β₯ π) |
40 | 26, 39 | ssrabdv 4032 |
. . . . . . . . 9
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π₯ β {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π}) |
41 | 23, 40 | unssd 4147 |
. . . . . . . 8
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (π¦ βͺ π₯) β {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π}) |
42 | | ssdomg 8943 |
. . . . . . . 8
β’ ({π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} β V β ((π¦ βͺ π₯) β {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} β (π¦ βͺ π₯) βΌ {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π})) |
43 | 2, 41, 42 | mpsyl 68 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (π¦ βͺ π₯) βΌ {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π}) |
44 | | idomsubgmo.g |
. . . . . . . . . . 11
β’ πΊ = ((mulGrpβπ
) βΎs
(Unitβπ
)) |
45 | 44, 4, 18 | idomodle 41566 |
. . . . . . . . . 10
β’ ((π
β IDomn β§ π β β) β
(β―β{π§ β
(BaseβπΊ) β£
((odβπΊ)βπ§) β₯ π}) β€ π) |
46 | 45 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (β―β{π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π}) β€ π) |
47 | 46, 8 | breqtrrd 5134 |
. . . . . . . 8
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (β―β{π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π}) β€ (β―βπ¦)) |
48 | 2 | a1i 11 |
. . . . . . . . . 10
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} β V) |
49 | | hashbnd 14242 |
. . . . . . . . . 10
β’ (({π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} β V β§ (β―βπ¦) β β0
β§ (β―β{π§
β (BaseβπΊ)
β£ ((odβπΊ)βπ§) β₯ π}) β€ (β―βπ¦)) β {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} β Fin) |
50 | 48, 11, 47, 49 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} β Fin) |
51 | | hashdom 14285 |
. . . . . . . . 9
β’ (({π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} β Fin β§ π¦ β V) β ((β―β{π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π}) β€ (β―βπ¦) β {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} βΌ π¦)) |
52 | 50, 12, 51 | sylancl 587 |
. . . . . . . 8
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β ((β―β{π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π}) β€ (β―βπ¦) β {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} βΌ π¦)) |
53 | 47, 52 | mpbid 231 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} βΌ π¦) |
54 | | domtr 8950 |
. . . . . . 7
β’ (((π¦ βͺ π₯) βΌ {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} β§ {π§ β (BaseβπΊ) β£ ((odβπΊ)βπ§) β₯ π} βΌ π¦) β (π¦ βͺ π₯) βΌ π¦) |
55 | 43, 53, 54 | syl2anc 585 |
. . . . . 6
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (π¦ βͺ π₯) βΌ π¦) |
56 | 12, 30 | unex 7681 |
. . . . . . 7
β’ (π¦ βͺ π₯) β V |
57 | | ssun1 4133 |
. . . . . . 7
β’ π¦ β (π¦ βͺ π₯) |
58 | | ssdomg 8943 |
. . . . . . 7
β’ ((π¦ βͺ π₯) β V β (π¦ β (π¦ βͺ π₯) β π¦ βΌ (π¦ βͺ π₯))) |
59 | 56, 57, 58 | mp2 9 |
. . . . . 6
β’ π¦ βΌ (π¦ βͺ π₯) |
60 | | sbth 9040 |
. . . . . 6
β’ (((π¦ βͺ π₯) βΌ π¦ β§ π¦ βΌ (π¦ βͺ π₯)) β (π¦ βͺ π₯) β π¦) |
61 | 55, 59, 60 | sylancl 587 |
. . . . 5
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (π¦ βͺ π₯) β π¦) |
62 | 8, 28 | eqtr4d 2776 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β (β―βπ¦) = (β―βπ₯)) |
63 | | hashen 14253 |
. . . . . . . 8
β’ ((π¦ β Fin β§ π₯ β Fin) β
((β―βπ¦) =
(β―βπ₯) β
π¦ β π₯)) |
64 | 15, 33, 63 | syl2anc 585 |
. . . . . . 7
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β ((β―βπ¦) = (β―βπ₯) β π¦ β π₯)) |
65 | 62, 64 | mpbid 231 |
. . . . . 6
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π¦ β π₯) |
66 | | fiuneneq 41567 |
. . . . . 6
β’ ((π¦ β π₯ β§ π¦ β Fin) β ((π¦ βͺ π₯) β π¦ β π¦ = π₯)) |
67 | 65, 15, 66 | syl2anc 585 |
. . . . 5
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β ((π¦ βͺ π₯) β π¦ β π¦ = π₯)) |
68 | 61, 67 | mpbid 231 |
. . . 4
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ)) β§ ((β―βπ¦) = π β§ (β―βπ₯) = π)) β π¦ = π₯) |
69 | 68 | 3expia 1122 |
. . 3
β’ (((π
β IDomn β§ π β β) β§ (π¦ β (SubGrpβπΊ) β§ π₯ β (SubGrpβπΊ))) β (((β―βπ¦) = π β§ (β―βπ₯) = π) β π¦ = π₯)) |
70 | 69 | ralrimivva 3194 |
. 2
β’ ((π
β IDomn β§ π β β) β
βπ¦ β
(SubGrpβπΊ)βπ₯ β (SubGrpβπΊ)(((β―βπ¦) = π β§ (β―βπ₯) = π) β π¦ = π₯)) |
71 | | fveqeq2 6852 |
. . 3
β’ (π¦ = π₯ β ((β―βπ¦) = π β (β―βπ₯) = π)) |
72 | 71 | rmo4 3689 |
. 2
β’
(β*π¦ β
(SubGrpβπΊ)(β―βπ¦) = π β βπ¦ β (SubGrpβπΊ)βπ₯ β (SubGrpβπΊ)(((β―βπ¦) = π β§ (β―βπ₯) = π) β π¦ = π₯)) |
73 | 70, 72 | sylibr 233 |
1
β’ ((π
β IDomn β§ π β β) β
β*π¦ β
(SubGrpβπΊ)(β―βπ¦) = π) |