Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . 7
β’
(1st βπ) = (1st βπ) |
2 | | eqid 2737 |
. . . . . . 7
β’ ran
(1st βπ) =
ran (1st βπ) |
3 | | eqid 2737 |
. . . . . . 7
β’
(1st βπ) = (1st βπ) |
4 | | eqid 2737 |
. . . . . . 7
β’ ran
(1st βπ) =
ran (1st βπ) |
5 | 1, 2, 3, 4 | rngohomf 36428 |
. . . . . 6
β’ ((π β RingOps β§ π β RingOps β§ πΊ β (π RngHom π)) β πΊ:ran (1st βπ)βΆran (1st
βπ)) |
6 | 5 | 3expa 1119 |
. . . . 5
β’ (((π β RingOps β§ π β RingOps) β§ πΊ β (π RngHom π)) β πΊ:ran (1st βπ)βΆran (1st
βπ)) |
7 | 6 | 3adantl1 1167 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΊ β (π RngHom π)) β πΊ:ran (1st βπ)βΆran (1st
βπ)) |
8 | 7 | adantrl 715 |
. . 3
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β πΊ:ran (1st βπ)βΆran (1st
βπ)) |
9 | | eqid 2737 |
. . . . . . 7
β’
(1st βπ
) = (1st βπ
) |
10 | | eqid 2737 |
. . . . . . 7
β’ ran
(1st βπ
) =
ran (1st βπ
) |
11 | 9, 10, 1, 2 | rngohomf 36428 |
. . . . . 6
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β πΉ:ran (1st βπ
)βΆran (1st
βπ)) |
12 | 11 | 3expa 1119 |
. . . . 5
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β πΉ:ran (1st βπ
)βΆran (1st
βπ)) |
13 | 12 | 3adantl3 1169 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β πΉ:ran (1st βπ
)βΆran (1st
βπ)) |
14 | 13 | adantrr 716 |
. . 3
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β πΉ:ran (1st βπ
)βΆran (1st
βπ)) |
15 | | fco 6693 |
. . 3
β’ ((πΊ:ran (1st
βπ)βΆran
(1st βπ)
β§ πΉ:ran (1st
βπ
)βΆran
(1st βπ))
β (πΊ β πΉ):ran (1st
βπ
)βΆran
(1st βπ)) |
16 | 8, 14, 15 | syl2anc 585 |
. 2
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β (πΊ β πΉ):ran (1st βπ
)βΆran (1st
βπ)) |
17 | | eqid 2737 |
. . . . . . 7
β’
(2nd βπ
) = (2nd βπ
) |
18 | | eqid 2737 |
. . . . . . 7
β’
(GIdβ(2nd βπ
)) = (GIdβ(2nd βπ
)) |
19 | 10, 17, 18 | rngo1cl 36401 |
. . . . . 6
β’ (π
β RingOps β
(GIdβ(2nd βπ
)) β ran (1st βπ
)) |
20 | 19 | 3ad2ant1 1134 |
. . . . 5
β’ ((π
β RingOps β§ π β RingOps β§ π β RingOps) β
(GIdβ(2nd βπ
)) β ran (1st βπ
)) |
21 | 20 | adantr 482 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β (GIdβ(2nd
βπ
)) β ran
(1st βπ
)) |
22 | | fvco3 6941 |
. . . 4
β’ ((πΉ:ran (1st
βπ
)βΆran
(1st βπ)
β§ (GIdβ(2nd βπ
)) β ran (1st βπ
)) β ((πΊ β πΉ)β(GIdβ(2nd
βπ
))) = (πΊβ(πΉβ(GIdβ(2nd
βπ
))))) |
23 | 14, 21, 22 | syl2anc 585 |
. . 3
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β ((πΊ β πΉ)β(GIdβ(2nd
βπ
))) = (πΊβ(πΉβ(GIdβ(2nd
βπ
))))) |
24 | | eqid 2737 |
. . . . . . . . 9
β’
(2nd βπ) = (2nd βπ) |
25 | | eqid 2737 |
. . . . . . . . 9
β’
(GIdβ(2nd βπ)) = (GIdβ(2nd βπ)) |
26 | 17, 18, 24, 25 | rngohom1 36430 |
. . . . . . . 8
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ))) |
27 | 26 | 3expa 1119 |
. . . . . . 7
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β (πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ))) |
28 | 27 | 3adantl3 1169 |
. . . . . 6
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β (πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ))) |
29 | 28 | adantrr 716 |
. . . . 5
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β (πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ))) |
30 | 29 | fveq2d 6847 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β (πΊβ(πΉβ(GIdβ(2nd
βπ
)))) = (πΊβ(GIdβ(2nd
βπ)))) |
31 | | eqid 2737 |
. . . . . . . 8
β’
(2nd βπ) = (2nd βπ) |
32 | | eqid 2737 |
. . . . . . . 8
β’
(GIdβ(2nd βπ)) = (GIdβ(2nd βπ)) |
33 | 24, 25, 31, 32 | rngohom1 36430 |
. . . . . . 7
β’ ((π β RingOps β§ π β RingOps β§ πΊ β (π RngHom π)) β (πΊβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ))) |
34 | 33 | 3expa 1119 |
. . . . . 6
β’ (((π β RingOps β§ π β RingOps) β§ πΊ β (π RngHom π)) β (πΊβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ))) |
35 | 34 | 3adantl1 1167 |
. . . . 5
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΊ β (π RngHom π)) β (πΊβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ))) |
36 | 35 | adantrl 715 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β (πΊβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ))) |
37 | 30, 36 | eqtrd 2777 |
. . 3
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β (πΊβ(πΉβ(GIdβ(2nd
βπ
)))) =
(GIdβ(2nd βπ))) |
38 | 23, 37 | eqtrd 2777 |
. 2
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β ((πΊ β πΉ)β(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ))) |
39 | 9, 10, 1 | rngohomadd 36431 |
. . . . . . . . . . . 12
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΉβ(π₯(1st βπ
)π¦)) = ((πΉβπ₯)(1st βπ)(πΉβπ¦))) |
40 | 39 | ex 414 |
. . . . . . . . . . 11
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β (πΉβ(π₯(1st βπ
)π¦)) = ((πΉβπ₯)(1st βπ)(πΉβπ¦)))) |
41 | 40 | 3expa 1119 |
. . . . . . . . . 10
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β (πΉβ(π₯(1st βπ
)π¦)) = ((πΉβπ₯)(1st βπ)(πΉβπ¦)))) |
42 | 41 | 3adantl3 1169 |
. . . . . . . . 9
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β (πΉβ(π₯(1st βπ
)π¦)) = ((πΉβπ₯)(1st βπ)(πΉβπ¦)))) |
43 | 42 | imp 408 |
. . . . . . . 8
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΉβ(π₯(1st βπ
)π¦)) = ((πΉβπ₯)(1st βπ)(πΉβπ¦))) |
44 | 43 | adantlrr 720 |
. . . . . . 7
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΉβ(π₯(1st βπ
)π¦)) = ((πΉβπ₯)(1st βπ)(πΉβπ¦))) |
45 | 44 | fveq2d 6847 |
. . . . . 6
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΊβ(πΉβ(π₯(1st βπ
)π¦))) = (πΊβ((πΉβπ₯)(1st βπ)(πΉβπ¦)))) |
46 | 9, 10, 1, 2 | rngohomcl 36429 |
. . . . . . . . . . . . 13
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π₯ β ran (1st βπ
)) β (πΉβπ₯) β ran (1st βπ)) |
47 | 9, 10, 1, 2 | rngohomcl 36429 |
. . . . . . . . . . . . 13
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π¦ β ran (1st βπ
)) β (πΉβπ¦) β ran (1st βπ)) |
48 | 46, 47 | anim12dan 620 |
. . . . . . . . . . . 12
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ))) |
49 | 48 | ex 414 |
. . . . . . . . . . 11
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ)))) |
50 | 49 | 3expa 1119 |
. . . . . . . . . 10
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ)))) |
51 | 50 | 3adantl3 1169 |
. . . . . . . . 9
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ)))) |
52 | 51 | imp 408 |
. . . . . . . 8
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ))) |
53 | 52 | adantlrr 720 |
. . . . . . 7
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ))) |
54 | 1, 2, 3 | rngohomadd 36431 |
. . . . . . . . . . . 12
β’ (((π β RingOps β§ π β RingOps β§ πΊ β (π RngHom π)) β§ ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ))) β (πΊβ((πΉβπ₯)(1st βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(1st βπ)(πΊβ(πΉβπ¦)))) |
55 | 54 | ex 414 |
. . . . . . . . . . 11
β’ ((π β RingOps β§ π β RingOps β§ πΊ β (π RngHom π)) β (((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ)) β (πΊβ((πΉβπ₯)(1st βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(1st βπ)(πΊβ(πΉβπ¦))))) |
56 | 55 | 3expa 1119 |
. . . . . . . . . 10
β’ (((π β RingOps β§ π β RingOps) β§ πΊ β (π RngHom π)) β (((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ)) β (πΊβ((πΉβπ₯)(1st βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(1st βπ)(πΊβ(πΉβπ¦))))) |
57 | 56 | 3adantl1 1167 |
. . . . . . . . 9
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΊ β (π RngHom π)) β (((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ)) β (πΊβ((πΉβπ₯)(1st βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(1st βπ)(πΊβ(πΉβπ¦))))) |
58 | 57 | imp 408 |
. . . . . . . 8
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΊ β (π RngHom π)) β§ ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ))) β (πΊβ((πΉβπ₯)(1st βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(1st βπ)(πΊβ(πΉβπ¦)))) |
59 | 58 | adantlrl 719 |
. . . . . . 7
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ))) β (πΊβ((πΉβπ₯)(1st βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(1st βπ)(πΊβ(πΉβπ¦)))) |
60 | 53, 59 | syldan 592 |
. . . . . 6
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΊβ((πΉβπ₯)(1st βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(1st βπ)(πΊβ(πΉβπ¦)))) |
61 | 45, 60 | eqtrd 2777 |
. . . . 5
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΊβ(πΉβ(π₯(1st βπ
)π¦))) = ((πΊβ(πΉβπ₯))(1st βπ)(πΊβ(πΉβπ¦)))) |
62 | 9, 10 | rngogcl 36374 |
. . . . . . . . 9
β’ ((π
β RingOps β§ π₯ β ran (1st
βπ
) β§ π¦ β ran (1st
βπ
)) β (π₯(1st βπ
)π¦) β ran (1st βπ
)) |
63 | 62 | 3expb 1121 |
. . . . . . . 8
β’ ((π
β RingOps β§ (π₯ β ran (1st
βπ
) β§ π¦ β ran (1st
βπ
))) β (π₯(1st βπ
)π¦) β ran (1st βπ
)) |
64 | 63 | 3ad2antl1 1186 |
. . . . . . 7
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (π₯ β ran (1st
βπ
) β§ π¦ β ran (1st
βπ
))) β (π₯(1st βπ
)π¦) β ran (1st βπ
)) |
65 | 64 | adantlr 714 |
. . . . . 6
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (π₯(1st βπ
)π¦) β ran (1st βπ
)) |
66 | | fvco3 6941 |
. . . . . . 7
β’ ((πΉ:ran (1st
βπ
)βΆran
(1st βπ)
β§ (π₯(1st
βπ
)π¦) β ran (1st βπ
)) β ((πΊ β πΉ)β(π₯(1st βπ
)π¦)) = (πΊβ(πΉβ(π₯(1st βπ
)π¦)))) |
67 | 14, 66 | sylan 581 |
. . . . . 6
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯(1st βπ
)π¦) β ran (1st βπ
)) β ((πΊ β πΉ)β(π₯(1st βπ
)π¦)) = (πΊβ(πΉβ(π₯(1st βπ
)π¦)))) |
68 | 65, 67 | syldan 592 |
. . . . 5
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β ((πΊ β πΉ)β(π₯(1st βπ
)π¦)) = (πΊβ(πΉβ(π₯(1st βπ
)π¦)))) |
69 | | fvco3 6941 |
. . . . . . . 8
β’ ((πΉ:ran (1st
βπ
)βΆran
(1st βπ)
β§ π₯ β ran
(1st βπ
))
β ((πΊ β πΉ)βπ₯) = (πΊβ(πΉβπ₯))) |
70 | 14, 69 | sylan 581 |
. . . . . . 7
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ π₯ β ran (1st βπ
)) β ((πΊ β πΉ)βπ₯) = (πΊβ(πΉβπ₯))) |
71 | | fvco3 6941 |
. . . . . . . 8
β’ ((πΉ:ran (1st
βπ
)βΆran
(1st βπ)
β§ π¦ β ran
(1st βπ
))
β ((πΊ β πΉ)βπ¦) = (πΊβ(πΉβπ¦))) |
72 | 14, 71 | sylan 581 |
. . . . . . 7
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ π¦ β ran (1st βπ
)) β ((πΊ β πΉ)βπ¦) = (πΊβ(πΉβπ¦))) |
73 | 70, 72 | anim12dan 620 |
. . . . . 6
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (((πΊ β πΉ)βπ₯) = (πΊβ(πΉβπ₯)) β§ ((πΊ β πΉ)βπ¦) = (πΊβ(πΉβπ¦)))) |
74 | | oveq12 7367 |
. . . . . 6
β’ ((((πΊ β πΉ)βπ₯) = (πΊβ(πΉβπ₯)) β§ ((πΊ β πΉ)βπ¦) = (πΊβ(πΉβπ¦))) β (((πΊ β πΉ)βπ₯)(1st βπ)((πΊ β πΉ)βπ¦)) = ((πΊβ(πΉβπ₯))(1st βπ)(πΊβ(πΉβπ¦)))) |
75 | 73, 74 | syl 17 |
. . . . 5
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (((πΊ β πΉ)βπ₯)(1st βπ)((πΊ β πΉ)βπ¦)) = ((πΊβ(πΉβπ₯))(1st βπ)(πΊβ(πΉβπ¦)))) |
76 | 61, 68, 75 | 3eqtr4d 2787 |
. . . 4
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β ((πΊ β πΉ)β(π₯(1st βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(1st βπ)((πΊ β πΉ)βπ¦))) |
77 | 9, 10, 17, 24 | rngohommul 36432 |
. . . . . . . . . . . 12
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) |
78 | 77 | ex 414 |
. . . . . . . . . . 11
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦)))) |
79 | 78 | 3expa 1119 |
. . . . . . . . . 10
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦)))) |
80 | 79 | 3adantl3 1169 |
. . . . . . . . 9
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦)))) |
81 | 80 | imp 408 |
. . . . . . . 8
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) |
82 | 81 | adantlrr 720 |
. . . . . . 7
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΉβ(π₯(2nd βπ
)π¦)) = ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) |
83 | 82 | fveq2d 6847 |
. . . . . 6
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΊβ(πΉβ(π₯(2nd βπ
)π¦))) = (πΊβ((πΉβπ₯)(2nd βπ)(πΉβπ¦)))) |
84 | 1, 2, 24, 31 | rngohommul 36432 |
. . . . . . . . . . . 12
β’ (((π β RingOps β§ π β RingOps β§ πΊ β (π RngHom π)) β§ ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ))) β (πΊβ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(2nd βπ)(πΊβ(πΉβπ¦)))) |
85 | 84 | ex 414 |
. . . . . . . . . . 11
β’ ((π β RingOps β§ π β RingOps β§ πΊ β (π RngHom π)) β (((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ)) β (πΊβ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(2nd βπ)(πΊβ(πΉβπ¦))))) |
86 | 85 | 3expa 1119 |
. . . . . . . . . 10
β’ (((π β RingOps β§ π β RingOps) β§ πΊ β (π RngHom π)) β (((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ)) β (πΊβ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(2nd βπ)(πΊβ(πΉβπ¦))))) |
87 | 86 | 3adantl1 1167 |
. . . . . . . . 9
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΊ β (π RngHom π)) β (((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ)) β (πΊβ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(2nd βπ)(πΊβ(πΉβπ¦))))) |
88 | 87 | imp 408 |
. . . . . . . 8
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ πΊ β (π RngHom π)) β§ ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ))) β (πΊβ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(2nd βπ)(πΊβ(πΉβπ¦)))) |
89 | 88 | adantlrl 719 |
. . . . . . 7
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ ((πΉβπ₯) β ran (1st βπ) β§ (πΉβπ¦) β ran (1st βπ))) β (πΊβ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(2nd βπ)(πΊβ(πΉβπ¦)))) |
90 | 53, 89 | syldan 592 |
. . . . . 6
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΊβ((πΉβπ₯)(2nd βπ)(πΉβπ¦))) = ((πΊβ(πΉβπ₯))(2nd βπ)(πΊβ(πΉβπ¦)))) |
91 | 83, 90 | eqtrd 2777 |
. . . . 5
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΊβ(πΉβ(π₯(2nd βπ
)π¦))) = ((πΊβ(πΉβπ₯))(2nd βπ)(πΊβ(πΉβπ¦)))) |
92 | 9, 17, 10 | rngocl 36363 |
. . . . . . . . 9
β’ ((π
β RingOps β§ π₯ β ran (1st
βπ
) β§ π¦ β ran (1st
βπ
)) β (π₯(2nd βπ
)π¦) β ran (1st βπ
)) |
93 | 92 | 3expb 1121 |
. . . . . . . 8
β’ ((π
β RingOps β§ (π₯ β ran (1st
βπ
) β§ π¦ β ran (1st
βπ
))) β (π₯(2nd βπ
)π¦) β ran (1st βπ
)) |
94 | 93 | 3ad2antl1 1186 |
. . . . . . 7
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (π₯ β ran (1st
βπ
) β§ π¦ β ran (1st
βπ
))) β (π₯(2nd βπ
)π¦) β ran (1st βπ
)) |
95 | 94 | adantlr 714 |
. . . . . 6
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (π₯(2nd βπ
)π¦) β ran (1st βπ
)) |
96 | | fvco3 6941 |
. . . . . . 7
β’ ((πΉ:ran (1st
βπ
)βΆran
(1st βπ)
β§ (π₯(2nd
βπ
)π¦) β ran (1st βπ
)) β ((πΊ β πΉ)β(π₯(2nd βπ
)π¦)) = (πΊβ(πΉβ(π₯(2nd βπ
)π¦)))) |
97 | 14, 96 | sylan 581 |
. . . . . 6
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯(2nd βπ
)π¦) β ran (1st βπ
)) β ((πΊ β πΉ)β(π₯(2nd βπ
)π¦)) = (πΊβ(πΉβ(π₯(2nd βπ
)π¦)))) |
98 | 95, 97 | syldan 592 |
. . . . 5
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β ((πΊ β πΉ)β(π₯(2nd βπ
)π¦)) = (πΊβ(πΉβ(π₯(2nd βπ
)π¦)))) |
99 | | oveq12 7367 |
. . . . . 6
β’ ((((πΊ β πΉ)βπ₯) = (πΊβ(πΉβπ₯)) β§ ((πΊ β πΉ)βπ¦) = (πΊβ(πΉβπ¦))) β (((πΊ β πΉ)βπ₯)(2nd βπ)((πΊ β πΉ)βπ¦)) = ((πΊβ(πΉβπ₯))(2nd βπ)(πΊβ(πΉβπ¦)))) |
100 | 73, 99 | syl 17 |
. . . . 5
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (((πΊ β πΉ)βπ₯)(2nd βπ)((πΊ β πΉ)βπ¦)) = ((πΊβ(πΉβπ₯))(2nd βπ)(πΊβ(πΉβπ¦)))) |
101 | 91, 98, 100 | 3eqtr4d 2787 |
. . . 4
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β ((πΊ β πΉ)β(π₯(2nd βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(2nd βπ)((πΊ β πΉ)βπ¦))) |
102 | 76, 101 | jca 513 |
. . 3
β’ ((((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (((πΊ β πΉ)β(π₯(1st βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(1st βπ)((πΊ β πΉ)βπ¦)) β§ ((πΊ β πΉ)β(π₯(2nd βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(2nd βπ)((πΊ β πΉ)βπ¦)))) |
103 | 102 | ralrimivva 3198 |
. 2
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β βπ₯ β ran (1st βπ
)βπ¦ β ran (1st βπ
)(((πΊ β πΉ)β(π₯(1st βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(1st βπ)((πΊ β πΉ)βπ¦)) β§ ((πΊ β πΉ)β(π₯(2nd βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(2nd βπ)((πΊ β πΉ)βπ¦)))) |
104 | 9, 17, 10, 18, 3, 31, 4, 32 | isrngohom 36427 |
. . . 4
β’ ((π
β RingOps β§ π β RingOps) β ((πΊ β πΉ) β (π
RngHom π) β ((πΊ β πΉ):ran (1st βπ
)βΆran (1st
βπ) β§ ((πΊ β πΉ)β(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ)) β§ βπ₯ β ran (1st βπ
)βπ¦ β ran (1st βπ
)(((πΊ β πΉ)β(π₯(1st βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(1st βπ)((πΊ β πΉ)βπ¦)) β§ ((πΊ β πΉ)β(π₯(2nd βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(2nd βπ)((πΊ β πΉ)βπ¦)))))) |
105 | 104 | 3adant2 1132 |
. . 3
β’ ((π
β RingOps β§ π β RingOps β§ π β RingOps) β ((πΊ β πΉ) β (π
RngHom π) β ((πΊ β πΉ):ran (1st βπ
)βΆran (1st
βπ) β§ ((πΊ β πΉ)β(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ)) β§ βπ₯ β ran (1st βπ
)βπ¦ β ran (1st βπ
)(((πΊ β πΉ)β(π₯(1st βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(1st βπ)((πΊ β πΉ)βπ¦)) β§ ((πΊ β πΉ)β(π₯(2nd βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(2nd βπ)((πΊ β πΉ)βπ¦)))))) |
106 | 105 | adantr 482 |
. 2
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β ((πΊ β πΉ) β (π
RngHom π) β ((πΊ β πΉ):ran (1st βπ
)βΆran (1st
βπ) β§ ((πΊ β πΉ)β(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ)) β§ βπ₯ β ran (1st βπ
)βπ¦ β ran (1st βπ
)(((πΊ β πΉ)β(π₯(1st βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(1st βπ)((πΊ β πΉ)βπ¦)) β§ ((πΊ β πΉ)β(π₯(2nd βπ
)π¦)) = (((πΊ β πΉ)βπ₯)(2nd βπ)((πΊ β πΉ)βπ¦)))))) |
107 | 16, 38, 103, 106 | mpbir3and 1343 |
1
β’ (((π
β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΊ β (π RngHom π))) β (πΊ β πΉ) β (π
RngHom π)) |