Step | Hyp | Ref
| Expression |
1 | | rnghomadd.1 |
. . . . . . 7
β’ πΊ = (1st βπ
) |
2 | | eqid 2737 |
. . . . . . 7
β’
(2nd βπ
) = (2nd βπ
) |
3 | | rnghomadd.2 |
. . . . . . 7
β’ π = ran πΊ |
4 | | eqid 2737 |
. . . . . . 7
β’
(GIdβ(2nd βπ
)) = (GIdβ(2nd βπ
)) |
5 | | rnghomadd.3 |
. . . . . . 7
β’ π½ = (1st βπ) |
6 | | eqid 2737 |
. . . . . . 7
β’
(2nd βπ) = (2nd βπ) |
7 | | eqid 2737 |
. . . . . . 7
β’ ran π½ = ran π½ |
8 | | eqid 2737 |
. . . . . . 7
β’
(GIdβ(2nd βπ)) = (GIdβ(2nd βπ)) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | isrngohom 36427 |
. . . . . 6
β’ ((π
β RingOps β§ π β RingOps) β (πΉ β (π
RngHom π) β (πΉ:πβΆran π½ β§ (πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ)) β§ βπ₯ β π βπ¦ β π ((πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦)) β§ (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦)))))) |
10 | 9 | biimpa 478 |
. . . . 5
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β (πΉ:πβΆran π½ β§ (πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ)) β§ βπ₯ β π βπ¦ β π ((πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦)) β§ (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦))))) |
11 | 10 | simp3d 1145 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β βπ₯ β π βπ¦ β π ((πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦)) β§ (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦)))) |
12 | 11 | 3impa 1111 |
. . 3
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β βπ₯ β π βπ¦ β π ((πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦)) β§ (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦)))) |
13 | | simpl 484 |
. . . 4
β’ (((πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦)) β§ (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) β (πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦))) |
14 | 13 | 2ralimi 3127 |
. . 3
β’
(βπ₯ β
π βπ¦ β π ((πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦)) β§ (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) β βπ₯ β π βπ¦ β π (πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦))) |
15 | 12, 14 | syl 17 |
. 2
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β βπ₯ β π βπ¦ β π (πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦))) |
16 | | fvoveq1 7381 |
. . . 4
β’ (π₯ = π΄ β (πΉβ(π₯πΊπ¦)) = (πΉβ(π΄πΊπ¦))) |
17 | | fveq2 6843 |
. . . . 5
β’ (π₯ = π΄ β (πΉβπ₯) = (πΉβπ΄)) |
18 | 17 | oveq1d 7373 |
. . . 4
β’ (π₯ = π΄ β ((πΉβπ₯)π½(πΉβπ¦)) = ((πΉβπ΄)π½(πΉβπ¦))) |
19 | 16, 18 | eqeq12d 2753 |
. . 3
β’ (π₯ = π΄ β ((πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦)) β (πΉβ(π΄πΊπ¦)) = ((πΉβπ΄)π½(πΉβπ¦)))) |
20 | | oveq2 7366 |
. . . . 5
β’ (π¦ = π΅ β (π΄πΊπ¦) = (π΄πΊπ΅)) |
21 | 20 | fveq2d 6847 |
. . . 4
β’ (π¦ = π΅ β (πΉβ(π΄πΊπ¦)) = (πΉβ(π΄πΊπ΅))) |
22 | | fveq2 6843 |
. . . . 5
β’ (π¦ = π΅ β (πΉβπ¦) = (πΉβπ΅)) |
23 | 22 | oveq2d 7374 |
. . . 4
β’ (π¦ = π΅ β ((πΉβπ΄)π½(πΉβπ¦)) = ((πΉβπ΄)π½(πΉβπ΅))) |
24 | 21, 23 | eqeq12d 2753 |
. . 3
β’ (π¦ = π΅ β ((πΉβ(π΄πΊπ¦)) = ((πΉβπ΄)π½(πΉβπ¦)) β (πΉβ(π΄πΊπ΅)) = ((πΉβπ΄)π½(πΉβπ΅)))) |
25 | 19, 24 | rspc2v 3591 |
. 2
β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β π βπ¦ β π (πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦)) β (πΉβ(π΄πΊπ΅)) = ((πΉβπ΄)π½(πΉβπ΅)))) |
26 | 15, 25 | mpan9 508 |
1
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄πΊπ΅)) = ((πΉβπ΄)π½(πΉβπ΅))) |