Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . 7
β’
(mulGrpβπ) =
(mulGrpβπ) |
2 | | cznrng.y |
. . . . . . . 8
β’ π =
(β€/nβ€βπ) |
3 | | cznrng.b |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
4 | | cznrng.x |
. . . . . . . 8
β’ π = (π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©) |
5 | 2, 3, 4 | cznrnglem 46337 |
. . . . . . 7
β’ π΅ = (Baseβπ) |
6 | 1, 5 | mgpbas 19907 |
. . . . . 6
β’ π΅ =
(Baseβ(mulGrpβπ)) |
7 | 4 | fveq2i 6846 |
. . . . . . . 8
β’
(mulGrpβπ) =
(mulGrpβ(π sSet
β¨(.rβndx), (π₯ β π΅, π¦ β π΅ β¦ πΆ)β©)) |
8 | 2 | fvexi 6857 |
. . . . . . . . 9
β’ π β V |
9 | 3 | fvexi 6857 |
. . . . . . . . . 10
β’ π΅ β V |
10 | 9, 9 | mpoex 8013 |
. . . . . . . . 9
β’ (π₯ β π΅, π¦ β π΅ β¦ πΆ) β V |
11 | | mulrid 17180 |
. . . . . . . . . 10
β’
.r = Slot (.rβndx) |
12 | 11 | setsid 17085 |
. . . . . . . . 9
β’ ((π β V β§ (π₯ β π΅, π¦ β π΅ β¦ πΆ) β V) β (π₯ β π΅, π¦ β π΅ β¦ πΆ) = (.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))) |
13 | 8, 10, 12 | mp2an 691 |
. . . . . . . 8
β’ (π₯ β π΅, π¦ β π΅ β¦ πΆ) = (.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©)) |
14 | 7, 13 | mgpplusg 19905 |
. . . . . . 7
β’ (π₯ β π΅, π¦ β π΅ β¦ πΆ) = (+gβ(mulGrpβπ)) |
15 | 14 | eqcomi 2742 |
. . . . . 6
β’
(+gβ(mulGrpβπ)) = (π₯ β π΅, π¦ β π΅ β¦ πΆ) |
16 | | simpr 486 |
. . . . . 6
β’ ((π β
(β€β₯β2) β§ πΆ β π΅) β πΆ β π΅) |
17 | | eluz2 12774 |
. . . . . . . . 9
β’ (π β
(β€β₯β2) β (2 β β€ β§ π β β€ β§ 2 β€
π)) |
18 | | 1lt2 12329 |
. . . . . . . . . 10
β’ 1 <
2 |
19 | | 1red 11161 |
. . . . . . . . . . . . . 14
β’ (π β β€ β 1 β
β) |
20 | | 2re 12232 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β€ β 2 β
β) |
22 | | zre 12508 |
. . . . . . . . . . . . . 14
β’ (π β β€ β π β
β) |
23 | | ltletr 11252 |
. . . . . . . . . . . . . 14
β’ ((1
β β β§ 2 β β β§ π β β) β ((1 < 2 β§ 2
β€ π) β 1 < π)) |
24 | 19, 21, 22, 23 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β β€ β ((1 <
2 β§ 2 β€ π) β 1
< π)) |
25 | 24 | expcomd 418 |
. . . . . . . . . . . 12
β’ (π β β€ β (2 β€
π β (1 < 2 β 1
< π))) |
26 | 25 | a1i 11 |
. . . . . . . . . . 11
β’ (2 β
β€ β (π β
β€ β (2 β€ π
β (1 < 2 β 1 < π)))) |
27 | 26 | 3imp 1112 |
. . . . . . . . . 10
β’ ((2
β β€ β§ π
β β€ β§ 2 β€ π) β (1 < 2 β 1 < π)) |
28 | 18, 27 | mpi 20 |
. . . . . . . . 9
β’ ((2
β β€ β§ π
β β€ β§ 2 β€ π) β 1 < π) |
29 | 17, 28 | sylbi 216 |
. . . . . . . 8
β’ (π β
(β€β₯β2) β 1 < π) |
30 | | eluz2nn 12814 |
. . . . . . . . 9
β’ (π β
(β€β₯β2) β π β β) |
31 | 2, 3 | znhash 20981 |
. . . . . . . . 9
β’ (π β β β
(β―βπ΅) = π) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
β’ (π β
(β€β₯β2) β (β―βπ΅) = π) |
33 | 29, 32 | breqtrrd 5134 |
. . . . . . 7
β’ (π β
(β€β₯β2) β 1 < (β―βπ΅)) |
34 | 33 | adantr 482 |
. . . . . 6
β’ ((π β
(β€β₯β2) β§ πΆ β π΅) β 1 < (β―βπ΅)) |
35 | 6, 15, 16, 34 | copisnmnd 46189 |
. . . . 5
β’ ((π β
(β€β₯β2) β§ πΆ β π΅) β (mulGrpβπ) β Mnd) |
36 | | df-nel 3047 |
. . . . 5
β’
((mulGrpβπ)
β Mnd β Β¬ (mulGrpβπ) β Mnd) |
37 | 35, 36 | sylib 217 |
. . . 4
β’ ((π β
(β€β₯β2) β§ πΆ β π΅) β Β¬ (mulGrpβπ) β Mnd) |
38 | 37 | intn3an2d 1481 |
. . 3
β’ ((π β
(β€β₯β2) β§ πΆ β π΅) β Β¬ (π β Grp β§ (mulGrpβπ) β Mnd β§ βπ β π΅ βπ β π΅ βπ β π΅ ((π(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))(π(+gβπ)π)) = ((π(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))π)(+gβπ)(π(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))π)) β§ ((π(+gβπ)π)(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))π) = ((π(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))π)(+gβπ)(π(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))π))))) |
39 | | eqid 2733 |
. . . 4
β’
(+gβπ) = (+gβπ) |
40 | 4 | eqcomi 2742 |
. . . . 5
β’ (π sSet
β¨(.rβndx), (π₯ β π΅, π¦ β π΅ β¦ πΆ)β©) = π |
41 | 40 | fveq2i 6846 |
. . . 4
β’
(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©)) = (.rβπ) |
42 | 5, 1, 39, 41 | isring 19973 |
. . 3
β’ (π β Ring β (π β Grp β§
(mulGrpβπ) β Mnd
β§ βπ β
π΅ βπ β π΅ βπ β π΅ ((π(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))(π(+gβπ)π)) = ((π(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))π)(+gβπ)(π(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))π)) β§ ((π(+gβπ)π)(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))π) = ((π(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))π)(+gβπ)(π(.rβ(π sSet β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ πΆ)β©))π))))) |
43 | 38, 42 | sylnibr 329 |
. 2
β’ ((π β
(β€β₯β2) β§ πΆ β π΅) β Β¬ π β Ring) |
44 | | df-nel 3047 |
. 2
β’ (π β Ring β Β¬ π β Ring) |
45 | 43, 44 | sylibr 233 |
1
β’ ((π β
(β€β₯β2) β§ πΆ β π΅) β π β Ring) |