Step | Hyp | Ref
| Expression |
1 | | rngabl 20060 |
. . . 4
β’ (π
β Rng β π
β Abel) |
2 | 1 | 3ad2ant1 1130 |
. . 3
β’ ((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β π
β Abel) |
3 | | simp3 1135 |
. . 3
β’ ((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β π β (SubGrpβπ
)) |
4 | | rnglidlabl.i |
. . . 4
β’ πΌ = (π
βΎs π) |
5 | 4 | subgabl 19756 |
. . 3
β’ ((π
β Abel β§ π β (SubGrpβπ
)) β πΌ β Abel) |
6 | 2, 3, 5 | syl2anc 583 |
. 2
β’ ((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β πΌ β Abel) |
7 | | eqid 2726 |
. . . 4
β’
(0gβπ
) = (0gβπ
) |
8 | 7 | subg0cl 19061 |
. . 3
β’ (π β (SubGrpβπ
) β
(0gβπ
)
β π) |
9 | | rnglidlabl.l |
. . . 4
β’ πΏ = (LIdealβπ
) |
10 | 9, 4, 7 | rnglidlmsgrp 21104 |
. . 3
β’ ((π
β Rng β§ π β πΏ β§ (0gβπ
) β π) β (mulGrpβπΌ) β Smgrp) |
11 | 8, 10 | syl3an3 1162 |
. 2
β’ ((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β (mulGrpβπΌ) β Smgrp) |
12 | | simpl1 1188 |
. . . . 5
β’ (((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β§ (π β (BaseβπΌ) β§ π β (BaseβπΌ) β§ π β (BaseβπΌ))) β π
β Rng) |
13 | 9, 4 | lidlssbas 21072 |
. . . . . . . . 9
β’ (π β πΏ β (BaseβπΌ) β (Baseβπ
)) |
14 | 13 | sseld 3976 |
. . . . . . . 8
β’ (π β πΏ β (π β (BaseβπΌ) β π β (Baseβπ
))) |
15 | 13 | sseld 3976 |
. . . . . . . 8
β’ (π β πΏ β (π β (BaseβπΌ) β π β (Baseβπ
))) |
16 | 13 | sseld 3976 |
. . . . . . . 8
β’ (π β πΏ β (π β (BaseβπΌ) β π β (Baseβπ
))) |
17 | 14, 15, 16 | 3anim123d 1439 |
. . . . . . 7
β’ (π β πΏ β ((π β (BaseβπΌ) β§ π β (BaseβπΌ) β§ π β (BaseβπΌ)) β (π β (Baseβπ
) β§ π β (Baseβπ
) β§ π β (Baseβπ
)))) |
18 | 17 | 3ad2ant2 1131 |
. . . . . 6
β’ ((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β ((π β (BaseβπΌ) β§ π β (BaseβπΌ) β§ π β (BaseβπΌ)) β (π β (Baseβπ
) β§ π β (Baseβπ
) β§ π β (Baseβπ
)))) |
19 | 18 | imp 406 |
. . . . 5
β’ (((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β§ (π β (BaseβπΌ) β§ π β (BaseβπΌ) β§ π β (BaseβπΌ))) β (π β (Baseβπ
) β§ π β (Baseβπ
) β§ π β (Baseβπ
))) |
20 | | eqid 2726 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
21 | | eqid 2726 |
. . . . . 6
β’
(+gβπ
) = (+gβπ
) |
22 | | eqid 2726 |
. . . . . 6
β’
(.rβπ
) = (.rβπ
) |
23 | 20, 21, 22 | rngdi 20065 |
. . . . 5
β’ ((π
β Rng β§ (π β (Baseβπ
) β§ π β (Baseβπ
) β§ π β (Baseβπ
))) β (π(.rβπ
)(π(+gβπ
)π)) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π))) |
24 | 12, 19, 23 | syl2anc 583 |
. . . 4
β’ (((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β§ (π β (BaseβπΌ) β§ π β (BaseβπΌ) β§ π β (BaseβπΌ))) β (π(.rβπ
)(π(+gβπ
)π)) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π))) |
25 | 20, 21, 22 | rngdir 20066 |
. . . . 5
β’ ((π
β Rng β§ (π β (Baseβπ
) β§ π β (Baseβπ
) β§ π β (Baseβπ
))) β ((π(+gβπ
)π)(.rβπ
)π) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π))) |
26 | 12, 19, 25 | syl2anc 583 |
. . . 4
β’ (((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β§ (π β (BaseβπΌ) β§ π β (BaseβπΌ) β§ π β (BaseβπΌ))) β ((π(+gβπ
)π)(.rβπ
)π) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π))) |
27 | 4, 22 | ressmulr 17261 |
. . . . . . . . . 10
β’ (π β πΏ β (.rβπ
) = (.rβπΌ)) |
28 | 27 | eqcomd 2732 |
. . . . . . . . 9
β’ (π β πΏ β (.rβπΌ) = (.rβπ
)) |
29 | | eqidd 2727 |
. . . . . . . . 9
β’ (π β πΏ β π = π) |
30 | 4, 21 | ressplusg 17244 |
. . . . . . . . . . 11
β’ (π β πΏ β (+gβπ
) = (+gβπΌ)) |
31 | 30 | eqcomd 2732 |
. . . . . . . . . 10
β’ (π β πΏ β (+gβπΌ) = (+gβπ
)) |
32 | 31 | oveqd 7422 |
. . . . . . . . 9
β’ (π β πΏ β (π(+gβπΌ)π) = (π(+gβπ
)π)) |
33 | 28, 29, 32 | oveq123d 7426 |
. . . . . . . 8
β’ (π β πΏ β (π(.rβπΌ)(π(+gβπΌ)π)) = (π(.rβπ
)(π(+gβπ
)π))) |
34 | 28 | oveqd 7422 |
. . . . . . . . 9
β’ (π β πΏ β (π(.rβπΌ)π) = (π(.rβπ
)π)) |
35 | 28 | oveqd 7422 |
. . . . . . . . 9
β’ (π β πΏ β (π(.rβπΌ)π) = (π(.rβπ
)π)) |
36 | 31, 34, 35 | oveq123d 7426 |
. . . . . . . 8
β’ (π β πΏ β ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π))) |
37 | 33, 36 | eqeq12d 2742 |
. . . . . . 7
β’ (π β πΏ β ((π(.rβπΌ)(π(+gβπΌ)π)) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)) β (π(.rβπ
)(π(+gβπ
)π)) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π)))) |
38 | 31 | oveqd 7422 |
. . . . . . . . 9
β’ (π β πΏ β (π(+gβπΌ)π) = (π(+gβπ
)π)) |
39 | | eqidd 2727 |
. . . . . . . . 9
β’ (π β πΏ β π = π) |
40 | 28, 38, 39 | oveq123d 7426 |
. . . . . . . 8
β’ (π β πΏ β ((π(+gβπΌ)π)(.rβπΌ)π) = ((π(+gβπ
)π)(.rβπ
)π)) |
41 | 28 | oveqd 7422 |
. . . . . . . . 9
β’ (π β πΏ β (π(.rβπΌ)π) = (π(.rβπ
)π)) |
42 | 31, 35, 41 | oveq123d 7426 |
. . . . . . . 8
β’ (π β πΏ β ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π))) |
43 | 40, 42 | eqeq12d 2742 |
. . . . . . 7
β’ (π β πΏ β (((π(+gβπΌ)π)(.rβπΌ)π) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)) β ((π(+gβπ
)π)(.rβπ
)π) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π)))) |
44 | 37, 43 | anbi12d 630 |
. . . . . 6
β’ (π β πΏ β (((π(.rβπΌ)(π(+gβπΌ)π)) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)) β§ ((π(+gβπΌ)π)(.rβπΌ)π) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π))) β ((π(.rβπ
)(π(+gβπ
)π)) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π)) β§ ((π(+gβπ
)π)(.rβπ
)π) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π))))) |
45 | 44 | 3ad2ant2 1131 |
. . . . 5
β’ ((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β (((π(.rβπΌ)(π(+gβπΌ)π)) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)) β§ ((π(+gβπΌ)π)(.rβπΌ)π) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π))) β ((π(.rβπ
)(π(+gβπ
)π)) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π)) β§ ((π(+gβπ
)π)(.rβπ
)π) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π))))) |
46 | 45 | adantr 480 |
. . . 4
β’ (((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β§ (π β (BaseβπΌ) β§ π β (BaseβπΌ) β§ π β (BaseβπΌ))) β (((π(.rβπΌ)(π(+gβπΌ)π)) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)) β§ ((π(+gβπΌ)π)(.rβπΌ)π) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π))) β ((π(.rβπ
)(π(+gβπ
)π)) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π)) β§ ((π(+gβπ
)π)(.rβπ
)π) = ((π(.rβπ
)π)(+gβπ
)(π(.rβπ
)π))))) |
47 | 24, 26, 46 | mpbir2and 710 |
. . 3
β’ (((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β§ (π β (BaseβπΌ) β§ π β (BaseβπΌ) β§ π β (BaseβπΌ))) β ((π(.rβπΌ)(π(+gβπΌ)π)) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)) β§ ((π(+gβπΌ)π)(.rβπΌ)π) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)))) |
48 | 47 | ralrimivvva 3197 |
. 2
β’ ((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β βπ β (BaseβπΌ)βπ β (BaseβπΌ)βπ β (BaseβπΌ)((π(.rβπΌ)(π(+gβπΌ)π)) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)) β§ ((π(+gβπΌ)π)(.rβπΌ)π) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)))) |
49 | | eqid 2726 |
. . 3
β’
(BaseβπΌ) =
(BaseβπΌ) |
50 | | eqid 2726 |
. . 3
β’
(mulGrpβπΌ) =
(mulGrpβπΌ) |
51 | | eqid 2726 |
. . 3
β’
(+gβπΌ) = (+gβπΌ) |
52 | | eqid 2726 |
. . 3
β’
(.rβπΌ) = (.rβπΌ) |
53 | 49, 50, 51, 52 | isrng 20059 |
. 2
β’ (πΌ β Rng β (πΌ β Abel β§
(mulGrpβπΌ) β
Smgrp β§ βπ
β (BaseβπΌ)βπ β (BaseβπΌ)βπ β (BaseβπΌ)((π(.rβπΌ)(π(+gβπΌ)π)) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π)) β§ ((π(+gβπΌ)π)(.rβπΌ)π) = ((π(.rβπΌ)π)(+gβπΌ)(π(.rβπΌ)π))))) |
54 | 6, 11, 48, 53 | syl3anbrc 1340 |
1
β’ ((π
β Rng β§ π β πΏ β§ π β (SubGrpβπ
)) β πΌ β Rng) |