Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β π) |
2 | 1 | ad2antrr 725 |
. . . . . 6
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π) |
3 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦ β π΅ β§ π§ β π΅)) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π¦ β π΅ β§ π§ β π΅)) |
5 | | simprr 772 |
. . . . . 6
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β (π¦π»π§)) |
6 | | rhmsubcrngc.h |
. . . . . . 7
β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) |
7 | 6 | rhmresel 46382 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅) β§ π β (π¦π»π§)) β π β (π¦ RingHom π§)) |
8 | 2, 4, 5, 7 | syl3anc 1372 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β (π¦ RingHom π§)) |
9 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β π₯ β π΅) |
10 | | simpl 484 |
. . . . . . . 8
β’ ((π¦ β π΅ β§ π§ β π΅) β π¦ β π΅) |
11 | 9, 10 | anim12i 614 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π₯ β π΅ β§ π¦ β π΅)) |
12 | 11 | adantr 482 |
. . . . . 6
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π₯ β π΅ β§ π¦ β π΅)) |
13 | | simprl 770 |
. . . . . 6
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β (π₯π»π¦)) |
14 | 6 | rhmresel 46382 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅) β§ π β (π₯π»π¦)) β π β (π₯ RingHom π¦)) |
15 | 2, 12, 13, 14 | syl3anc 1372 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β (π₯ RingHom π¦)) |
16 | | rhmco 20180 |
. . . . 5
β’ ((π β (π¦ RingHom π§) β§ π β (π₯ RingHom π¦)) β (π β π) β (π₯ RingHom π§)) |
17 | 8, 15, 16 | syl2anc 585 |
. . . 4
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π β π) β (π₯ RingHom π§)) |
18 | | rhmsubcrngc.c |
. . . . 5
β’ πΆ = (RngCatβπ) |
19 | | rhmsubcrngc.u |
. . . . . . 7
β’ (π β π β π) |
20 | 19 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β π β π) |
21 | 20 | ad2antrr 725 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β π) |
22 | | eqid 2737 |
. . . . 5
β’
(compβπΆ) =
(compβπΆ) |
23 | | rhmsubcrngc.b |
. . . . . . . . 9
β’ (π β π΅ = (Ring β© π)) |
24 | 23 | eleq2d 2824 |
. . . . . . . 8
β’ (π β (π₯ β π΅ β π₯ β (Ring β© π))) |
25 | | elinel2 4161 |
. . . . . . . 8
β’ (π₯ β (Ring β© π) β π₯ β π) |
26 | 24, 25 | syl6bi 253 |
. . . . . . 7
β’ (π β (π₯ β π΅ β π₯ β π)) |
27 | 26 | imp 408 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β π₯ β π) |
28 | 27 | ad2antrr 725 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π₯ β π) |
29 | 23 | eleq2d 2824 |
. . . . . . . . . . 11
β’ (π β (π¦ β π΅ β π¦ β (Ring β© π))) |
30 | | elinel2 4161 |
. . . . . . . . . . 11
β’ (π¦ β (Ring β© π) β π¦ β π) |
31 | 29, 30 | syl6bi 253 |
. . . . . . . . . 10
β’ (π β (π¦ β π΅ β π¦ β π)) |
32 | 31 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β (π¦ β π΅ β π¦ β π)) |
33 | 32 | com12 32 |
. . . . . . . 8
β’ (π¦ β π΅ β ((π β§ π₯ β π΅) β π¦ β π)) |
34 | 33 | adantr 482 |
. . . . . . 7
β’ ((π¦ β π΅ β§ π§ β π΅) β ((π β§ π₯ β π΅) β π¦ β π)) |
35 | 34 | impcom 409 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β π¦ β π) |
36 | 35 | adantr 482 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π¦ β π) |
37 | 23 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π β (π§ β π΅ β π§ β (Ring β© π))) |
38 | | elinel2 4161 |
. . . . . . . . . 10
β’ (π§ β (Ring β© π) β π§ β π) |
39 | 37, 38 | syl6bi 253 |
. . . . . . . . 9
β’ (π β (π§ β π΅ β π§ β π)) |
40 | 39 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (π§ β π΅ β π§ β π)) |
41 | 40 | adantld 492 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β ((π¦ β π΅ β§ π§ β π΅) β π§ β π)) |
42 | 41 | imp 408 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β π§ β π) |
43 | 42 | adantr 482 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π§ β π) |
44 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π΅ β§ (π β§ π₯ β π΅)) β π) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π¦ β π΅ β§ (π β§ π₯ β π΅)) β§ π β (π₯π»π¦)) β π) |
46 | 9 | anim1i 616 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΅) β§ π¦ β π΅) β (π₯ β π΅ β§ π¦ β π΅)) |
47 | 46 | ancoms 460 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π΅ β§ (π β§ π₯ β π΅)) β (π₯ β π΅ β§ π¦ β π΅)) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π¦ β π΅ β§ (π β§ π₯ β π΅)) β§ π β (π₯π»π¦)) β (π₯ β π΅ β§ π¦ β π΅)) |
49 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π¦ β π΅ β§ (π β§ π₯ β π΅)) β§ π β (π₯π»π¦)) β π β (π₯π»π¦)) |
50 | 45, 48, 49, 14 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π¦ β π΅ β§ (π β§ π₯ β π΅)) β§ π β (π₯π»π¦)) β π β (π₯ RingHom π¦)) |
51 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(Baseβπ₯) =
(Baseβπ₯) |
52 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(Baseβπ¦) =
(Baseβπ¦) |
53 | 51, 52 | rhmf 20167 |
. . . . . . . . . . . 12
β’ (π β (π₯ RingHom π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦)) |
54 | 50, 53 | syl 17 |
. . . . . . . . . . 11
β’ (((π¦ β π΅ β§ (π β§ π₯ β π΅)) β§ π β (π₯π»π¦)) β π:(Baseβπ₯)βΆ(Baseβπ¦)) |
55 | 54 | exp31 421 |
. . . . . . . . . 10
β’ (π¦ β π΅ β ((π β§ π₯ β π΅) β (π β (π₯π»π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦)))) |
56 | 55 | adantr 482 |
. . . . . . . . 9
β’ ((π¦ β π΅ β§ π§ β π΅) β ((π β§ π₯ β π΅) β (π β (π₯π»π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦)))) |
57 | 56 | impcom 409 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π β (π₯π»π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦))) |
58 | 57 | com12 32 |
. . . . . . 7
β’ (π β (π₯π»π¦) β (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β π:(Baseβπ₯)βΆ(Baseβπ¦))) |
59 | 58 | adantr 482 |
. . . . . 6
β’ ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β π:(Baseβπ₯)βΆ(Baseβπ¦))) |
60 | 59 | impcom 409 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π:(Baseβπ₯)βΆ(Baseβπ¦)) |
61 | 7 | 3expa 1119 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β (π¦π»π§)) β π β (π¦ RingHom π§)) |
62 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβπ§) =
(Baseβπ§) |
63 | 52, 62 | rhmf 20167 |
. . . . . . . . . 10
β’ (π β (π¦ RingHom π§) β π:(Baseβπ¦)βΆ(Baseβπ§)) |
64 | 61, 63 | syl 17 |
. . . . . . . . 9
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β (π¦π»π§)) β π:(Baseβπ¦)βΆ(Baseβπ§)) |
65 | 64 | ex 414 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π β (π¦π»π§) β π:(Baseβπ¦)βΆ(Baseβπ§))) |
66 | 65 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π β (π¦π»π§) β π:(Baseβπ¦)βΆ(Baseβπ§))) |
67 | 66 | adantld 492 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β π:(Baseβπ¦)βΆ(Baseβπ§))) |
68 | 67 | imp 408 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π:(Baseβπ¦)βΆ(Baseβπ§)) |
69 | 18, 21, 22, 28, 36, 43, 60, 68 | rngcco 46343 |
. . . 4
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) = (π β π)) |
70 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β π» = ( RingHom βΎ (π΅ Γ π΅))) |
71 | 70 | oveqdr 7390 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π₯π»π§) = (π₯( RingHom βΎ (π΅ Γ π΅))π§)) |
72 | | ovres 7525 |
. . . . . . 7
β’ ((π₯ β π΅ β§ π§ β π΅) β (π₯( RingHom βΎ (π΅ Γ π΅))π§) = (π₯ RingHom π§)) |
73 | 72 | ad2ant2l 745 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π₯( RingHom βΎ (π΅ Γ π΅))π§) = (π₯ RingHom π§)) |
74 | 71, 73 | eqtrd 2777 |
. . . . 5
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π₯π»π§) = (π₯ RingHom π§)) |
75 | 74 | adantr 482 |
. . . 4
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π₯π»π§) = (π₯ RingHom π§)) |
76 | 17, 69, 75 | 3eltr4d 2853 |
. . 3
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) |
77 | 76 | ralrimivva 3198 |
. 2
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) |
78 | 77 | ralrimivva 3198 |
1
β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π΅ βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) |