Step | Hyp | Ref
| Expression |
1 | | cntzsubrng.m |
. . . . . 6
โข ๐ = (mulGrpโ๐
) |
2 | | cntzsubrng.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
3 | 1, 2 | mgpbas 20045 |
. . . . 5
โข ๐ต = (Baseโ๐) |
4 | | cntzsubrng.z |
. . . . 5
โข ๐ = (Cntzโ๐) |
5 | 3, 4 | cntzssv 19244 |
. . . 4
โข (๐โ๐) โ ๐ต |
6 | 5 | a1i 11 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (๐โ๐) โ ๐ต) |
7 | | simpll 764 |
. . . . . . . 8
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ง โ ๐) โ ๐
โ Rng) |
8 | | ssel2 3972 |
. . . . . . . . 9
โข ((๐ โ ๐ต โง ๐ง โ ๐) โ ๐ง โ ๐ต) |
9 | 8 | adantll 711 |
. . . . . . . 8
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ง โ ๐) โ ๐ง โ ๐ต) |
10 | | eqid 2726 |
. . . . . . . . 9
โข
(.rโ๐
) = (.rโ๐
) |
11 | | eqid 2726 |
. . . . . . . . 9
โข
(0gโ๐
) = (0gโ๐
) |
12 | 2, 10, 11 | rnglz 20070 |
. . . . . . . 8
โข ((๐
โ Rng โง ๐ง โ ๐ต) โ ((0gโ๐
)(.rโ๐
)๐ง) = (0gโ๐
)) |
13 | 7, 9, 12 | syl2anc 583 |
. . . . . . 7
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ง โ ๐) โ ((0gโ๐
)(.rโ๐
)๐ง) = (0gโ๐
)) |
14 | 2, 10, 11 | rngrz 20071 |
. . . . . . . 8
โข ((๐
โ Rng โง ๐ง โ ๐ต) โ (๐ง(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
15 | 7, 9, 14 | syl2anc 583 |
. . . . . . 7
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ง โ ๐) โ (๐ง(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
16 | 13, 15 | eqtr4d 2769 |
. . . . . 6
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ง โ ๐) โ ((0gโ๐
)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)(0gโ๐
))) |
17 | 16 | ralrimiva 3140 |
. . . . 5
โข ((๐
โ Rng โง ๐ โ ๐ต) โ โ๐ง โ ๐ ((0gโ๐
)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)(0gโ๐
))) |
18 | | simpr 484 |
. . . . . 6
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
19 | 2, 11 | rng0cl 20068 |
. . . . . . 7
โข (๐
โ Rng โ
(0gโ๐
)
โ ๐ต) |
20 | 19 | adantr 480 |
. . . . . 6
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (0gโ๐
) โ ๐ต) |
21 | 1, 10 | mgpplusg 20043 |
. . . . . . 7
โข
(.rโ๐
) = (+gโ๐) |
22 | 3, 21, 4 | cntzel 19239 |
. . . . . 6
โข ((๐ โ ๐ต โง (0gโ๐
) โ ๐ต) โ ((0gโ๐
) โ (๐โ๐) โ โ๐ง โ ๐ ((0gโ๐
)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)(0gโ๐
)))) |
23 | 18, 20, 22 | syl2anc 583 |
. . . . 5
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ((0gโ๐
) โ (๐โ๐) โ โ๐ง โ ๐ ((0gโ๐
)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)(0gโ๐
)))) |
24 | 17, 23 | mpbird 257 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (0gโ๐
) โ (๐โ๐)) |
25 | 24 | ne0d 4330 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (๐โ๐) โ โ
) |
26 | | simpl2 1189 |
. . . . . . . . . . . 12
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ ๐ฅ โ (๐โ๐)) |
27 | 21, 4 | cntzi 19245 |
. . . . . . . . . . . 12
โข ((๐ฅ โ (๐โ๐) โง ๐ง โ ๐) โ (๐ฅ(.rโ๐
)๐ง) = (๐ง(.rโ๐
)๐ฅ)) |
28 | 26, 27 | sylancom 587 |
. . . . . . . . . . 11
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ (๐ฅ(.rโ๐
)๐ง) = (๐ง(.rโ๐
)๐ฅ)) |
29 | | simpl3 1190 |
. . . . . . . . . . . 12
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ ๐ฆ โ (๐โ๐)) |
30 | 21, 4 | cntzi 19245 |
. . . . . . . . . . . 12
โข ((๐ฆ โ (๐โ๐) โง ๐ง โ ๐) โ (๐ฆ(.rโ๐
)๐ง) = (๐ง(.rโ๐
)๐ฆ)) |
31 | 29, 30 | sylancom 587 |
. . . . . . . . . . 11
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ (๐ฆ(.rโ๐
)๐ง) = (๐ง(.rโ๐
)๐ฆ)) |
32 | 28, 31 | oveq12d 7423 |
. . . . . . . . . 10
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ ((๐ฅ(.rโ๐
)๐ง)(+gโ๐
)(๐ฆ(.rโ๐
)๐ง)) = ((๐ง(.rโ๐
)๐ฅ)(+gโ๐
)(๐ง(.rโ๐
)๐ฆ))) |
33 | | simpl1l 1221 |
. . . . . . . . . . 11
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ ๐
โ Rng) |
34 | 5, 26 | sselid 3975 |
. . . . . . . . . . 11
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ ๐ฅ โ ๐ต) |
35 | 5, 29 | sselid 3975 |
. . . . . . . . . . 11
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ ๐ฆ โ ๐ต) |
36 | | simp1r 1195 |
. . . . . . . . . . . 12
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โ ๐ โ ๐ต) |
37 | 36 | sselda 3977 |
. . . . . . . . . . 11
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ ๐ง โ ๐ต) |
38 | | eqid 2726 |
. . . . . . . . . . . 12
โข
(+gโ๐
) = (+gโ๐
) |
39 | 2, 38, 10 | rngdir 20066 |
. . . . . . . . . . 11
โข ((๐
โ Rng โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ(+gโ๐
)๐ฆ)(.rโ๐
)๐ง) = ((๐ฅ(.rโ๐
)๐ง)(+gโ๐
)(๐ฆ(.rโ๐
)๐ง))) |
40 | 33, 34, 35, 37, 39 | syl13anc 1369 |
. . . . . . . . . 10
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ ((๐ฅ(+gโ๐
)๐ฆ)(.rโ๐
)๐ง) = ((๐ฅ(.rโ๐
)๐ง)(+gโ๐
)(๐ฆ(.rโ๐
)๐ง))) |
41 | 2, 38, 10 | rngdi 20065 |
. . . . . . . . . . 11
โข ((๐
โ Rng โง (๐ง โ ๐ต โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ง(.rโ๐
)(๐ฅ(+gโ๐
)๐ฆ)) = ((๐ง(.rโ๐
)๐ฅ)(+gโ๐
)(๐ง(.rโ๐
)๐ฆ))) |
42 | 33, 37, 34, 35, 41 | syl13anc 1369 |
. . . . . . . . . 10
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ (๐ง(.rโ๐
)(๐ฅ(+gโ๐
)๐ฆ)) = ((๐ง(.rโ๐
)๐ฅ)(+gโ๐
)(๐ง(.rโ๐
)๐ฆ))) |
43 | 32, 40, 42 | 3eqtr4d 2776 |
. . . . . . . . 9
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โง ๐ง โ ๐) โ ((๐ฅ(+gโ๐
)๐ฆ)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)(๐ฅ(+gโ๐
)๐ฆ))) |
44 | 43 | ralrimiva 3140 |
. . . . . . . 8
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โ โ๐ง โ ๐ ((๐ฅ(+gโ๐
)๐ฆ)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)(๐ฅ(+gโ๐
)๐ฆ))) |
45 | | simp1l 1194 |
. . . . . . . . . 10
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โ ๐
โ Rng) |
46 | | simp2 1134 |
. . . . . . . . . . 11
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โ ๐ฅ โ (๐โ๐)) |
47 | 5, 46 | sselid 3975 |
. . . . . . . . . 10
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โ ๐ฅ โ ๐ต) |
48 | | simp3 1135 |
. . . . . . . . . . 11
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โ ๐ฆ โ (๐โ๐)) |
49 | 5, 48 | sselid 3975 |
. . . . . . . . . 10
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โ ๐ฆ โ ๐ต) |
50 | 2, 38 | rngacl 20067 |
. . . . . . . . . 10
โข ((๐
โ Rng โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ(+gโ๐
)๐ฆ) โ ๐ต) |
51 | 45, 47, 49, 50 | syl3anc 1368 |
. . . . . . . . 9
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โ (๐ฅ(+gโ๐
)๐ฆ) โ ๐ต) |
52 | 3, 21, 4 | cntzel 19239 |
. . . . . . . . 9
โข ((๐ โ ๐ต โง (๐ฅ(+gโ๐
)๐ฆ) โ ๐ต) โ ((๐ฅ(+gโ๐
)๐ฆ) โ (๐โ๐) โ โ๐ง โ ๐ ((๐ฅ(+gโ๐
)๐ฆ)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)(๐ฅ(+gโ๐
)๐ฆ)))) |
53 | 36, 51, 52 | syl2anc 583 |
. . . . . . . 8
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โ ((๐ฅ(+gโ๐
)๐ฆ) โ (๐โ๐) โ โ๐ง โ ๐ ((๐ฅ(+gโ๐
)๐ฆ)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)(๐ฅ(+gโ๐
)๐ฆ)))) |
54 | 44, 53 | mpbird 257 |
. . . . . . 7
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐) โง ๐ฆ โ (๐โ๐)) โ (๐ฅ(+gโ๐
)๐ฆ) โ (๐โ๐)) |
55 | 54 | 3expa 1115 |
. . . . . 6
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โง ๐ฆ โ (๐โ๐)) โ (๐ฅ(+gโ๐
)๐ฆ) โ (๐โ๐)) |
56 | 55 | ralrimiva 3140 |
. . . . 5
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โ โ๐ฆ โ (๐โ๐)(๐ฅ(+gโ๐
)๐ฆ) โ (๐โ๐)) |
57 | 27 | adantll 711 |
. . . . . . . . 9
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โง ๐ง โ ๐) โ (๐ฅ(.rโ๐
)๐ง) = (๐ง(.rโ๐
)๐ฅ)) |
58 | 57 | fveq2d 6889 |
. . . . . . . 8
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โง ๐ง โ ๐) โ ((invgโ๐
)โ(๐ฅ(.rโ๐
)๐ง)) = ((invgโ๐
)โ(๐ง(.rโ๐
)๐ฅ))) |
59 | | eqid 2726 |
. . . . . . . . 9
โข
(invgโ๐
) = (invgโ๐
) |
60 | | simplll 772 |
. . . . . . . . 9
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โง ๐ง โ ๐) โ ๐
โ Rng) |
61 | | simplr 766 |
. . . . . . . . . 10
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โง ๐ง โ ๐) โ ๐ฅ โ (๐โ๐)) |
62 | 5, 61 | sselid 3975 |
. . . . . . . . 9
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โง ๐ง โ ๐) โ ๐ฅ โ ๐ต) |
63 | | simplr 766 |
. . . . . . . . . 10
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โ ๐ โ ๐ต) |
64 | 63 | sselda 3977 |
. . . . . . . . 9
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โง ๐ง โ ๐) โ ๐ง โ ๐ต) |
65 | 2, 10, 59, 60, 62, 64 | rngmneg1 20072 |
. . . . . . . 8
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โง ๐ง โ ๐) โ (((invgโ๐
)โ๐ฅ)(.rโ๐
)๐ง) = ((invgโ๐
)โ(๐ฅ(.rโ๐
)๐ง))) |
66 | 2, 10, 59, 60, 64, 62 | rngmneg2 20073 |
. . . . . . . 8
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โง ๐ง โ ๐) โ (๐ง(.rโ๐
)((invgโ๐
)โ๐ฅ)) = ((invgโ๐
)โ(๐ง(.rโ๐
)๐ฅ))) |
67 | 58, 65, 66 | 3eqtr4d 2776 |
. . . . . . 7
โข ((((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โง ๐ง โ ๐) โ (((invgโ๐
)โ๐ฅ)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)((invgโ๐
)โ๐ฅ))) |
68 | 67 | ralrimiva 3140 |
. . . . . 6
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โ โ๐ง โ ๐ (((invgโ๐
)โ๐ฅ)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)((invgโ๐
)โ๐ฅ))) |
69 | | rnggrp 20063 |
. . . . . . . . 9
โข (๐
โ Rng โ ๐
โ Grp) |
70 | 69 | ad2antrr 723 |
. . . . . . . 8
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โ ๐
โ Grp) |
71 | | simpr 484 |
. . . . . . . . 9
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โ ๐ฅ โ (๐โ๐)) |
72 | 5, 71 | sselid 3975 |
. . . . . . . 8
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โ ๐ฅ โ ๐ต) |
73 | 2, 59, 70, 72 | grpinvcld 18918 |
. . . . . . 7
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โ ((invgโ๐
)โ๐ฅ) โ ๐ต) |
74 | 3, 21, 4 | cntzel 19239 |
. . . . . . 7
โข ((๐ โ ๐ต โง ((invgโ๐
)โ๐ฅ) โ ๐ต) โ (((invgโ๐
)โ๐ฅ) โ (๐โ๐) โ โ๐ง โ ๐ (((invgโ๐
)โ๐ฅ)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)((invgโ๐
)โ๐ฅ)))) |
75 | 63, 73, 74 | syl2anc 583 |
. . . . . 6
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โ (((invgโ๐
)โ๐ฅ) โ (๐โ๐) โ โ๐ง โ ๐ (((invgโ๐
)โ๐ฅ)(.rโ๐
)๐ง) = (๐ง(.rโ๐
)((invgโ๐
)โ๐ฅ)))) |
76 | 68, 75 | mpbird 257 |
. . . . 5
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โ ((invgโ๐
)โ๐ฅ) โ (๐โ๐)) |
77 | 56, 76 | jca 511 |
. . . 4
โข (((๐
โ Rng โง ๐ โ ๐ต) โง ๐ฅ โ (๐โ๐)) โ (โ๐ฆ โ (๐โ๐)(๐ฅ(+gโ๐
)๐ฆ) โ (๐โ๐) โง ((invgโ๐
)โ๐ฅ) โ (๐โ๐))) |
78 | 77 | ralrimiva 3140 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ โ๐ฅ โ (๐โ๐)(โ๐ฆ โ (๐โ๐)(๐ฅ(+gโ๐
)๐ฆ) โ (๐โ๐) โง ((invgโ๐
)โ๐ฅ) โ (๐โ๐))) |
79 | 69 | adantr 480 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ๐
โ Grp) |
80 | 2, 38, 59 | issubg2 19068 |
. . . 4
โข (๐
โ Grp โ ((๐โ๐) โ (SubGrpโ๐
) โ ((๐โ๐) โ ๐ต โง (๐โ๐) โ โ
โง โ๐ฅ โ (๐โ๐)(โ๐ฆ โ (๐โ๐)(๐ฅ(+gโ๐
)๐ฆ) โ (๐โ๐) โง ((invgโ๐
)โ๐ฅ) โ (๐โ๐))))) |
81 | 79, 80 | syl 17 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ((๐โ๐) โ (SubGrpโ๐
) โ ((๐โ๐) โ ๐ต โง (๐โ๐) โ โ
โง โ๐ฅ โ (๐โ๐)(โ๐ฆ โ (๐โ๐)(๐ฅ(+gโ๐
)๐ฆ) โ (๐โ๐) โง ((invgโ๐
)โ๐ฅ) โ (๐โ๐))))) |
82 | 6, 25, 78, 81 | mpbir3and 1339 |
. 2
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (๐โ๐) โ (SubGrpโ๐
)) |
83 | | eqid 2726 |
. . . . 5
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
84 | 83 | rngmgp 20061 |
. . . 4
โข (๐
โ Rng โ
(mulGrpโ๐
) โ
Smgrp) |
85 | 83, 2 | mgpbas 20045 |
. . . . . 6
โข ๐ต =
(Baseโ(mulGrpโ๐
)) |
86 | 85 | sseq2i 4006 |
. . . . 5
โข (๐ โ ๐ต โ ๐ โ (Baseโ(mulGrpโ๐
))) |
87 | 86 | biimpi 215 |
. . . 4
โข (๐ โ ๐ต โ ๐ โ (Baseโ(mulGrpโ๐
))) |
88 | | eqid 2726 |
. . . . 5
โข
(Baseโ(mulGrpโ๐
)) = (Baseโ(mulGrpโ๐
)) |
89 | 1 | fveq2i 6888 |
. . . . . 6
โข
(Cntzโ๐) =
(Cntzโ(mulGrpโ๐
)) |
90 | 4, 89 | eqtri 2754 |
. . . . 5
โข ๐ =
(Cntzโ(mulGrpโ๐
)) |
91 | | eqid 2726 |
. . . . 5
โข (๐โ๐) = (๐โ๐) |
92 | 88, 90, 91 | cntzsgrpcl 19250 |
. . . 4
โข
(((mulGrpโ๐
)
โ Smgrp โง ๐
โ (Baseโ(mulGrpโ๐
))) โ โ๐ฅ โ (๐โ๐)โ๐ฆ โ (๐โ๐)(๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) โ (๐โ๐)) |
93 | 84, 87, 92 | syl2an 595 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ โ๐ฅ โ (๐โ๐)โ๐ฆ โ (๐โ๐)(๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) โ (๐โ๐)) |
94 | 83, 10 | mgpplusg 20043 |
. . . . . 6
โข
(.rโ๐
) = (+gโ(mulGrpโ๐
)) |
95 | 94 | oveqi 7418 |
. . . . 5
โข (๐ฅ(.rโ๐
)๐ฆ) = (๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) |
96 | 95 | eleq1i 2818 |
. . . 4
โข ((๐ฅ(.rโ๐
)๐ฆ) โ (๐โ๐) โ (๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) โ (๐โ๐)) |
97 | 96 | 2ralbii 3122 |
. . 3
โข
(โ๐ฅ โ
(๐โ๐)โ๐ฆ โ (๐โ๐)(๐ฅ(.rโ๐
)๐ฆ) โ (๐โ๐) โ โ๐ฅ โ (๐โ๐)โ๐ฆ โ (๐โ๐)(๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) โ (๐โ๐)) |
98 | 93, 97 | sylibr 233 |
. 2
โข ((๐
โ Rng โง ๐ โ ๐ต) โ โ๐ฅ โ (๐โ๐)โ๐ฆ โ (๐โ๐)(๐ฅ(.rโ๐
)๐ฆ) โ (๐โ๐)) |
99 | 2, 10 | issubrng2 20458 |
. . 3
โข (๐
โ Rng โ ((๐โ๐) โ (SubRngโ๐
) โ ((๐โ๐) โ (SubGrpโ๐
) โง โ๐ฅ โ (๐โ๐)โ๐ฆ โ (๐โ๐)(๐ฅ(.rโ๐
)๐ฆ) โ (๐โ๐)))) |
100 | 99 | adantr 480 |
. 2
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ((๐โ๐) โ (SubRngโ๐
) โ ((๐โ๐) โ (SubGrpโ๐
) โง โ๐ฅ โ (๐โ๐)โ๐ฆ โ (๐โ๐)(๐ฅ(.rโ๐
)๐ฆ) โ (๐โ๐)))) |
101 | 82, 98, 100 | mpbir2and 710 |
1
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (๐โ๐) โ (SubRngโ๐
)) |