Step | Hyp | Ref
| Expression |
1 | | f1ocnv 6797 |
. . . . . . . 8
β’ (πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β β‘πΉ:ran (1st βπ)β1-1-ontoβran
(1st βπ
)) |
2 | | f1of 6785 |
. . . . . . . 8
β’ (β‘πΉ:ran (1st βπ)β1-1-ontoβran
(1st βπ
)
β β‘πΉ:ran (1st βπ)βΆran (1st
βπ
)) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ (πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β β‘πΉ:ran (1st βπ)βΆran (1st
βπ
)) |
4 | 3 | ad2antll 728 |
. . . . . 6
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β β‘πΉ:ran (1st βπ)βΆran (1st
βπ
)) |
5 | | eqid 2737 |
. . . . . . . . . 10
β’
(2nd βπ
) = (2nd βπ
) |
6 | | eqid 2737 |
. . . . . . . . . 10
β’
(GIdβ(2nd βπ
)) = (GIdβ(2nd βπ
)) |
7 | | eqid 2737 |
. . . . . . . . . 10
β’
(2nd βπ) = (2nd βπ) |
8 | | eqid 2737 |
. . . . . . . . . 10
β’
(GIdβ(2nd βπ)) = (GIdβ(2nd βπ)) |
9 | 5, 6, 7, 8 | rngohom1 36430 |
. . . . . . . . 9
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ))) |
10 | 9 | 3expa 1119 |
. . . . . . . 8
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β (πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ))) |
11 | 10 | adantrr 716 |
. . . . . . 7
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β (πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ))) |
12 | | eqid 2737 |
. . . . . . . . . . 11
β’ ran
(1st βπ
) =
ran (1st βπ
) |
13 | 12, 5, 6 | rngo1cl 36401 |
. . . . . . . . . 10
β’ (π
β RingOps β
(GIdβ(2nd βπ
)) β ran (1st βπ
)) |
14 | | f1ocnvfv 7225 |
. . . . . . . . . 10
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (GIdβ(2nd
βπ
)) β ran
(1st βπ
))
β ((πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ)) β (β‘πΉβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ
)))) |
15 | 13, 14 | sylan2 594 |
. . . . . . . . 9
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ π
β RingOps) β ((πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ)) β (β‘πΉβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ
)))) |
16 | 15 | ancoms 460 |
. . . . . . . 8
β’ ((π
β RingOps β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β ((πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ)) β (β‘πΉβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ
)))) |
17 | 16 | ad2ant2rl 748 |
. . . . . . 7
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β ((πΉβ(GIdβ(2nd
βπ
))) =
(GIdβ(2nd βπ)) β (β‘πΉβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ
)))) |
18 | 11, 17 | mpd 15 |
. . . . . 6
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β (β‘πΉβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ
))) |
19 | | f1ocnvfv2 7224 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ π₯ β ran (1st βπ)) β (πΉβ(β‘πΉβπ₯)) = π₯) |
20 | | f1ocnvfv2 7224 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ π¦ β ran (1st βπ)) β (πΉβ(β‘πΉβπ¦)) = π¦) |
21 | 19, 20 | anim12dan 620 |
. . . . . . . . . . . . 13
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β ((πΉβ(β‘πΉβπ₯)) = π₯ β§ (πΉβ(β‘πΉβπ¦)) = π¦)) |
22 | | oveq12 7367 |
. . . . . . . . . . . . 13
β’ (((πΉβ(β‘πΉβπ₯)) = π₯ β§ (πΉβ(β‘πΉβπ¦)) = π¦) β ((πΉβ(β‘πΉβπ₯))(1st βπ)(πΉβ(β‘πΉβπ¦))) = (π₯(1st βπ)π¦)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β ((πΉβ(β‘πΉβπ₯))(1st βπ)(πΉβ(β‘πΉβπ¦))) = (π₯(1st βπ)π¦)) |
24 | 23 | adantll 713 |
. . . . . . . . . . 11
β’ (((πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β ((πΉβ(β‘πΉβπ₯))(1st βπ)(πΉβ(β‘πΉβπ¦))) = (π₯(1st βπ)π¦)) |
25 | 24 | adantll 713 |
. . . . . . . . . 10
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β ((πΉβ(β‘πΉβπ₯))(1st βπ)(πΉβ(β‘πΉβπ¦))) = (π₯(1st βπ)π¦)) |
26 | | f1ocnvdm 7232 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ π₯ β ran (1st βπ)) β (β‘πΉβπ₯) β ran (1st βπ
)) |
27 | | f1ocnvdm 7232 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ π¦ β ran (1st βπ)) β (β‘πΉβπ¦) β ran (1st βπ
)) |
28 | 26, 27 | anim12dan 620 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β ((β‘πΉβπ₯) β ran (1st βπ
) β§ (β‘πΉβπ¦) β ran (1st βπ
))) |
29 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(1st βπ
) = (1st βπ
) |
30 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(1st βπ) = (1st βπ) |
31 | 29, 12, 30 | rngohomadd 36431 |
. . . . . . . . . . . . . . 15
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ ((β‘πΉβπ₯) β ran (1st βπ
) β§ (β‘πΉβπ¦) β ran (1st βπ
))) β (πΉβ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(1st βπ)(πΉβ(β‘πΉβπ¦)))) |
32 | 28, 31 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))) β (πΉβ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(1st βπ)(πΉβ(β‘πΉβπ¦)))) |
33 | 32 | exp32 422 |
. . . . . . . . . . . . 13
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)
β ((π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ))
β (πΉβ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(1st βπ)(πΉβ(β‘πΉβπ¦)))))) |
34 | 33 | 3expa 1119 |
. . . . . . . . . . . 12
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β (πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)
β ((π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ))
β (πΉβ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(1st βπ)(πΉβ(β‘πΉβπ¦)))))) |
35 | 34 | impr 456 |
. . . . . . . . . . 11
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β ((π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ))
β (πΉβ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(1st βπ)(πΉβ(β‘πΉβπ¦))))) |
36 | 35 | imp 408 |
. . . . . . . . . 10
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β (πΉβ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(1st βπ)(πΉβ(β‘πΉβπ¦)))) |
37 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ ran
(1st βπ) =
ran (1st βπ) |
38 | 30, 37 | rngogcl 36374 |
. . . . . . . . . . . . . . 15
β’ ((π β RingOps β§ π₯ β ran (1st
βπ) β§ π¦ β ran (1st
βπ)) β (π₯(1st βπ)π¦) β ran (1st βπ)) |
39 | 38 | 3expb 1121 |
. . . . . . . . . . . . . 14
β’ ((π β RingOps β§ (π₯ β ran (1st
βπ) β§ π¦ β ran (1st
βπ))) β (π₯(1st βπ)π¦) β ran (1st βπ)) |
40 | | f1ocnvfv2 7224 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (π₯(1st βπ)π¦) β ran (1st βπ)) β (πΉβ(β‘πΉβ(π₯(1st βπ)π¦))) = (π₯(1st βπ)π¦)) |
41 | 40 | ancoms 460 |
. . . . . . . . . . . . . 14
β’ (((π₯(1st βπ)π¦) β ran (1st βπ) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ))
β (πΉβ(β‘πΉβ(π₯(1st βπ)π¦))) = (π₯(1st βπ)π¦)) |
42 | 39, 41 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β RingOps β§ (π₯ β ran (1st
βπ) β§ π¦ β ran (1st
βπ))) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β (πΉβ(β‘πΉβ(π₯(1st βπ)π¦))) = (π₯(1st βπ)π¦)) |
43 | 42 | an32s 651 |
. . . . . . . . . . . 12
β’ (((π β RingOps β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β (πΉβ(β‘πΉβ(π₯(1st βπ)π¦))) = (π₯(1st βπ)π¦)) |
44 | 43 | adantlll 717 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β (πΉβ(β‘πΉβ(π₯(1st βπ)π¦))) = (π₯(1st βπ)π¦)) |
45 | 44 | adantlrl 719 |
. . . . . . . . . 10
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β (πΉβ(β‘πΉβ(π₯(1st βπ)π¦))) = (π₯(1st βπ)π¦)) |
46 | 25, 36, 45 | 3eqtr4rd 2788 |
. . . . . . . . 9
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β (πΉβ(β‘πΉβ(π₯(1st βπ)π¦))) = (πΉβ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)))) |
47 | | f1of1 6784 |
. . . . . . . . . . . 12
β’ (πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β πΉ:ran (1st βπ
)β1-1βran (1st βπ)) |
48 | 47 | ad2antlr 726 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β πΉ:ran (1st βπ
)β1-1βran (1st βπ)) |
49 | | f1ocnvdm 7232 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (π₯(1st βπ)π¦) β ran (1st βπ)) β (β‘πΉβ(π₯(1st βπ)π¦)) β ran (1st βπ
)) |
50 | 49 | ancoms 460 |
. . . . . . . . . . . . . 14
β’ (((π₯(1st βπ)π¦) β ran (1st βπ) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ))
β (β‘πΉβ(π₯(1st βπ)π¦)) β ran (1st βπ
)) |
51 | 39, 50 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β RingOps β§ (π₯ β ran (1st
βπ) β§ π¦ β ran (1st
βπ))) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β (β‘πΉβ(π₯(1st βπ)π¦)) β ran (1st βπ
)) |
52 | 51 | an32s 651 |
. . . . . . . . . . . 12
β’ (((π β RingOps β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β (β‘πΉβ(π₯(1st βπ)π¦)) β ran (1st βπ
)) |
53 | 52 | adantlll 717 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β (β‘πΉβ(π₯(1st βπ)π¦)) β ran (1st βπ
)) |
54 | 29, 12 | rngogcl 36374 |
. . . . . . . . . . . . . . 15
β’ ((π
β RingOps β§ (β‘πΉβπ₯) β ran (1st βπ
) β§ (β‘πΉβπ¦) β ran (1st βπ
)) β ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β ran (1st βπ
)) |
55 | 54 | 3expb 1121 |
. . . . . . . . . . . . . 14
β’ ((π
β RingOps β§ ((β‘πΉβπ₯) β ran (1st βπ
) β§ (β‘πΉβπ¦) β ran (1st βπ
))) β ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β ran (1st βπ
)) |
56 | 28, 55 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π
β RingOps β§ (πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ)))) β ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β ran (1st βπ
)) |
57 | 56 | anassrs 469 |
. . . . . . . . . . . 12
β’ (((π
β RingOps β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β ran (1st βπ
)) |
58 | 57 | adantllr 718 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β ran (1st βπ
)) |
59 | | f1fveq 7210 |
. . . . . . . . . . 11
β’ ((πΉ:ran (1st
βπ
)β1-1βran (1st βπ) β§ ((β‘πΉβ(π₯(1st βπ)π¦)) β ran (1st βπ
) β§ ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β ran (1st βπ
))) β ((πΉβ(β‘πΉβ(π₯(1st βπ)π¦))) = (πΉβ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦))) β (β‘πΉβ(π₯(1st βπ)π¦)) = ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)))) |
60 | 48, 53, 58, 59 | syl12anc 836 |
. . . . . . . . . 10
β’ ((((π
β RingOps β§ π β RingOps) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β ((πΉβ(β‘πΉβ(π₯(1st βπ)π¦))) = (πΉβ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦))) β (β‘πΉβ(π₯(1st βπ)π¦)) = ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)))) |
61 | 60 | adantlrl 719 |
. . . . . . . . 9
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β ((πΉβ(β‘πΉβ(π₯(1st βπ)π¦))) = (πΉβ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦))) β (β‘πΉβ(π₯(1st βπ)π¦)) = ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)))) |
62 | 46, 61 | mpbid 231 |
. . . . . . . 8
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β (β‘πΉβ(π₯(1st βπ)π¦)) = ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦))) |
63 | | oveq12 7367 |
. . . . . . . . . . . . 13
β’ (((πΉβ(β‘πΉβπ₯)) = π₯ β§ (πΉβ(β‘πΉβπ¦)) = π¦) β ((πΉβ(β‘πΉβπ₯))(2nd βπ)(πΉβ(β‘πΉβπ¦))) = (π₯(2nd βπ)π¦)) |
64 | 21, 63 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β ((πΉβ(β‘πΉβπ₯))(2nd βπ)(πΉβ(β‘πΉβπ¦))) = (π₯(2nd βπ)π¦)) |
65 | 64 | adantll 713 |
. . . . . . . . . . 11
β’ (((πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β ((πΉβ(β‘πΉβπ₯))(2nd βπ)(πΉβ(β‘πΉβπ¦))) = (π₯(2nd βπ)π¦)) |
66 | 65 | adantll 713 |
. . . . . . . . . 10
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β ((πΉβ(β‘πΉβπ₯))(2nd βπ)(πΉβ(β‘πΉβπ¦))) = (π₯(2nd βπ)π¦)) |
67 | 29, 12, 5, 7 | rngohommul 36432 |
. . . . . . . . . . . . . . 15
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ ((β‘πΉβπ₯) β ran (1st βπ
) β§ (β‘πΉβπ¦) β ran (1st βπ
))) β (πΉβ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(2nd βπ)(πΉβ(β‘πΉβπ¦)))) |
68 | 28, 67 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))) β (πΉβ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(2nd βπ)(πΉβ(β‘πΉβπ¦)))) |
69 | 68 | exp32 422 |
. . . . . . . . . . . . 13
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)
β ((π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ))
β (πΉβ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(2nd βπ)(πΉβ(β‘πΉβπ¦)))))) |
70 | 69 | 3expa 1119 |
. . . . . . . . . . . 12
β’ (((π
β RingOps β§ π β RingOps) β§ πΉ β (π
RngHom π)) β (πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)
β ((π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ))
β (πΉβ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(2nd βπ)(πΉβ(β‘πΉβπ¦)))))) |
71 | 70 | impr 456 |
. . . . . . . . . . 11
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β ((π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ))
β (πΉβ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(2nd βπ)(πΉβ(β‘πΉβπ¦))))) |
72 | 71 | imp 408 |
. . . . . . . . . 10
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β (πΉβ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦))) = ((πΉβ(β‘πΉβπ₯))(2nd βπ)(πΉβ(β‘πΉβπ¦)))) |
73 | 30, 7, 37 | rngocl 36363 |
. . . . . . . . . . . . . . 15
β’ ((π β RingOps β§ π₯ β ran (1st
βπ) β§ π¦ β ran (1st
βπ)) β (π₯(2nd βπ)π¦) β ran (1st βπ)) |
74 | 73 | 3expb 1121 |
. . . . . . . . . . . . . 14
β’ ((π β RingOps β§ (π₯ β ran (1st
βπ) β§ π¦ β ran (1st
βπ))) β (π₯(2nd βπ)π¦) β ran (1st βπ)) |
75 | | f1ocnvfv2 7224 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (π₯(2nd βπ)π¦) β ran (1st βπ)) β (πΉβ(β‘πΉβ(π₯(2nd βπ)π¦))) = (π₯(2nd βπ)π¦)) |
76 | 75 | ancoms 460 |
. . . . . . . . . . . . . 14
β’ (((π₯(2nd βπ)π¦) β ran (1st βπ) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ))
β (πΉβ(β‘πΉβ(π₯(2nd βπ)π¦))) = (π₯(2nd βπ)π¦)) |
77 | 74, 76 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β RingOps β§ (π₯ β ran (1st
βπ) β§ π¦ β ran (1st
βπ))) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β (πΉβ(β‘πΉβ(π₯(2nd βπ)π¦))) = (π₯(2nd βπ)π¦)) |
78 | 77 | an32s 651 |
. . . . . . . . . . . 12
β’ (((π β RingOps β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β (πΉβ(β‘πΉβ(π₯(2nd βπ)π¦))) = (π₯(2nd βπ)π¦)) |
79 | 78 | adantlll 717 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β (πΉβ(β‘πΉβ(π₯(2nd βπ)π¦))) = (π₯(2nd βπ)π¦)) |
80 | 79 | adantlrl 719 |
. . . . . . . . . 10
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β (πΉβ(β‘πΉβ(π₯(2nd βπ)π¦))) = (π₯(2nd βπ)π¦)) |
81 | 66, 72, 80 | 3eqtr4rd 2788 |
. . . . . . . . 9
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β (πΉβ(β‘πΉβ(π₯(2nd βπ)π¦))) = (πΉβ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)))) |
82 | | f1ocnvdm 7232 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (π₯(2nd βπ)π¦) β ran (1st βπ)) β (β‘πΉβ(π₯(2nd βπ)π¦)) β ran (1st βπ
)) |
83 | 82 | ancoms 460 |
. . . . . . . . . . . . . 14
β’ (((π₯(2nd βπ)π¦) β ran (1st βπ) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ))
β (β‘πΉβ(π₯(2nd βπ)π¦)) β ran (1st βπ
)) |
84 | 74, 83 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β RingOps β§ (π₯ β ran (1st
βπ) β§ π¦ β ran (1st
βπ))) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β (β‘πΉβ(π₯(2nd βπ)π¦)) β ran (1st βπ
)) |
85 | 84 | an32s 651 |
. . . . . . . . . . . 12
β’ (((π β RingOps β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β (β‘πΉβ(π₯(2nd βπ)π¦)) β ran (1st βπ
)) |
86 | 85 | adantlll 717 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β (β‘πΉβ(π₯(2nd βπ)π¦)) β ran (1st βπ
)) |
87 | 29, 5, 12 | rngocl 36363 |
. . . . . . . . . . . . . . 15
β’ ((π
β RingOps β§ (β‘πΉβπ₯) β ran (1st βπ
) β§ (β‘πΉβπ¦) β ran (1st βπ
)) β ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)) β ran (1st βπ
)) |
88 | 87 | 3expb 1121 |
. . . . . . . . . . . . . 14
β’ ((π
β RingOps β§ ((β‘πΉβπ₯) β ran (1st βπ
) β§ (β‘πΉβπ¦) β ran (1st βπ
))) β ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)) β ran (1st βπ
)) |
89 | 28, 88 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π
β RingOps β§ (πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ)))) β ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)) β ran (1st βπ
)) |
90 | 89 | anassrs 469 |
. . . . . . . . . . . 12
β’ (((π
β RingOps β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)) β ran (1st βπ
)) |
91 | 90 | adantllr 718 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)) β ran (1st βπ
)) |
92 | | f1fveq 7210 |
. . . . . . . . . . 11
β’ ((πΉ:ran (1st
βπ
)β1-1βran (1st βπ) β§ ((β‘πΉβ(π₯(2nd βπ)π¦)) β ran (1st βπ
) β§ ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)) β ran (1st βπ
))) β ((πΉβ(β‘πΉβ(π₯(2nd βπ)π¦))) = (πΉβ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦))) β (β‘πΉβ(π₯(2nd βπ)π¦)) = ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)))) |
93 | 48, 86, 91, 92 | syl12anc 836 |
. . . . . . . . . 10
β’ ((((π
β RingOps β§ π β RingOps) β§ πΉ:ran (1st
βπ
)β1-1-ontoβran (1st βπ)) β§ (π₯ β ran (1st βπ) β§ π¦ β ran (1st βπ))) β ((πΉβ(β‘πΉβ(π₯(2nd βπ)π¦))) = (πΉβ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦))) β (β‘πΉβ(π₯(2nd βπ)π¦)) = ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)))) |
94 | 93 | adantlrl 719 |
. . . . . . . . 9
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β ((πΉβ(β‘πΉβ(π₯(2nd βπ)π¦))) = (πΉβ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦))) β (β‘πΉβ(π₯(2nd βπ)π¦)) = ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)))) |
95 | 81, 94 | mpbid 231 |
. . . . . . . 8
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β (β‘πΉβ(π₯(2nd βπ)π¦)) = ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦))) |
96 | 62, 95 | jca 513 |
. . . . . . 7
β’ ((((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β§ (π₯ β ran
(1st βπ)
β§ π¦ β ran
(1st βπ)))
β ((β‘πΉβ(π₯(1st βπ)π¦)) = ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β§ (β‘πΉβ(π₯(2nd βπ)π¦)) = ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)))) |
97 | 96 | ralrimivva 3198 |
. . . . . 6
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β βπ₯ β ran
(1st βπ)βπ¦ β ran (1st βπ)((β‘πΉβ(π₯(1st βπ)π¦)) = ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β§ (β‘πΉβ(π₯(2nd βπ)π¦)) = ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)))) |
98 | 30, 7, 37, 8, 29, 5, 12, 6 | isrngohom 36427 |
. . . . . . . 8
β’ ((π β RingOps β§ π
β RingOps) β (β‘πΉ β (π RngHom π
) β (β‘πΉ:ran (1st βπ)βΆran (1st
βπ
) β§ (β‘πΉβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ
)) β§ βπ₯ β ran (1st βπ)βπ¦ β ran (1st βπ)((β‘πΉβ(π₯(1st βπ)π¦)) = ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β§ (β‘πΉβ(π₯(2nd βπ)π¦)) = ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)))))) |
99 | 98 | ancoms 460 |
. . . . . . 7
β’ ((π
β RingOps β§ π β RingOps) β (β‘πΉ β (π RngHom π
) β (β‘πΉ:ran (1st βπ)βΆran (1st
βπ
) β§ (β‘πΉβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ
)) β§ βπ₯ β ran (1st βπ)βπ¦ β ran (1st βπ)((β‘πΉβ(π₯(1st βπ)π¦)) = ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β§ (β‘πΉβ(π₯(2nd βπ)π¦)) = ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)))))) |
100 | 99 | adantr 482 |
. . . . . 6
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β (β‘πΉ β (π RngHom π
) β (β‘πΉ:ran (1st βπ)βΆran (1st
βπ
) β§ (β‘πΉβ(GIdβ(2nd
βπ))) =
(GIdβ(2nd βπ
)) β§ βπ₯ β ran (1st βπ)βπ¦ β ran (1st βπ)((β‘πΉβ(π₯(1st βπ)π¦)) = ((β‘πΉβπ₯)(1st βπ
)(β‘πΉβπ¦)) β§ (β‘πΉβ(π₯(2nd βπ)π¦)) = ((β‘πΉβπ₯)(2nd βπ
)(β‘πΉβπ¦)))))) |
101 | 4, 18, 97, 100 | mpbir3and 1343 |
. . . . 5
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β β‘πΉ β (π RngHom π
)) |
102 | 1 | ad2antll 728 |
. . . . 5
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β β‘πΉ:ran (1st βπ)β1-1-ontoβran
(1st βπ
)) |
103 | 101, 102 | jca 513 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps) β§ (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))
β (β‘πΉ β (π RngHom π
) β§ β‘πΉ:ran (1st βπ)β1-1-ontoβran
(1st βπ
))) |
104 | 103 | ex 414 |
. . 3
β’ ((π
β RingOps β§ π β RingOps) β ((πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ))
β (β‘πΉ β (π RngHom π
) β§ β‘πΉ:ran (1st βπ)β1-1-ontoβran
(1st βπ
)))) |
105 | 29, 12, 30, 37 | isrngoiso 36440 |
. . 3
β’ ((π
β RingOps β§ π β RingOps) β (πΉ β (π
RngIso π) β (πΉ β (π
RngHom π) β§ πΉ:ran (1st βπ
)β1-1-ontoβran
(1st βπ)))) |
106 | 30, 37, 29, 12 | isrngoiso 36440 |
. . . 4
β’ ((π β RingOps β§ π
β RingOps) β (β‘πΉ β (π RngIso π
) β (β‘πΉ β (π RngHom π
) β§ β‘πΉ:ran (1st βπ)β1-1-ontoβran
(1st βπ
)))) |
107 | 106 | ancoms 460 |
. . 3
β’ ((π
β RingOps β§ π β RingOps) β (β‘πΉ β (π RngIso π
) β (β‘πΉ β (π RngHom π
) β§ β‘πΉ:ran (1st βπ)β1-1-ontoβran
(1st βπ
)))) |
108 | 104, 105,
107 | 3imtr4d 294 |
. 2
β’ ((π
β RingOps β§ π β RingOps) β (πΉ β (π
RngIso π) β β‘πΉ β (π RngIso π
))) |
109 | 108 | 3impia 1118 |
1
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngIso π)) β β‘πΉ β (π RngIso π
)) |