Step | Hyp | Ref
| Expression |
1 | | imacrhmcl.h |
. . . 4
β’ (π β πΉ β (π RingHom π)) |
2 | | imacrhmcl.s |
. . . 4
β’ (π β π β (SubRingβπ)) |
3 | | rhmima 20506 |
. . . 4
β’ ((πΉ β (π RingHom π) β§ π β (SubRingβπ)) β (πΉ β π) β (SubRingβπ)) |
4 | 1, 2, 3 | syl2anc 583 |
. . 3
β’ (π β (πΉ β π) β (SubRingβπ)) |
5 | | imacrhmcl.c |
. . . 4
β’ πΆ = (π βΎs (πΉ β π)) |
6 | 5 | subrgring 20476 |
. . 3
β’ ((πΉ β π) β (SubRingβπ) β πΆ β Ring) |
7 | 4, 6 | syl 17 |
. 2
β’ (π β πΆ β Ring) |
8 | 5 | ressbasss2 17194 |
. . . . . 6
β’
(BaseβπΆ)
β (πΉ β π) |
9 | 8 | sseli 3973 |
. . . . 5
β’ (π₯ β (BaseβπΆ) β π₯ β (πΉ β π)) |
10 | 8 | sseli 3973 |
. . . . 5
β’ (π¦ β (BaseβπΆ) β π¦ β (πΉ β π)) |
11 | 9, 10 | anim12i 612 |
. . . 4
β’ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) |
12 | | eqid 2726 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
13 | | eqid 2726 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
14 | 12, 13 | rhmf 20387 |
. . . . . . . . 9
β’ (πΉ β (π RingHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
15 | 1, 14 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:(Baseβπ)βΆ(Baseβπ)) |
16 | 15 | ffund 6715 |
. . . . . . 7
β’ (π β Fun πΉ) |
17 | | fvelima 6951 |
. . . . . . 7
β’ ((Fun
πΉ β§ π₯ β (πΉ β π)) β βπ β π (πΉβπ) = π₯) |
18 | 16, 17 | sylan 579 |
. . . . . 6
β’ ((π β§ π₯ β (πΉ β π)) β βπ β π (πΉβπ) = π₯) |
19 | 18 | adantrr 714 |
. . . . 5
β’ ((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β βπ β π (πΉβπ) = π₯) |
20 | | fvelima 6951 |
. . . . . . . . 9
β’ ((Fun
πΉ β§ π¦ β (πΉ β π)) β βπ β π (πΉβπ) = π¦) |
21 | 16, 20 | sylan 579 |
. . . . . . . 8
β’ ((π β§ π¦ β (πΉ β π)) β βπ β π (πΉβπ) = π¦) |
22 | 21 | adantrl 713 |
. . . . . . 7
β’ ((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β βπ β π (πΉβπ) = π¦) |
23 | 22 | adantr 480 |
. . . . . 6
β’ (((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β βπ β π (πΉβπ) = π¦) |
24 | | imacrhmcl.m |
. . . . . . . . . . 11
β’ (π β π β CRing) |
25 | 24 | ad3antrrr 727 |
. . . . . . . . . 10
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β π β CRing) |
26 | 12 | subrgss 20474 |
. . . . . . . . . . . . 13
β’ (π β (SubRingβπ) β π β (Baseβπ)) |
27 | 2, 26 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β (Baseβπ)) |
28 | 27 | ad3antrrr 727 |
. . . . . . . . . . 11
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β π β (Baseβπ)) |
29 | | simplrl 774 |
. . . . . . . . . . 11
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β π β π) |
30 | 28, 29 | sseldd 3978 |
. . . . . . . . . 10
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β π β (Baseβπ)) |
31 | | simprl 768 |
. . . . . . . . . . 11
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β π β π) |
32 | 28, 31 | sseldd 3978 |
. . . . . . . . . 10
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β π β (Baseβπ)) |
33 | | eqid 2726 |
. . . . . . . . . . 11
β’
(.rβπ) = (.rβπ) |
34 | 12, 33 | crngcom 20156 |
. . . . . . . . . 10
β’ ((π β CRing β§ π β (Baseβπ) β§ π β (Baseβπ)) β (π(.rβπ)π) = (π(.rβπ)π)) |
35 | 25, 30, 32, 34 | syl3anc 1368 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β (π(.rβπ)π) = (π(.rβπ)π)) |
36 | 35 | fveq2d 6889 |
. . . . . . . 8
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β (πΉβ(π(.rβπ)π)) = (πΉβ(π(.rβπ)π))) |
37 | 1 | ad3antrrr 727 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β πΉ β (π RingHom π)) |
38 | | eqid 2726 |
. . . . . . . . . 10
β’
(.rβπ) = (.rβπ) |
39 | 12, 33, 38 | rhmmul 20388 |
. . . . . . . . 9
β’ ((πΉ β (π RingHom π) β§ π β (Baseβπ) β§ π β (Baseβπ)) β (πΉβ(π(.rβπ)π)) = ((πΉβπ)(.rβπ)(πΉβπ))) |
40 | 37, 30, 32, 39 | syl3anc 1368 |
. . . . . . . 8
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β (πΉβ(π(.rβπ)π)) = ((πΉβπ)(.rβπ)(πΉβπ))) |
41 | 12, 33, 38 | rhmmul 20388 |
. . . . . . . . 9
β’ ((πΉ β (π RingHom π) β§ π β (Baseβπ) β§ π β (Baseβπ)) β (πΉβ(π(.rβπ)π)) = ((πΉβπ)(.rβπ)(πΉβπ))) |
42 | 37, 32, 30, 41 | syl3anc 1368 |
. . . . . . . 8
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β (πΉβ(π(.rβπ)π)) = ((πΉβπ)(.rβπ)(πΉβπ))) |
43 | 36, 40, 42 | 3eqtr3d 2774 |
. . . . . . 7
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β ((πΉβπ)(.rβπ)(πΉβπ)) = ((πΉβπ)(.rβπ)(πΉβπ))) |
44 | | imaexg 7903 |
. . . . . . . . . 10
β’ (πΉ β (π RingHom π) β (πΉ β π) β V) |
45 | 5, 38 | ressmulr 17261 |
. . . . . . . . . 10
β’ ((πΉ β π) β V β (.rβπ) = (.rβπΆ)) |
46 | 1, 44, 45 | 3syl 18 |
. . . . . . . . 9
β’ (π β (.rβπ) = (.rβπΆ)) |
47 | 46 | ad3antrrr 727 |
. . . . . . . 8
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β (.rβπ) = (.rβπΆ)) |
48 | | simplrr 775 |
. . . . . . . 8
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β (πΉβπ) = π₯) |
49 | | simprr 770 |
. . . . . . . 8
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β (πΉβπ) = π¦) |
50 | 47, 48, 49 | oveq123d 7426 |
. . . . . . 7
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β ((πΉβπ)(.rβπ)(πΉβπ)) = (π₯(.rβπΆ)π¦)) |
51 | 47, 49, 48 | oveq123d 7426 |
. . . . . . 7
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β ((πΉβπ)(.rβπ)(πΉβπ)) = (π¦(.rβπΆ)π₯)) |
52 | 43, 50, 51 | 3eqtr3d 2774 |
. . . . . 6
β’ ((((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β§ (π β π β§ (πΉβπ) = π¦)) β (π₯(.rβπΆ)π¦) = (π¦(.rβπΆ)π₯)) |
53 | 23, 52 | rexlimddv 3155 |
. . . . 5
β’ (((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β§ (π β π β§ (πΉβπ) = π₯)) β (π₯(.rβπΆ)π¦) = (π¦(.rβπΆ)π₯)) |
54 | 19, 53 | rexlimddv 3155 |
. . . 4
β’ ((π β§ (π₯ β (πΉ β π) β§ π¦ β (πΉ β π))) β (π₯(.rβπΆ)π¦) = (π¦(.rβπΆ)π₯)) |
55 | 11, 54 | sylan2 592 |
. . 3
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (π₯(.rβπΆ)π¦) = (π¦(.rβπΆ)π₯)) |
56 | 55 | ralrimivva 3194 |
. 2
β’ (π β βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)(π₯(.rβπΆ)π¦) = (π¦(.rβπΆ)π₯)) |
57 | | eqid 2726 |
. . 3
β’
(BaseβπΆ) =
(BaseβπΆ) |
58 | | eqid 2726 |
. . 3
β’
(.rβπΆ) = (.rβπΆ) |
59 | 57, 58 | iscrng2 20157 |
. 2
β’ (πΆ β CRing β (πΆ β Ring β§ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)(π₯(.rβπΆ)π¦) = (π¦(.rβπΆ)π₯))) |
60 | 7, 56, 59 | sylanbrc 582 |
1
β’ (π β πΆ β CRing) |