Step | Hyp | Ref
| Expression |
1 | | cnvimass 6034 |
. . 3
β’ (β‘πΉ β {π}) β dom πΉ |
2 | | eqid 2737 |
. . . 4
β’
(1st βπ
) = (1st βπ
) |
3 | | eqid 2737 |
. . . 4
β’ ran
(1st βπ
) =
ran (1st βπ
) |
4 | | keridl.1 |
. . . 4
β’ πΊ = (1st βπ) |
5 | | eqid 2737 |
. . . 4
β’ ran πΊ = ran πΊ |
6 | 2, 3, 4, 5 | rngohomf 36428 |
. . 3
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β πΉ:ran (1st βπ
)βΆran πΊ) |
7 | 1, 6 | fssdm 6689 |
. 2
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (β‘πΉ β {π}) β ran (1st βπ
)) |
8 | | eqid 2737 |
. . . . 5
β’
(GIdβ(1st βπ
)) = (GIdβ(1st βπ
)) |
9 | 2, 3, 8 | rngo0cl 36381 |
. . . 4
β’ (π
β RingOps β
(GIdβ(1st βπ
)) β ran (1st βπ
)) |
10 | 9 | 3ad2ant1 1134 |
. . 3
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (GIdβ(1st
βπ
)) β ran
(1st βπ
)) |
11 | | keridl.2 |
. . . . 5
β’ π = (GIdβπΊ) |
12 | 2, 8, 4, 11 | rngohom0 36434 |
. . . 4
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (πΉβ(GIdβ(1st
βπ
))) = π) |
13 | | fvex 6856 |
. . . . 5
β’ (πΉβ(GIdβ(1st
βπ
))) β
V |
14 | 13 | elsn 4602 |
. . . 4
β’ ((πΉβ(GIdβ(1st
βπ
))) β {π} β (πΉβ(GIdβ(1st
βπ
))) = π) |
15 | 12, 14 | sylibr 233 |
. . 3
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (πΉβ(GIdβ(1st
βπ
))) β {π}) |
16 | | ffn 6669 |
. . . 4
β’ (πΉ:ran (1st
βπ
)βΆran πΊ β πΉ Fn ran (1st βπ
)) |
17 | | elpreima 7009 |
. . . 4
β’ (πΉ Fn ran (1st
βπ
) β
((GIdβ(1st βπ
)) β (β‘πΉ β {π}) β ((GIdβ(1st
βπ
)) β ran
(1st βπ
)
β§ (πΉβ(GIdβ(1st
βπ
))) β {π}))) |
18 | 6, 16, 17 | 3syl 18 |
. . 3
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((GIdβ(1st
βπ
)) β (β‘πΉ β {π}) β ((GIdβ(1st
βπ
)) β ran
(1st βπ
)
β§ (πΉβ(GIdβ(1st
βπ
))) β {π}))) |
19 | 10, 15, 18 | mpbir2and 712 |
. 2
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (GIdβ(1st
βπ
)) β (β‘πΉ β {π})) |
20 | | an4 655 |
. . . . . . . 8
β’ (((π₯ β ran (1st
βπ
) β§ (πΉβπ₯) β {π}) β§ (π¦ β ran (1st βπ
) β§ (πΉβπ¦) β {π})) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β§ ((πΉβπ₯) β {π} β§ (πΉβπ¦) β {π}))) |
21 | 2, 3, 4 | rngohomadd 36431 |
. . . . . . . . . . . . . 14
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (πΉβ(π₯(1st βπ
)π¦)) = ((πΉβπ₯)πΊ(πΉβπ¦))) |
22 | 21 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β§ ((πΉβπ₯) = π β§ (πΉβπ¦) = π)) β (πΉβ(π₯(1st βπ
)π¦)) = ((πΉβπ₯)πΊ(πΉβπ¦))) |
23 | | oveq12 7367 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ₯) = π β§ (πΉβπ¦) = π) β ((πΉβπ₯)πΊ(πΉβπ¦)) = (ππΊπ)) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β§ ((πΉβπ₯) = π β§ (πΉβπ¦) = π)) β ((πΉβπ₯)πΊ(πΉβπ¦)) = (ππΊπ)) |
25 | 4 | rngogrpo 36372 |
. . . . . . . . . . . . . . . 16
β’ (π β RingOps β πΊ β GrpOp) |
26 | 5, 11 | grpoidcl 29459 |
. . . . . . . . . . . . . . . 16
β’ (πΊ β GrpOp β π β ran πΊ) |
27 | 5, 11 | grpolid 29461 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β GrpOp β§ π β ran πΊ) β (ππΊπ) = π) |
28 | 25, 26, 27 | syl2anc2 586 |
. . . . . . . . . . . . . . 15
β’ (π β RingOps β (ππΊπ) = π) |
29 | 28 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (ππΊπ) = π) |
30 | 29 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β§ ((πΉβπ₯) = π β§ (πΉβπ¦) = π)) β (ππΊπ) = π) |
31 | 22, 24, 30 | 3eqtrd 2781 |
. . . . . . . . . . . 12
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β§ ((πΉβπ₯) = π β§ (πΉβπ¦) = π)) β (πΉβ(π₯(1st βπ
)π¦)) = π) |
32 | 31 | ex 414 |
. . . . . . . . . . 11
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (((πΉβπ₯) = π β§ (πΉβπ¦) = π) β (πΉβ(π₯(1st βπ
)π¦)) = π)) |
33 | | fvex 6856 |
. . . . . . . . . . . . 13
β’ (πΉβπ₯) β V |
34 | 33 | elsn 4602 |
. . . . . . . . . . . 12
β’ ((πΉβπ₯) β {π} β (πΉβπ₯) = π) |
35 | | fvex 6856 |
. . . . . . . . . . . . 13
β’ (πΉβπ¦) β V |
36 | 35 | elsn 4602 |
. . . . . . . . . . . 12
β’ ((πΉβπ¦) β {π} β (πΉβπ¦) = π) |
37 | 34, 36 | anbi12i 628 |
. . . . . . . . . . 11
β’ (((πΉβπ₯) β {π} β§ (πΉβπ¦) β {π}) β ((πΉβπ₯) = π β§ (πΉβπ¦) = π)) |
38 | | fvex 6856 |
. . . . . . . . . . . 12
β’ (πΉβ(π₯(1st βπ
)π¦)) β V |
39 | 38 | elsn 4602 |
. . . . . . . . . . 11
β’ ((πΉβ(π₯(1st βπ
)π¦)) β {π} β (πΉβ(π₯(1st βπ
)π¦)) = π) |
40 | 32, 37, 39 | 3imtr4g 296 |
. . . . . . . . . 10
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
))) β (((πΉβπ₯) β {π} β§ (πΉβπ¦) β {π}) β (πΉβ(π₯(1st βπ
)π¦)) β {π})) |
41 | 40 | imdistanda 573 |
. . . . . . . . 9
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β§ ((πΉβπ₯) β {π} β§ (πΉβπ¦) β {π})) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β§ (πΉβ(π₯(1st βπ
)π¦)) β {π}))) |
42 | 2, 3 | rngogcl 36374 |
. . . . . . . . . . . 12
β’ ((π
β RingOps β§ π₯ β ran (1st
βπ
) β§ π¦ β ran (1st
βπ
)) β (π₯(1st βπ
)π¦) β ran (1st βπ
)) |
43 | 42 | 3expib 1123 |
. . . . . . . . . . 11
β’ (π
β RingOps β ((π₯ β ran (1st
βπ
) β§ π¦ β ran (1st
βπ
)) β (π₯(1st βπ
)π¦) β ran (1st βπ
))) |
44 | 43 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β (π₯(1st βπ
)π¦) β ran (1st βπ
))) |
45 | 44 | anim1d 612 |
. . . . . . . . 9
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β§ (πΉβ(π₯(1st βπ
)π¦)) β {π}) β ((π₯(1st βπ
)π¦) β ran (1st βπ
) β§ (πΉβ(π₯(1st βπ
)π¦)) β {π}))) |
46 | 41, 45 | syld 47 |
. . . . . . . 8
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (((π₯ β ran (1st βπ
) β§ π¦ β ran (1st βπ
)) β§ ((πΉβπ₯) β {π} β§ (πΉβπ¦) β {π})) β ((π₯(1st βπ
)π¦) β ran (1st βπ
) β§ (πΉβ(π₯(1st βπ
)π¦)) β {π}))) |
47 | 20, 46 | biimtrid 241 |
. . . . . . 7
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (((π₯ β ran (1st βπ
) β§ (πΉβπ₯) β {π}) β§ (π¦ β ran (1st βπ
) β§ (πΉβπ¦) β {π})) β ((π₯(1st βπ
)π¦) β ran (1st βπ
) β§ (πΉβ(π₯(1st βπ
)π¦)) β {π}))) |
48 | | elpreima 7009 |
. . . . . . . . 9
β’ (πΉ Fn ran (1st
βπ
) β (π₯ β (β‘πΉ β {π}) β (π₯ β ran (1st βπ
) β§ (πΉβπ₯) β {π}))) |
49 | 6, 16, 48 | 3syl 18 |
. . . . . . . 8
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (π₯ β (β‘πΉ β {π}) β (π₯ β ran (1st βπ
) β§ (πΉβπ₯) β {π}))) |
50 | | elpreima 7009 |
. . . . . . . . 9
β’ (πΉ Fn ran (1st
βπ
) β (π¦ β (β‘πΉ β {π}) β (π¦ β ran (1st βπ
) β§ (πΉβπ¦) β {π}))) |
51 | 6, 16, 50 | 3syl 18 |
. . . . . . . 8
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (π¦ β (β‘πΉ β {π}) β (π¦ β ran (1st βπ
) β§ (πΉβπ¦) β {π}))) |
52 | 49, 51 | anbi12d 632 |
. . . . . . 7
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π₯ β (β‘πΉ β {π}) β§ π¦ β (β‘πΉ β {π})) β ((π₯ β ran (1st βπ
) β§ (πΉβπ₯) β {π}) β§ (π¦ β ran (1st βπ
) β§ (πΉβπ¦) β {π})))) |
53 | | elpreima 7009 |
. . . . . . . 8
β’ (πΉ Fn ran (1st
βπ
) β ((π₯(1st βπ
)π¦) β (β‘πΉ β {π}) β ((π₯(1st βπ
)π¦) β ran (1st βπ
) β§ (πΉβ(π₯(1st βπ
)π¦)) β {π}))) |
54 | 6, 16, 53 | 3syl 18 |
. . . . . . 7
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π₯(1st βπ
)π¦) β (β‘πΉ β {π}) β ((π₯(1st βπ
)π¦) β ran (1st βπ
) β§ (πΉβ(π₯(1st βπ
)π¦)) β {π}))) |
55 | 47, 52, 54 | 3imtr4d 294 |
. . . . . 6
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π₯ β (β‘πΉ β {π}) β§ π¦ β (β‘πΉ β {π})) β (π₯(1st βπ
)π¦) β (β‘πΉ β {π}))) |
56 | 55 | impl 457 |
. . . . 5
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π₯ β (β‘πΉ β {π})) β§ π¦ β (β‘πΉ β {π})) β (π₯(1st βπ
)π¦) β (β‘πΉ β {π})) |
57 | 56 | ralrimiva 3144 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π₯ β (β‘πΉ β {π})) β βπ¦ β (β‘πΉ β {π})(π₯(1st βπ
)π¦) β (β‘πΉ β {π})) |
58 | 34 | anbi2i 624 |
. . . . . . 7
β’ ((π₯ β ran (1st
βπ
) β§ (πΉβπ₯) β {π}) β (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) |
59 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(2nd βπ
) = (2nd βπ
) |
60 | 2, 59, 3 | rngocl 36363 |
. . . . . . . . . . . . . . 15
β’ ((π
β RingOps β§ π§ β ran (1st
βπ
) β§ π₯ β ran (1st
βπ
)) β (π§(2nd βπ
)π₯) β ran (1st βπ
)) |
61 | 60 | 3expb 1121 |
. . . . . . . . . . . . . 14
β’ ((π
β RingOps β§ (π§ β ran (1st
βπ
) β§ π₯ β ran (1st
βπ
))) β (π§(2nd βπ
)π₯) β ran (1st βπ
)) |
62 | 61 | 3ad2antl1 1186 |
. . . . . . . . . . . . 13
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π§ β ran (1st βπ
) β§ π₯ β ran (1st βπ
))) β (π§(2nd βπ
)π₯) β ran (1st βπ
)) |
63 | 62 | anass1rs 654 |
. . . . . . . . . . . 12
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π₯ β ran (1st βπ
)) β§ π§ β ran (1st βπ
)) β (π§(2nd βπ
)π₯) β ran (1st βπ
)) |
64 | 63 | adantlrr 720 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (π§(2nd βπ
)π₯) β ran (1st βπ
)) |
65 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(2nd βπ) = (2nd βπ) |
66 | 2, 3, 59, 65 | rngohommul 36432 |
. . . . . . . . . . . . . . 15
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π§ β ran (1st βπ
) β§ π₯ β ran (1st βπ
))) β (πΉβ(π§(2nd βπ
)π₯)) = ((πΉβπ§)(2nd βπ)(πΉβπ₯))) |
67 | 66 | anass1rs 654 |
. . . . . . . . . . . . . 14
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π₯ β ran (1st βπ
)) β§ π§ β ran (1st βπ
)) β (πΉβ(π§(2nd βπ
)π₯)) = ((πΉβπ§)(2nd βπ)(πΉβπ₯))) |
68 | 67 | adantlrr 720 |
. . . . . . . . . . . . 13
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (πΉβ(π§(2nd βπ
)π₯)) = ((πΉβπ§)(2nd βπ)(πΉβπ₯))) |
69 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ₯) = π β ((πΉβπ§)(2nd βπ)(πΉβπ₯)) = ((πΉβπ§)(2nd βπ)π)) |
70 | 69 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π₯ β ran (1st
βπ
) β§ (πΉβπ₯) = π) β ((πΉβπ§)(2nd βπ)(πΉβπ₯)) = ((πΉβπ§)(2nd βπ)π)) |
71 | 70 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β ((πΉβπ§)(2nd βπ)(πΉβπ₯)) = ((πΉβπ§)(2nd βπ)π)) |
72 | 2, 3, 4, 5 | rngohomcl 36429 |
. . . . . . . . . . . . . . 15
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π§ β ran (1st βπ
)) β (πΉβπ§) β ran πΊ) |
73 | 11, 5, 4, 65 | rngorz 36385 |
. . . . . . . . . . . . . . . 16
β’ ((π β RingOps β§ (πΉβπ§) β ran πΊ) β ((πΉβπ§)(2nd βπ)π) = π) |
74 | 73 | 3ad2antl2 1187 |
. . . . . . . . . . . . . . 15
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (πΉβπ§) β ran πΊ) β ((πΉβπ§)(2nd βπ)π) = π) |
75 | 72, 74 | syldan 592 |
. . . . . . . . . . . . . 14
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π§ β ran (1st βπ
)) β ((πΉβπ§)(2nd βπ)π) = π) |
76 | 75 | adantlr 714 |
. . . . . . . . . . . . 13
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β ((πΉβπ§)(2nd βπ)π) = π) |
77 | 68, 71, 76 | 3eqtrd 2781 |
. . . . . . . . . . . 12
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (πΉβ(π§(2nd βπ
)π₯)) = π) |
78 | | fvex 6856 |
. . . . . . . . . . . . 13
β’ (πΉβ(π§(2nd βπ
)π₯)) β V |
79 | 78 | elsn 4602 |
. . . . . . . . . . . 12
β’ ((πΉβ(π§(2nd βπ
)π₯)) β {π} β (πΉβ(π§(2nd βπ
)π₯)) = π) |
80 | 77, 79 | sylibr 233 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (πΉβ(π§(2nd βπ
)π₯)) β {π}) |
81 | | elpreima 7009 |
. . . . . . . . . . . . 13
β’ (πΉ Fn ran (1st
βπ
) β ((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β ((π§(2nd βπ
)π₯) β ran (1st βπ
) β§ (πΉβ(π§(2nd βπ
)π₯)) β {π}))) |
82 | 6, 16, 81 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β ((π§(2nd βπ
)π₯) β ran (1st βπ
) β§ (πΉβ(π§(2nd βπ
)π₯)) β {π}))) |
83 | 82 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β ((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β ((π§(2nd βπ
)π₯) β ran (1st βπ
) β§ (πΉβ(π§(2nd βπ
)π₯)) β {π}))) |
84 | 64, 80, 83 | mpbir2and 712 |
. . . . . . . . . 10
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (π§(2nd βπ
)π₯) β (β‘πΉ β {π})) |
85 | 2, 59, 3 | rngocl 36363 |
. . . . . . . . . . . . . . 15
β’ ((π
β RingOps β§ π₯ β ran (1st
βπ
) β§ π§ β ran (1st
βπ
)) β (π₯(2nd βπ
)π§) β ran (1st βπ
)) |
86 | 85 | 3expb 1121 |
. . . . . . . . . . . . . 14
β’ ((π
β RingOps β§ (π₯ β ran (1st
βπ
) β§ π§ β ran (1st
βπ
))) β (π₯(2nd βπ
)π§) β ran (1st βπ
)) |
87 | 86 | 3ad2antl1 1186 |
. . . . . . . . . . . . 13
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π§ β ran (1st βπ
))) β (π₯(2nd βπ
)π§) β ran (1st βπ
)) |
88 | 87 | anassrs 469 |
. . . . . . . . . . . 12
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π₯ β ran (1st βπ
)) β§ π§ β ran (1st βπ
)) β (π₯(2nd βπ
)π§) β ran (1st βπ
)) |
89 | 88 | adantlrr 720 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (π₯(2nd βπ
)π§) β ran (1st βπ
)) |
90 | 2, 3, 59, 65 | rngohommul 36432 |
. . . . . . . . . . . . . . 15
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ π§ β ran (1st βπ
))) β (πΉβ(π₯(2nd βπ
)π§)) = ((πΉβπ₯)(2nd βπ)(πΉβπ§))) |
91 | 90 | anassrs 469 |
. . . . . . . . . . . . . 14
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π₯ β ran (1st βπ
)) β§ π§ β ran (1st βπ
)) β (πΉβ(π₯(2nd βπ
)π§)) = ((πΉβπ₯)(2nd βπ)(πΉβπ§))) |
92 | 91 | adantlrr 720 |
. . . . . . . . . . . . 13
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (πΉβ(π₯(2nd βπ
)π§)) = ((πΉβπ₯)(2nd βπ)(πΉβπ§))) |
93 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ₯) = π β ((πΉβπ₯)(2nd βπ)(πΉβπ§)) = (π(2nd βπ)(πΉβπ§))) |
94 | 93 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π₯ β ran (1st
βπ
) β§ (πΉβπ₯) = π) β ((πΉβπ₯)(2nd βπ)(πΉβπ§)) = (π(2nd βπ)(πΉβπ§))) |
95 | 94 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β ((πΉβπ₯)(2nd βπ)(πΉβπ§)) = (π(2nd βπ)(πΉβπ§))) |
96 | 11, 5, 4, 65 | rngolz 36384 |
. . . . . . . . . . . . . . . 16
β’ ((π β RingOps β§ (πΉβπ§) β ran πΊ) β (π(2nd βπ)(πΉβπ§)) = π) |
97 | 96 | 3ad2antl2 1187 |
. . . . . . . . . . . . . . 15
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (πΉβπ§) β ran πΊ) β (π(2nd βπ)(πΉβπ§)) = π) |
98 | 72, 97 | syldan 592 |
. . . . . . . . . . . . . 14
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π§ β ran (1st βπ
)) β (π(2nd βπ)(πΉβπ§)) = π) |
99 | 98 | adantlr 714 |
. . . . . . . . . . . . 13
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (π(2nd βπ)(πΉβπ§)) = π) |
100 | 92, 95, 99 | 3eqtrd 2781 |
. . . . . . . . . . . 12
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (πΉβ(π₯(2nd βπ
)π§)) = π) |
101 | | fvex 6856 |
. . . . . . . . . . . . 13
β’ (πΉβ(π₯(2nd βπ
)π§)) β V |
102 | 101 | elsn 4602 |
. . . . . . . . . . . 12
β’ ((πΉβ(π₯(2nd βπ
)π§)) β {π} β (πΉβ(π₯(2nd βπ
)π§)) = π) |
103 | 100, 102 | sylibr 233 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (πΉβ(π₯(2nd βπ
)π§)) β {π}) |
104 | | elpreima 7009 |
. . . . . . . . . . . . 13
β’ (πΉ Fn ran (1st
βπ
) β ((π₯(2nd βπ
)π§) β (β‘πΉ β {π}) β ((π₯(2nd βπ
)π§) β ran (1st βπ
) β§ (πΉβ(π₯(2nd βπ
)π§)) β {π}))) |
105 | 6, 16, 104 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π₯(2nd βπ
)π§) β (β‘πΉ β {π}) β ((π₯(2nd βπ
)π§) β ran (1st βπ
) β§ (πΉβ(π₯(2nd βπ
)π§)) β {π}))) |
106 | 105 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β ((π₯(2nd βπ
)π§) β (β‘πΉ β {π}) β ((π₯(2nd βπ
)π§) β ran (1st βπ
) β§ (πΉβ(π₯(2nd βπ
)π§)) β {π}))) |
107 | 89, 103, 106 | mpbir2and 712 |
. . . . . . . . . 10
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β (π₯(2nd βπ
)π§) β (β‘πΉ β {π})) |
108 | 84, 107 | jca 513 |
. . . . . . . . 9
β’ ((((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β§ π§ β ran (1st βπ
)) β ((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β§ (π₯(2nd βπ
)π§) β (β‘πΉ β {π}))) |
109 | 108 | ralrimiva 3144 |
. . . . . . . 8
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ (π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π)) β βπ§ β ran (1st βπ
)((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β§ (π₯(2nd βπ
)π§) β (β‘πΉ β {π}))) |
110 | 109 | ex 414 |
. . . . . . 7
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ (πΉβπ₯) = π) β βπ§ β ran (1st βπ
)((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β§ (π₯(2nd βπ
)π§) β (β‘πΉ β {π})))) |
111 | 58, 110 | biimtrid 241 |
. . . . . 6
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((π₯ β ran (1st βπ
) β§ (πΉβπ₯) β {π}) β βπ§ β ran (1st βπ
)((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β§ (π₯(2nd βπ
)π§) β (β‘πΉ β {π})))) |
112 | 49, 111 | sylbid 239 |
. . . . 5
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (π₯ β (β‘πΉ β {π}) β βπ§ β ran (1st βπ
)((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β§ (π₯(2nd βπ
)π§) β (β‘πΉ β {π})))) |
113 | 112 | imp 408 |
. . . 4
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π₯ β (β‘πΉ β {π})) β βπ§ β ran (1st βπ
)((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β§ (π₯(2nd βπ
)π§) β (β‘πΉ β {π}))) |
114 | 57, 113 | jca 513 |
. . 3
β’ (((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β§ π₯ β (β‘πΉ β {π})) β (βπ¦ β (β‘πΉ β {π})(π₯(1st βπ
)π¦) β (β‘πΉ β {π}) β§ βπ§ β ran (1st βπ
)((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β§ (π₯(2nd βπ
)π§) β (β‘πΉ β {π})))) |
115 | 114 | ralrimiva 3144 |
. 2
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β βπ₯ β (β‘πΉ β {π})(βπ¦ β (β‘πΉ β {π})(π₯(1st βπ
)π¦) β (β‘πΉ β {π}) β§ βπ§ β ran (1st βπ
)((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β§ (π₯(2nd βπ
)π§) β (β‘πΉ β {π})))) |
116 | 2, 59, 3, 8 | isidl 36476 |
. . 3
β’ (π
β RingOps β ((β‘πΉ β {π}) β (Idlβπ
) β ((β‘πΉ β {π}) β ran (1st βπ
) β§
(GIdβ(1st βπ
)) β (β‘πΉ β {π}) β§ βπ₯ β (β‘πΉ β {π})(βπ¦ β (β‘πΉ β {π})(π₯(1st βπ
)π¦) β (β‘πΉ β {π}) β§ βπ§ β ran (1st βπ
)((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β§ (π₯(2nd βπ
)π§) β (β‘πΉ β {π})))))) |
117 | 116 | 3ad2ant1 1134 |
. 2
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β ((β‘πΉ β {π}) β (Idlβπ
) β ((β‘πΉ β {π}) β ran (1st βπ
) β§
(GIdβ(1st βπ
)) β (β‘πΉ β {π}) β§ βπ₯ β (β‘πΉ β {π})(βπ¦ β (β‘πΉ β {π})(π₯(1st βπ
)π¦) β (β‘πΉ β {π}) β§ βπ§ β ran (1st βπ
)((π§(2nd βπ
)π₯) β (β‘πΉ β {π}) β§ (π₯(2nd βπ
)π§) β (β‘πΉ β {π})))))) |
118 | 7, 19, 115, 117 | mpbir3and 1343 |
1
β’ ((π
β RingOps β§ π β RingOps β§ πΉ β (π
RngHom π)) β (β‘πΉ β {π}) β (Idlβπ
)) |