Step | Hyp | Ref
| Expression |
1 | | isdrngd.r |
. . 3
โข (๐ โ ๐
โ Ring) |
2 | | difss 4095 |
. . . . . 6
โข (๐ต โ { 0 }) โ ๐ต |
3 | | isdrngd.b |
. . . . . 6
โข (๐ โ ๐ต = (Baseโ๐
)) |
4 | 2, 3 | sseqtrid 4000 |
. . . . 5
โข (๐ โ (๐ต โ { 0 }) โ
(Baseโ๐
)) |
5 | | eqid 2733 |
. . . . . 6
โข
((mulGrpโ๐
)
โพs (๐ต
โ { 0 })) = ((mulGrpโ๐
) โพs (๐ต โ { 0 })) |
6 | | eqid 2733 |
. . . . . . 7
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
7 | | eqid 2733 |
. . . . . . 7
โข
(Baseโ๐
) =
(Baseโ๐
) |
8 | 6, 7 | mgpbas 19910 |
. . . . . 6
โข
(Baseโ๐
) =
(Baseโ(mulGrpโ๐
)) |
9 | 5, 8 | ressbas2 17128 |
. . . . 5
โข ((๐ต โ { 0 }) โ
(Baseโ๐
) โ
(๐ต โ { 0 }) =
(Baseโ((mulGrpโ๐
) โพs (๐ต โ { 0 })))) |
10 | 4, 9 | syl 17 |
. . . 4
โข (๐ โ (๐ต โ { 0 }) =
(Baseโ((mulGrpโ๐
) โพs (๐ต โ { 0 })))) |
11 | | isdrngd.t |
. . . . 5
โข (๐ โ ยท =
(.rโ๐
)) |
12 | | fvex 6859 |
. . . . . . 7
โข
(Baseโ๐
)
โ V |
13 | 3, 12 | eqeltrdi 2842 |
. . . . . 6
โข (๐ โ ๐ต โ V) |
14 | | difexg 5288 |
. . . . . 6
โข (๐ต โ V โ (๐ต โ { 0 }) โ
V) |
15 | | eqid 2733 |
. . . . . . . 8
โข
(.rโ๐
) = (.rโ๐
) |
16 | 6, 15 | mgpplusg 19908 |
. . . . . . 7
โข
(.rโ๐
) = (+gโ(mulGrpโ๐
)) |
17 | 5, 16 | ressplusg 17179 |
. . . . . 6
โข ((๐ต โ { 0 }) โ V โ
(.rโ๐
) =
(+gโ((mulGrpโ๐
) โพs (๐ต โ { 0 })))) |
18 | 13, 14, 17 | 3syl 18 |
. . . . 5
โข (๐ โ (.rโ๐
) =
(+gโ((mulGrpโ๐
) โพs (๐ต โ { 0 })))) |
19 | 11, 18 | eqtrd 2773 |
. . . 4
โข (๐ โ ยท =
(+gโ((mulGrpโ๐
) โพs (๐ต โ { 0 })))) |
20 | | eldifsn 4751 |
. . . . 5
โข (๐ฅ โ (๐ต โ { 0 }) โ (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) |
21 | | eldifsn 4751 |
. . . . . 6
โข (๐ฆ โ (๐ต โ { 0 }) โ (๐ฆ โ ๐ต โง ๐ฆ โ 0 )) |
22 | 7, 15 | ringcl 19989 |
. . . . . . . . . . . . 13
โข ((๐
โ Ring โง ๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ (๐ฅ(.rโ๐
)๐ฆ) โ (Baseโ๐
)) |
23 | 1, 22 | syl3an1 1164 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ (๐ฅ(.rโ๐
)๐ฆ) โ (Baseโ๐
)) |
24 | 23 | 3expib 1123 |
. . . . . . . . . . 11
โข (๐ โ ((๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)) โ (๐ฅ(.rโ๐
)๐ฆ) โ (Baseโ๐
))) |
25 | 3 | eleq2d 2820 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ โ ๐ต โ ๐ฅ โ (Baseโ๐
))) |
26 | 3 | eleq2d 2820 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฆ โ ๐ต โ ๐ฆ โ (Baseโ๐
))) |
27 | 25, 26 | anbi12d 632 |
. . . . . . . . . . 11
โข (๐ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)))) |
28 | 11 | oveqd 7378 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ ยท ๐ฆ) = (๐ฅ(.rโ๐
)๐ฆ)) |
29 | 28, 3 | eleq12d 2828 |
. . . . . . . . . . 11
โข (๐ โ ((๐ฅ ยท ๐ฆ) โ ๐ต โ (๐ฅ(.rโ๐
)๐ฆ) โ (Baseโ๐
))) |
30 | 24, 27, 29 | 3imtr4d 294 |
. . . . . . . . . 10
โข (๐ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ ยท ๐ฆ) โ ๐ต)) |
31 | 30 | 3impib 1117 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ ยท ๐ฆ) โ ๐ต) |
32 | 31 | 3adant2r 1180 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 ) โง ๐ฆ โ ๐ต) โ (๐ฅ ยท ๐ฆ) โ ๐ต) |
33 | 32 | 3adant3r 1182 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 ) โง (๐ฆ โ ๐ต โง ๐ฆ โ 0 )) โ (๐ฅ ยท ๐ฆ) โ ๐ต) |
34 | | isdrngd.n |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 ) โง (๐ฆ โ ๐ต โง ๐ฆ โ 0 )) โ (๐ฅ ยท ๐ฆ) โ 0 ) |
35 | | eldifsn 4751 |
. . . . . . 7
โข ((๐ฅ ยท ๐ฆ) โ (๐ต โ { 0 }) โ ((๐ฅ ยท ๐ฆ) โ ๐ต โง (๐ฅ ยท ๐ฆ) โ 0 )) |
36 | 33, 34, 35 | sylanbrc 584 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 ) โง (๐ฆ โ ๐ต โง ๐ฆ โ 0 )) โ (๐ฅ ยท ๐ฆ) โ (๐ต โ { 0 })) |
37 | 21, 36 | syl3an3b 1406 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 ) โง ๐ฆ โ (๐ต โ { 0 })) โ (๐ฅ ยท ๐ฆ) โ (๐ต โ { 0 })) |
38 | 20, 37 | syl3an2b 1405 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ต โ { 0 }) โง ๐ฆ โ (๐ต โ { 0 })) โ (๐ฅ ยท ๐ฆ) โ (๐ต โ { 0 })) |
39 | 7, 15 | ringass 19992 |
. . . . . . . 8
โข ((๐
โ Ring โง (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
) โง ๐ง โ (Baseโ๐
))) โ ((๐ฅ(.rโ๐
)๐ฆ)(.rโ๐
)๐ง) = (๐ฅ(.rโ๐
)(๐ฆ(.rโ๐
)๐ง))) |
40 | 39 | ex 414 |
. . . . . . 7
โข (๐
โ Ring โ ((๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
) โง ๐ง โ (Baseโ๐
)) โ ((๐ฅ(.rโ๐
)๐ฆ)(.rโ๐
)๐ง) = (๐ฅ(.rโ๐
)(๐ฆ(.rโ๐
)๐ง)))) |
41 | 1, 40 | syl 17 |
. . . . . 6
โข (๐ โ ((๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
) โง ๐ง โ (Baseโ๐
)) โ ((๐ฅ(.rโ๐
)๐ฆ)(.rโ๐
)๐ง) = (๐ฅ(.rโ๐
)(๐ฆ(.rโ๐
)๐ง)))) |
42 | 3 | eleq2d 2820 |
. . . . . . 7
โข (๐ โ (๐ง โ ๐ต โ ๐ง โ (Baseโ๐
))) |
43 | 25, 26, 42 | 3anbi123d 1437 |
. . . . . 6
โข (๐ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต) โ (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
) โง ๐ง โ (Baseโ๐
)))) |
44 | | eqidd 2734 |
. . . . . . . 8
โข (๐ โ ๐ง = ๐ง) |
45 | 11, 28, 44 | oveq123d 7382 |
. . . . . . 7
โข (๐ โ ((๐ฅ ยท ๐ฆ) ยท ๐ง) = ((๐ฅ(.rโ๐
)๐ฆ)(.rโ๐
)๐ง)) |
46 | | eqidd 2734 |
. . . . . . . 8
โข (๐ โ ๐ฅ = ๐ฅ) |
47 | 11 | oveqd 7378 |
. . . . . . . 8
โข (๐ โ (๐ฆ ยท ๐ง) = (๐ฆ(.rโ๐
)๐ง)) |
48 | 11, 46, 47 | oveq123d 7382 |
. . . . . . 7
โข (๐ โ (๐ฅ ยท (๐ฆ ยท ๐ง)) = (๐ฅ(.rโ๐
)(๐ฆ(.rโ๐
)๐ง))) |
49 | 45, 48 | eqeq12d 2749 |
. . . . . 6
โข (๐ โ (((๐ฅ ยท ๐ฆ) ยท ๐ง) = (๐ฅ ยท (๐ฆ ยท ๐ง)) โ ((๐ฅ(.rโ๐
)๐ฆ)(.rโ๐
)๐ง) = (๐ฅ(.rโ๐
)(๐ฆ(.rโ๐
)๐ง)))) |
50 | 41, 43, 49 | 3imtr4d 294 |
. . . . 5
โข (๐ โ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต) โ ((๐ฅ ยท ๐ฆ) ยท ๐ง) = (๐ฅ ยท (๐ฆ ยท ๐ง)))) |
51 | | eldifi 4090 |
. . . . . 6
โข (๐ฅ โ (๐ต โ { 0 }) โ ๐ฅ โ ๐ต) |
52 | | eldifi 4090 |
. . . . . 6
โข (๐ฆ โ (๐ต โ { 0 }) โ ๐ฆ โ ๐ต) |
53 | | eldifi 4090 |
. . . . . 6
โข (๐ง โ (๐ต โ { 0 }) โ ๐ง โ ๐ต) |
54 | 51, 52, 53 | 3anim123i 1152 |
. . . . 5
โข ((๐ฅ โ (๐ต โ { 0 }) โง ๐ฆ โ (๐ต โ { 0 }) โง ๐ง โ (๐ต โ { 0 })) โ (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) |
55 | 50, 54 | impel 507 |
. . . 4
โข ((๐ โง (๐ฅ โ (๐ต โ { 0 }) โง ๐ฆ โ (๐ต โ { 0 }) โง ๐ง โ (๐ต โ { 0 }))) โ ((๐ฅ ยท ๐ฆ) ยท ๐ง) = (๐ฅ ยท (๐ฆ ยท ๐ง))) |
56 | | eqid 2733 |
. . . . . . . 8
โข
(1rโ๐
) = (1rโ๐
) |
57 | 7, 56 | ringidcl 19997 |
. . . . . . 7
โข (๐
โ Ring โ
(1rโ๐
)
โ (Baseโ๐
)) |
58 | 1, 57 | syl 17 |
. . . . . 6
โข (๐ โ (1rโ๐
) โ (Baseโ๐
)) |
59 | | isdrngd.u |
. . . . . 6
โข (๐ โ 1 =
(1rโ๐
)) |
60 | 58, 59, 3 | 3eltr4d 2849 |
. . . . 5
โข (๐ โ 1 โ ๐ต) |
61 | | isdrngd.o |
. . . . 5
โข (๐ โ 1 โ 0 ) |
62 | | eldifsn 4751 |
. . . . 5
โข ( 1 โ (๐ต โ { 0 }) โ ( 1 โ ๐ต โง 1 โ 0 )) |
63 | 60, 61, 62 | sylanbrc 584 |
. . . 4
โข (๐ โ 1 โ (๐ต โ { 0 })) |
64 | 7, 15, 56 | ringlidm 20000 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ฅ โ (Baseโ๐
)) โ
((1rโ๐
)(.rโ๐
)๐ฅ) = ๐ฅ) |
65 | 64 | ex 414 |
. . . . . . . . 9
โข (๐
โ Ring โ (๐ฅ โ (Baseโ๐
) โ
((1rโ๐
)(.rโ๐
)๐ฅ) = ๐ฅ)) |
66 | 1, 65 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ (Baseโ๐
) โ ((1rโ๐
)(.rโ๐
)๐ฅ) = ๐ฅ)) |
67 | 11, 59, 46 | oveq123d 7382 |
. . . . . . . . 9
โข (๐ โ ( 1 ยท ๐ฅ) = ((1rโ๐
)(.rโ๐
)๐ฅ)) |
68 | 67 | eqeq1d 2735 |
. . . . . . . 8
โข (๐ โ (( 1 ยท ๐ฅ) = ๐ฅ โ ((1rโ๐
)(.rโ๐
)๐ฅ) = ๐ฅ)) |
69 | 66, 25, 68 | 3imtr4d 294 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ต โ ( 1 ยท ๐ฅ) = ๐ฅ)) |
70 | 69 | imp 408 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ต) โ ( 1 ยท ๐ฅ) = ๐ฅ) |
71 | 70 | adantrr 716 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ ( 1 ยท ๐ฅ) = ๐ฅ) |
72 | 20, 71 | sylan2b 595 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ต โ { 0 })) โ ( 1 ยท ๐ฅ) = ๐ฅ) |
73 | | isdrngd.i |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ ๐ผ โ ๐ต) |
74 | 61 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ 1 โ 0
) |
75 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โง ๐ผ = 0 ) โ ๐ผ = 0 ) |
76 | 75 | oveq1d 7376 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โง ๐ผ = 0 ) โ (๐ผ ยท ๐ฅ) = ( 0 ยท ๐ฅ)) |
77 | | isdrngd.k |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ (๐ผ ยท ๐ฅ) = 1 ) |
78 | 77 | adantr 482 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โง ๐ผ = 0 ) โ (๐ผ ยท ๐ฅ) = 1 ) |
79 | 25 | biimpa 478 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ฅ โ (Baseโ๐
)) |
80 | 79 | adantrr 716 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ ๐ฅ โ (Baseโ๐
)) |
81 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(0gโ๐
) = (0gโ๐
) |
82 | 7, 15, 81 | ringlz 20019 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง ๐ฅ โ (Baseโ๐
)) โ
((0gโ๐
)(.rโ๐
)๐ฅ) = (0gโ๐
)) |
83 | 1, 80, 82 | syl2an2r 684 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ
((0gโ๐
)(.rโ๐
)๐ฅ) = (0gโ๐
)) |
84 | | isdrngd.z |
. . . . . . . . . . . 12
โข (๐ โ 0 =
(0gโ๐
)) |
85 | 11, 84, 46 | oveq123d 7382 |
. . . . . . . . . . 11
โข (๐ โ ( 0 ยท ๐ฅ) = ((0gโ๐
)(.rโ๐
)๐ฅ)) |
86 | 85 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ ( 0 ยท ๐ฅ) = ((0gโ๐
)(.rโ๐
)๐ฅ)) |
87 | 84 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ 0 =
(0gโ๐
)) |
88 | 83, 86, 87 | 3eqtr4d 2783 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ ( 0 ยท ๐ฅ) = 0 ) |
89 | 88 | adantr 482 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โง ๐ผ = 0 ) โ ( 0 ยท ๐ฅ) = 0 ) |
90 | 76, 78, 89 | 3eqtr3d 2781 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โง ๐ผ = 0 ) โ 1 = 0
) |
91 | 74, 90 | mteqand 3045 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ ๐ผ โ 0 ) |
92 | | eldifsn 4751 |
. . . . . 6
โข (๐ผ โ (๐ต โ { 0 }) โ (๐ผ โ ๐ต โง ๐ผ โ 0 )) |
93 | 73, 91, 92 | sylanbrc 584 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฅ โ 0 )) โ ๐ผ โ (๐ต โ { 0 })) |
94 | 20, 93 | sylan2b 595 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ต โ { 0 })) โ ๐ผ โ (๐ต โ { 0 })) |
95 | 20, 77 | sylan2b 595 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ต โ { 0 })) โ (๐ผ ยท ๐ฅ) = 1 ) |
96 | 10, 19, 38, 55, 63, 72, 94, 95 | isgrpd 18780 |
. . 3
โข (๐ โ ((mulGrpโ๐
) โพs (๐ต โ { 0 })) โ
Grp) |
97 | 84 | sneqd 4602 |
. . . . . . 7
โข (๐ โ { 0 } =
{(0gโ๐
)}) |
98 | 3, 97 | difeq12d 4087 |
. . . . . 6
โข (๐ โ (๐ต โ { 0 }) = ((Baseโ๐
) โ
{(0gโ๐
)})) |
99 | 98 | oveq2d 7377 |
. . . . 5
โข (๐ โ ((mulGrpโ๐
) โพs (๐ต โ { 0 })) = ((mulGrpโ๐
) โพs
((Baseโ๐
) โ
{(0gโ๐
)}))) |
100 | 99 | eleq1d 2819 |
. . . 4
โข (๐ โ (((mulGrpโ๐
) โพs (๐ต โ { 0 })) โ Grp โ
((mulGrpโ๐
)
โพs ((Baseโ๐
) โ {(0gโ๐
)})) โ
Grp)) |
101 | 100 | anbi2d 630 |
. . 3
โข (๐ โ ((๐
โ Ring โง ((mulGrpโ๐
) โพs (๐ต โ { 0 })) โ Grp) โ
(๐
โ Ring โง
((mulGrpโ๐
)
โพs ((Baseโ๐
) โ {(0gโ๐
)})) โ
Grp))) |
102 | 1, 96, 101 | mpbi2and 711 |
. 2
โข (๐ โ (๐
โ Ring โง ((mulGrpโ๐
) โพs
((Baseโ๐
) โ
{(0gโ๐
)}))
โ Grp)) |
103 | | eqid 2733 |
. . 3
โข
((mulGrpโ๐
)
โพs ((Baseโ๐
) โ {(0gโ๐
)})) = ((mulGrpโ๐
) โพs
((Baseโ๐
) โ
{(0gโ๐
)})) |
104 | 7, 81, 103 | isdrng2 20232 |
. 2
โข (๐
โ DivRing โ (๐
โ Ring โง
((mulGrpโ๐
)
โพs ((Baseโ๐
) โ {(0gโ๐
)})) โ
Grp)) |
105 | 102, 104 | sylibr 233 |
1
โข (๐ โ ๐
โ DivRing) |