Step | Hyp | Ref
| Expression |
1 | | subrngsubg 20452 |
. . 3
โข (๐ด โ (SubRngโ๐
) โ ๐ด โ (SubGrpโ๐
)) |
2 | | issubrng2.t |
. . . . . 6
โข ยท =
(.rโ๐
) |
3 | 2 | subrngmcl 20457 |
. . . . 5
โข ((๐ด โ (SubRngโ๐
) โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ด) โ (๐ฅ ยท ๐ฆ) โ ๐ด) |
4 | 3 | 3expb 1117 |
. . . 4
โข ((๐ด โ (SubRngโ๐
) โง (๐ฅ โ ๐ด โง ๐ฆ โ ๐ด)) โ (๐ฅ ยท ๐ฆ) โ ๐ด) |
5 | 4 | ralrimivva 3194 |
. . 3
โข (๐ด โ (SubRngโ๐
) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด) |
6 | 1, 5 | jca 511 |
. 2
โข (๐ด โ (SubRngโ๐
) โ (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) |
7 | | simpl 482 |
. . . 4
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ ๐
โ Rng) |
8 | | simprl 768 |
. . . . . 6
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ ๐ด โ (SubGrpโ๐
)) |
9 | | eqid 2726 |
. . . . . . 7
โข (๐
โพs ๐ด) = (๐
โพs ๐ด) |
10 | 9 | subgbas 19057 |
. . . . . 6
โข (๐ด โ (SubGrpโ๐
) โ ๐ด = (Baseโ(๐
โพs ๐ด))) |
11 | 8, 10 | syl 17 |
. . . . 5
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ ๐ด = (Baseโ(๐
โพs ๐ด))) |
12 | | eqid 2726 |
. . . . . . 7
โข
(+gโ๐
) = (+gโ๐
) |
13 | 9, 12 | ressplusg 17244 |
. . . . . 6
โข (๐ด โ (SubGrpโ๐
) โ
(+gโ๐
) =
(+gโ(๐
โพs ๐ด))) |
14 | 8, 13 | syl 17 |
. . . . 5
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ (+gโ๐
) = (+gโ(๐
โพs ๐ด))) |
15 | 9, 2 | ressmulr 17261 |
. . . . . 6
โข (๐ด โ (SubGrpโ๐
) โ ยท =
(.rโ(๐
โพs ๐ด))) |
16 | 8, 15 | syl 17 |
. . . . 5
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ ยท =
(.rโ(๐
โพs ๐ด))) |
17 | | rngabl 20060 |
. . . . . 6
โข (๐
โ Rng โ ๐
โ Abel) |
18 | 9 | subgabl 19756 |
. . . . . 6
โข ((๐
โ Abel โง ๐ด โ (SubGrpโ๐
)) โ (๐
โพs ๐ด) โ Abel) |
19 | 17, 8, 18 | syl2an2r 682 |
. . . . 5
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ (๐
โพs ๐ด) โ Abel) |
20 | | simprr 770 |
. . . . . . 7
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด) |
21 | | oveq1 7412 |
. . . . . . . . 9
โข (๐ฅ = ๐ข โ (๐ฅ ยท ๐ฆ) = (๐ข ยท ๐ฆ)) |
22 | 21 | eleq1d 2812 |
. . . . . . . 8
โข (๐ฅ = ๐ข โ ((๐ฅ ยท ๐ฆ) โ ๐ด โ (๐ข ยท ๐ฆ) โ ๐ด)) |
23 | | oveq2 7413 |
. . . . . . . . 9
โข (๐ฆ = ๐ฃ โ (๐ข ยท ๐ฆ) = (๐ข ยท ๐ฃ)) |
24 | 23 | eleq1d 2812 |
. . . . . . . 8
โข (๐ฆ = ๐ฃ โ ((๐ข ยท ๐ฆ) โ ๐ด โ (๐ข ยท ๐ฃ) โ ๐ด)) |
25 | 22, 24 | rspc2v 3617 |
. . . . . . 7
โข ((๐ข โ ๐ด โง ๐ฃ โ ๐ด) โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด โ (๐ข ยท ๐ฃ) โ ๐ด)) |
26 | 20, 25 | syl5com 31 |
. . . . . 6
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ ((๐ข โ ๐ด โง ๐ฃ โ ๐ด) โ (๐ข ยท ๐ฃ) โ ๐ด)) |
27 | 26 | 3impib 1113 |
. . . . 5
โข (((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โง ๐ข โ ๐ด โง ๐ฃ โ ๐ด) โ (๐ข ยท ๐ฃ) โ ๐ด) |
28 | | issubrng2.b |
. . . . . . . . . . 11
โข ๐ต = (Baseโ๐
) |
29 | 28 | subgss 19054 |
. . . . . . . . . 10
โข (๐ด โ (SubGrpโ๐
) โ ๐ด โ ๐ต) |
30 | 8, 29 | syl 17 |
. . . . . . . . 9
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ ๐ด โ ๐ต) |
31 | 30 | sseld 3976 |
. . . . . . . 8
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ (๐ข โ ๐ด โ ๐ข โ ๐ต)) |
32 | 30 | sseld 3976 |
. . . . . . . 8
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ (๐ฃ โ ๐ด โ ๐ฃ โ ๐ต)) |
33 | 30 | sseld 3976 |
. . . . . . . 8
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ (๐ค โ ๐ด โ ๐ค โ ๐ต)) |
34 | 31, 32, 33 | 3anim123d 1439 |
. . . . . . 7
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ ((๐ข โ ๐ด โง ๐ฃ โ ๐ด โง ๐ค โ ๐ด) โ (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต))) |
35 | 34 | imp 406 |
. . . . . 6
โข (((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โง (๐ข โ ๐ด โง ๐ฃ โ ๐ด โง ๐ค โ ๐ด)) โ (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต)) |
36 | 28, 2 | rngass 20064 |
. . . . . . 7
โข ((๐
โ Rng โง (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต)) โ ((๐ข ยท ๐ฃ) ยท ๐ค) = (๐ข ยท (๐ฃ ยท ๐ค))) |
37 | 36 | adantlr 712 |
. . . . . 6
โข (((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โง (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต)) โ ((๐ข ยท ๐ฃ) ยท ๐ค) = (๐ข ยท (๐ฃ ยท ๐ค))) |
38 | 35, 37 | syldan 590 |
. . . . 5
โข (((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โง (๐ข โ ๐ด โง ๐ฃ โ ๐ด โง ๐ค โ ๐ด)) โ ((๐ข ยท ๐ฃ) ยท ๐ค) = (๐ข ยท (๐ฃ ยท ๐ค))) |
39 | 28, 12, 2 | rngdi 20065 |
. . . . . . 7
โข ((๐
โ Rng โง (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต)) โ (๐ข ยท (๐ฃ(+gโ๐
)๐ค)) = ((๐ข ยท ๐ฃ)(+gโ๐
)(๐ข ยท ๐ค))) |
40 | 39 | adantlr 712 |
. . . . . 6
โข (((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โง (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต)) โ (๐ข ยท (๐ฃ(+gโ๐
)๐ค)) = ((๐ข ยท ๐ฃ)(+gโ๐
)(๐ข ยท ๐ค))) |
41 | 35, 40 | syldan 590 |
. . . . 5
โข (((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โง (๐ข โ ๐ด โง ๐ฃ โ ๐ด โง ๐ค โ ๐ด)) โ (๐ข ยท (๐ฃ(+gโ๐
)๐ค)) = ((๐ข ยท ๐ฃ)(+gโ๐
)(๐ข ยท ๐ค))) |
42 | 28, 12, 2 | rngdir 20066 |
. . . . . . 7
โข ((๐
โ Rng โง (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต)) โ ((๐ข(+gโ๐
)๐ฃ) ยท ๐ค) = ((๐ข ยท ๐ค)(+gโ๐
)(๐ฃ ยท ๐ค))) |
43 | 42 | adantlr 712 |
. . . . . 6
โข (((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โง (๐ข โ ๐ต โง ๐ฃ โ ๐ต โง ๐ค โ ๐ต)) โ ((๐ข(+gโ๐
)๐ฃ) ยท ๐ค) = ((๐ข ยท ๐ค)(+gโ๐
)(๐ฃ ยท ๐ค))) |
44 | 35, 43 | syldan 590 |
. . . . 5
โข (((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โง (๐ข โ ๐ด โง ๐ฃ โ ๐ด โง ๐ค โ ๐ด)) โ ((๐ข(+gโ๐
)๐ฃ) ยท ๐ค) = ((๐ข ยท ๐ค)(+gโ๐
)(๐ฃ ยท ๐ค))) |
45 | 11, 14, 16, 19, 27, 38, 41, 44 | isrngd 20078 |
. . . 4
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ (๐
โพs ๐ด) โ Rng) |
46 | 28 | issubrng 20447 |
. . . 4
โข (๐ด โ (SubRngโ๐
) โ (๐
โ Rng โง (๐
โพs ๐ด) โ Rng โง ๐ด โ ๐ต)) |
47 | 7, 45, 30, 46 | syl3anbrc 1340 |
. . 3
โข ((๐
โ Rng โง (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด)) โ ๐ด โ (SubRngโ๐
)) |
48 | 47 | ex 412 |
. 2
โข (๐
โ Rng โ ((๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด) โ ๐ด โ (SubRngโ๐
))) |
49 | 6, 48 | impbid2 225 |
1
โข (๐
โ Rng โ (๐ด โ (SubRngโ๐
) โ (๐ด โ (SubGrpโ๐
) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ ยท ๐ฆ) โ ๐ด))) |