Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . 8
β’
(invrβπ
) = (invrβπ
) |
2 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
3 | 1, 2 | issdrg2 20307 |
. . . . . . 7
β’ (π β (SubDRingβπ
) β (π
β DivRing β§ π β (SubRingβπ
) β§ βπ₯ β (π β {(0gβπ
)})((invrβπ
)βπ₯) β π )) |
4 | | 3anass 1096 |
. . . . . . 7
β’ ((π
β DivRing β§ π β (SubRingβπ
) β§ βπ₯ β (π β {(0gβπ
)})((invrβπ
)βπ₯) β π ) β (π
β DivRing β§ (π β (SubRingβπ
) β§ βπ₯ β (π β {(0gβπ
)})((invrβπ
)βπ₯) β π ))) |
5 | 3, 4 | bitri 275 |
. . . . . 6
β’ (π β (SubDRingβπ
) β (π
β DivRing β§ (π β (SubRingβπ
) β§ βπ₯ β (π β {(0gβπ
)})((invrβπ
)βπ₯) β π ))) |
6 | 5 | baib 537 |
. . . . 5
β’ (π
β DivRing β (π β (SubDRingβπ
) β (π β (SubRingβπ
) β§ βπ₯ β (π β {(0gβπ
)})((invrβπ
)βπ₯) β π ))) |
7 | | subrgacs.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ
) |
8 | 7 | subrgss 20265 |
. . . . . . . . 9
β’ (π β (SubRingβπ
) β π β π΅) |
9 | | velpw 4569 |
. . . . . . . . 9
β’ (π β π« π΅ β π β π΅) |
10 | 8, 9 | sylibr 233 |
. . . . . . . 8
β’ (π β (SubRingβπ
) β π β π« π΅) |
11 | 10 | adantl 483 |
. . . . . . 7
β’ ((π
β DivRing β§ π β (SubRingβπ
)) β π β π« π΅) |
12 | | iftrue 4496 |
. . . . . . . . . . . . . 14
β’ (π₯ = (0gβπ
) β if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) = π₯) |
13 | 12 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (π₯ = (0gβπ
) β (if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦ β π₯ β π¦)) |
14 | 13 | biimprd 248 |
. . . . . . . . . . . 12
β’ (π₯ = (0gβπ
) β (π₯ β π¦ β if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦)) |
15 | | eldifsni 4754 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π¦ β {(0gβπ
)}) β π₯ β (0gβπ
)) |
16 | 15 | necon2bi 2971 |
. . . . . . . . . . . . 13
β’ (π₯ = (0gβπ
) β Β¬ π₯ β (π¦ β {(0gβπ
)})) |
17 | 16 | pm2.21d 121 |
. . . . . . . . . . . 12
β’ (π₯ = (0gβπ
) β (π₯ β (π¦ β {(0gβπ
)}) β
((invrβπ
)βπ₯) β π¦)) |
18 | 14, 17 | 2thd 265 |
. . . . . . . . . . 11
β’ (π₯ = (0gβπ
) β ((π₯ β π¦ β if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦) β (π₯ β (π¦ β {(0gβπ
)}) β
((invrβπ
)βπ₯) β π¦))) |
19 | | eldifsn 4751 |
. . . . . . . . . . . . 13
β’ (π₯ β (π¦ β {(0gβπ
)}) β (π₯ β π¦ β§ π₯ β (0gβπ
))) |
20 | 19 | rbaibr 539 |
. . . . . . . . . . . 12
β’ (π₯ β (0gβπ
) β (π₯ β π¦ β π₯ β (π¦ β {(0gβπ
)}))) |
21 | | ifnefalse 4502 |
. . . . . . . . . . . . 13
β’ (π₯ β (0gβπ
) β if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) = ((invrβπ
)βπ₯)) |
22 | 21 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π₯ β (0gβπ
) β (if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦ β ((invrβπ
)βπ₯) β π¦)) |
23 | 20, 22 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π₯ β (0gβπ
) β ((π₯ β π¦ β if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦) β (π₯ β (π¦ β {(0gβπ
)}) β
((invrβπ
)βπ₯) β π¦))) |
24 | 18, 23 | pm2.61ine 3025 |
. . . . . . . . . 10
β’ ((π₯ β π¦ β if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦) β (π₯ β (π¦ β {(0gβπ
)}) β
((invrβπ
)βπ₯) β π¦)) |
25 | 24 | ralbii2 3089 |
. . . . . . . . 9
β’
(βπ₯ β
π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦ β βπ₯ β (π¦ β {(0gβπ
)})((invrβπ
)βπ₯) β π¦) |
26 | | difeq1 4079 |
. . . . . . . . . 10
β’ (π¦ = π β (π¦ β {(0gβπ
)}) = (π β {(0gβπ
)})) |
27 | | eleq2w 2818 |
. . . . . . . . . 10
β’ (π¦ = π β (((invrβπ
)βπ₯) β π¦ β ((invrβπ
)βπ₯) β π )) |
28 | 26, 27 | raleqbidv 3318 |
. . . . . . . . 9
β’ (π¦ = π β (βπ₯ β (π¦ β {(0gβπ
)})((invrβπ
)βπ₯) β π¦ β βπ₯ β (π β {(0gβπ
)})((invrβπ
)βπ₯) β π )) |
29 | 25, 28 | bitrid 283 |
. . . . . . . 8
β’ (π¦ = π β (βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦ β βπ₯ β (π β {(0gβπ
)})((invrβπ
)βπ₯) β π )) |
30 | 29 | elrab3 3650 |
. . . . . . 7
β’ (π β π« π΅ β (π β {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦} β βπ₯ β (π β {(0gβπ
)})((invrβπ
)βπ₯) β π )) |
31 | 11, 30 | syl 17 |
. . . . . 6
β’ ((π
β DivRing β§ π β (SubRingβπ
)) β (π β {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦} β βπ₯ β (π β {(0gβπ
)})((invrβπ
)βπ₯) β π )) |
32 | 31 | pm5.32da 580 |
. . . . 5
β’ (π
β DivRing β ((π β (SubRingβπ
) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦}) β (π β (SubRingβπ
) β§ βπ₯ β (π β {(0gβπ
)})((invrβπ
)βπ₯) β π ))) |
33 | 6, 32 | bitr4d 282 |
. . . 4
β’ (π
β DivRing β (π β (SubDRingβπ
) β (π β (SubRingβπ
) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦}))) |
34 | | elin 3930 |
. . . 4
β’ (π β ((SubRingβπ
) β© {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦}) β (π β (SubRingβπ
) β§ π β {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦})) |
35 | 33, 34 | bitr4di 289 |
. . 3
β’ (π
β DivRing β (π β (SubDRingβπ
) β π β ((SubRingβπ
) β© {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦}))) |
36 | 35 | eqrdv 2731 |
. 2
β’ (π
β DivRing β
(SubDRingβπ
) =
((SubRingβπ
) β©
{π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦})) |
37 | 7 | fvexi 6860 |
. . . 4
β’ π΅ β V |
38 | | mreacs 17546 |
. . . 4
β’ (π΅ β V β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
39 | 37, 38 | mp1i 13 |
. . 3
β’ (π
β DivRing β
(ACSβπ΅) β
(Mooreβπ« π΅)) |
40 | | drngring 20226 |
. . . 4
β’ (π
β DivRing β π
β Ring) |
41 | 7 | subrgacs 20310 |
. . . 4
β’ (π
β Ring β
(SubRingβπ
) β
(ACSβπ΅)) |
42 | 40, 41 | syl 17 |
. . 3
β’ (π
β DivRing β
(SubRingβπ
) β
(ACSβπ΅)) |
43 | | simplr 768 |
. . . . . 6
β’ (((π
β DivRing β§ π₯ β π΅) β§ π₯ = (0gβπ
)) β π₯ β π΅) |
44 | | df-ne 2941 |
. . . . . . 7
β’ (π₯ β (0gβπ
) β Β¬ π₯ = (0gβπ
)) |
45 | 7, 2, 1 | drnginvrcl 20240 |
. . . . . . . 8
β’ ((π
β DivRing β§ π₯ β π΅ β§ π₯ β (0gβπ
)) β ((invrβπ
)βπ₯) β π΅) |
46 | 45 | 3expa 1119 |
. . . . . . 7
β’ (((π
β DivRing β§ π₯ β π΅) β§ π₯ β (0gβπ
)) β ((invrβπ
)βπ₯) β π΅) |
47 | 44, 46 | sylan2br 596 |
. . . . . 6
β’ (((π
β DivRing β§ π₯ β π΅) β§ Β¬ π₯ = (0gβπ
)) β ((invrβπ
)βπ₯) β π΅) |
48 | 43, 47 | ifclda 4525 |
. . . . 5
β’ ((π
β DivRing β§ π₯ β π΅) β if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π΅) |
49 | 48 | ralrimiva 3140 |
. . . 4
β’ (π
β DivRing β
βπ₯ β π΅ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π΅) |
50 | | acsfn1 17549 |
. . . 4
β’ ((π΅ β V β§ βπ₯ β π΅ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π΅) β {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦} β (ACSβπ΅)) |
51 | 37, 49, 50 | sylancr 588 |
. . 3
β’ (π
β DivRing β {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦} β (ACSβπ΅)) |
52 | | mreincl 17487 |
. . 3
β’
(((ACSβπ΅)
β (Mooreβπ« π΅) β§ (SubRingβπ
) β (ACSβπ΅) β§ {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦} β (ACSβπ΅)) β ((SubRingβπ
) β© {π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦}) β (ACSβπ΅)) |
53 | 39, 42, 51, 52 | syl3anc 1372 |
. 2
β’ (π
β DivRing β
((SubRingβπ
) β©
{π¦ β π« π΅ β£ βπ₯ β π¦ if(π₯ = (0gβπ
), π₯, ((invrβπ
)βπ₯)) β π¦}) β (ACSβπ΅)) |
54 | 36, 53 | eqeltrd 2834 |
1
β’ (π
β DivRing β
(SubDRingβπ
) β
(ACSβπ΅)) |