Step | Hyp | Ref
| Expression |
1 | | elfvdm 6880 |
. . . 4
β’ (π β (Irredβπ
) β π
β dom Irred) |
2 | | irred.3 |
. . . 4
β’ πΌ = (Irredβπ
) |
3 | 1, 2 | eleq2s 2856 |
. . 3
β’ (π β πΌ β π
β dom Irred) |
4 | 3 | elexd 3466 |
. 2
β’ (π β πΌ β π
β V) |
5 | | eldifi 4087 |
. . . . . 6
β’ (π β (π΅ β π) β π β π΅) |
6 | | irred.4 |
. . . . . 6
β’ π = (π΅ β π) |
7 | 5, 6 | eleq2s 2856 |
. . . . 5
β’ (π β π β π β π΅) |
8 | | irred.1 |
. . . . 5
β’ π΅ = (Baseβπ
) |
9 | 7, 8 | eleqtrdi 2848 |
. . . 4
β’ (π β π β π β (Baseβπ
)) |
10 | 9 | elfvexd 6882 |
. . 3
β’ (π β π β π
β V) |
11 | 10 | adantr 482 |
. 2
β’ ((π β π β§ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π) β π
β V) |
12 | | fvex 6856 |
. . . . . . . 8
β’
(Baseβπ)
β V |
13 | | difexg 5285 |
. . . . . . . 8
β’
((Baseβπ)
β V β ((Baseβπ) β (Unitβπ)) β V) |
14 | 12, 13 | mp1i 13 |
. . . . . . 7
β’ (π = π
β ((Baseβπ) β (Unitβπ)) β V) |
15 | | simpr 486 |
. . . . . . . . 9
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β π = ((Baseβπ) β (Unitβπ))) |
16 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β π = π
) |
17 | 16 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β (Baseβπ) = (Baseβπ
)) |
18 | 17, 8 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β (Baseβπ) = π΅) |
19 | 16 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β (Unitβπ) = (Unitβπ
)) |
20 | | irred.2 |
. . . . . . . . . . . 12
β’ π = (Unitβπ
) |
21 | 19, 20 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β (Unitβπ) = π) |
22 | 18, 21 | difeq12d 4084 |
. . . . . . . . . 10
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β ((Baseβπ) β (Unitβπ)) = (π΅ β π)) |
23 | 22, 6 | eqtr4di 2795 |
. . . . . . . . 9
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β ((Baseβπ) β (Unitβπ)) = π) |
24 | 15, 23 | eqtrd 2777 |
. . . . . . . 8
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β π = π) |
25 | 16 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β (.rβπ) = (.rβπ
)) |
26 | | irred.5 |
. . . . . . . . . . . . 13
β’ Β· =
(.rβπ
) |
27 | 25, 26 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β (.rβπ) = Β· ) |
28 | 27 | oveqd 7375 |
. . . . . . . . . . 11
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β (π₯(.rβπ)π¦) = (π₯ Β· π¦)) |
29 | 28 | neeq1d 3004 |
. . . . . . . . . 10
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β ((π₯(.rβπ)π¦) β π§ β (π₯ Β· π¦) β π§)) |
30 | 24, 29 | raleqbidv 3320 |
. . . . . . . . 9
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β (βπ¦ β π (π₯(.rβπ)π¦) β π§ β βπ¦ β π (π₯ Β· π¦) β π§)) |
31 | 24, 30 | raleqbidv 3320 |
. . . . . . . 8
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β (βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π§ β βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π§)) |
32 | 24, 31 | rabeqbidv 3425 |
. . . . . . 7
β’ ((π = π
β§ π = ((Baseβπ) β (Unitβπ))) β {π§ β π β£ βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π§} = {π§ β π β£ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π§}) |
33 | 14, 32 | csbied 3894 |
. . . . . 6
β’ (π = π
β β¦((Baseβπ) β (Unitβπ)) / πβ¦{π§ β π β£ βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π§} = {π§ β π β£ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π§}) |
34 | | df-irred 20073 |
. . . . . 6
β’ Irred =
(π β V β¦
β¦((Baseβπ) β (Unitβπ)) / πβ¦{π§ β π β£ βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π§}) |
35 | | fvex 6856 |
. . . . . . . . . 10
β’
(Baseβπ
)
β V |
36 | 8, 35 | eqeltri 2834 |
. . . . . . . . 9
β’ π΅ β V |
37 | 36 | difexi 5286 |
. . . . . . . 8
β’ (π΅ β π) β V |
38 | 6, 37 | eqeltri 2834 |
. . . . . . 7
β’ π β V |
39 | 38 | rabex 5290 |
. . . . . 6
β’ {π§ β π β£ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π§} β V |
40 | 33, 34, 39 | fvmpt 6949 |
. . . . 5
β’ (π
β V β
(Irredβπ
) = {π§ β π β£ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π§}) |
41 | 2, 40 | eqtrid 2789 |
. . . 4
β’ (π
β V β πΌ = {π§ β π β£ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π§}) |
42 | 41 | eleq2d 2824 |
. . 3
β’ (π
β V β (π β πΌ β π β {π§ β π β£ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π§})) |
43 | | neeq2 3008 |
. . . . 5
β’ (π§ = π β ((π₯ Β· π¦) β π§ β (π₯ Β· π¦) β π)) |
44 | 43 | 2ralbidv 3213 |
. . . 4
β’ (π§ = π β (βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π§ β βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π)) |
45 | 44 | elrab 3646 |
. . 3
β’ (π β {π§ β π β£ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π§} β (π β π β§ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π)) |
46 | 42, 45 | bitrdi 287 |
. 2
β’ (π
β V β (π β πΌ β (π β π β§ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π))) |
47 | 4, 11, 46 | pm5.21nii 380 |
1
β’ (π β πΌ β (π β π β§ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π)) |