Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β π) |
2 | 1 | adantr 482 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β π) |
3 | 2 | adantr 482 |
. . . . . 6
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π) |
4 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦ β π΅ β§ π§ β π΅)) |
5 | 4 | adantr 482 |
. . . . . 6
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π¦ β π΅ β§ π§ β π΅)) |
6 | | simpr 486 |
. . . . . . 7
β’ ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β π β (π¦π»π§)) |
7 | 6 | adantl 483 |
. . . . . 6
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β (π¦π»π§)) |
8 | | rhmsubcsetc.h |
. . . . . . 7
β’ (π β π» = ( RingHom βΎ (π΅ Γ π΅))) |
9 | 8 | rhmresel 45625 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅) β§ π β (π¦π»π§)) β π β (π¦ RingHom π§)) |
10 | 3, 5, 7, 9 | syl3anc 1371 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β (π¦ RingHom π§)) |
11 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β π₯ β π΅) |
12 | | simpl 484 |
. . . . . . . 8
β’ ((π¦ β π΅ β§ π§ β π΅) β π¦ β π΅) |
13 | 11, 12 | anim12i 614 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π₯ β π΅ β§ π¦ β π΅)) |
14 | 13 | adantr 482 |
. . . . . 6
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π₯ β π΅ β§ π¦ β π΅)) |
15 | | simprl 769 |
. . . . . 6
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β (π₯π»π¦)) |
16 | 8 | rhmresel 45625 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅) β§ π β (π₯π»π¦)) β π β (π₯ RingHom π¦)) |
17 | 3, 14, 15, 16 | syl3anc 1371 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β (π₯ RingHom π¦)) |
18 | | rhmco 20022 |
. . . . 5
β’ ((π β (π¦ RingHom π§) β§ π β (π₯ RingHom π¦)) β (π β π) β (π₯ RingHom π§)) |
19 | 10, 17, 18 | syl2anc 585 |
. . . 4
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π β π) β (π₯ RingHom π§)) |
20 | | rhmsubcsetc.c |
. . . . 5
β’ πΆ = (ExtStrCatβπ) |
21 | | rhmsubcsetc.u |
. . . . . 6
β’ (π β π β π) |
22 | 21 | ad3antrrr 728 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π β π) |
23 | | eqid 2736 |
. . . . 5
β’
(compβπΆ) =
(compβπΆ) |
24 | | rhmsubcsetc.b |
. . . . . . . . . 10
β’ (π β π΅ = (Ring β© π)) |
25 | 24 | eleq2d 2822 |
. . . . . . . . 9
β’ (π β (π₯ β π΅ β π₯ β (Ring β© π))) |
26 | | elinel2 4136 |
. . . . . . . . 9
β’ (π₯ β (Ring β© π) β π₯ β π) |
27 | 25, 26 | syl6bi 254 |
. . . . . . . 8
β’ (π β (π₯ β π΅ β π₯ β π)) |
28 | 27 | imp 408 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β π₯ β π) |
29 | 28 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β π₯ β π) |
30 | 29 | adantr 482 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π₯ β π) |
31 | 24 | eleq2d 2822 |
. . . . . . . . . . 11
β’ (π β (π¦ β π΅ β π¦ β (Ring β© π))) |
32 | | elinel2 4136 |
. . . . . . . . . . 11
β’ (π¦ β (Ring β© π) β π¦ β π) |
33 | 31, 32 | syl6bi 254 |
. . . . . . . . . 10
β’ (π β (π¦ β π΅ β π¦ β π)) |
34 | 33 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β (π¦ β π΅ β π¦ β π)) |
35 | 34 | com12 32 |
. . . . . . . 8
β’ (π¦ β π΅ β ((π β§ π₯ β π΅) β π¦ β π)) |
36 | 35 | adantr 482 |
. . . . . . 7
β’ ((π¦ β π΅ β§ π§ β π΅) β ((π β§ π₯ β π΅) β π¦ β π)) |
37 | 36 | impcom 409 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β π¦ β π) |
38 | 37 | adantr 482 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π¦ β π) |
39 | 24 | eleq2d 2822 |
. . . . . . . . . 10
β’ (π β (π§ β π΅ β π§ β (Ring β© π))) |
40 | | elinel2 4136 |
. . . . . . . . . 10
β’ (π§ β (Ring β© π) β π§ β π) |
41 | 39, 40 | syl6bi 254 |
. . . . . . . . 9
β’ (π β (π§ β π΅ β π§ β π)) |
42 | 41 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (π§ β π΅ β π§ β π)) |
43 | 42 | adantld 492 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β ((π¦ β π΅ β§ π§ β π΅) β π§ β π)) |
44 | 43 | imp 408 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β π§ β π) |
45 | 44 | adantr 482 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π§ β π) |
46 | | eqid 2736 |
. . . . 5
β’
(Baseβπ₯) =
(Baseβπ₯) |
47 | | eqid 2736 |
. . . . 5
β’
(Baseβπ¦) =
(Baseβπ¦) |
48 | | eqid 2736 |
. . . . 5
β’
(Baseβπ§) =
(Baseβπ§) |
49 | | simprl 769 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β π΅ β§ (π β§ π₯ β π΅)) β π) |
50 | 49 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π¦ β π΅ β§ (π β§ π₯ β π΅)) β§ π β (π₯π»π¦)) β π) |
51 | 11 | anim1i 616 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π΅) β§ π¦ β π΅) β (π₯ β π΅ β§ π¦ β π΅)) |
52 | 51 | ancoms 460 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β π΅ β§ (π β§ π₯ β π΅)) β (π₯ β π΅ β§ π¦ β π΅)) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π¦ β π΅ β§ (π β§ π₯ β π΅)) β§ π β (π₯π»π¦)) β (π₯ β π΅ β§ π¦ β π΅)) |
54 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π¦ β π΅ β§ (π β§ π₯ β π΅)) β§ π β (π₯π»π¦)) β π β (π₯π»π¦)) |
55 | 50, 53, 54, 16 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ (((π¦ β π΅ β§ (π β§ π₯ β π΅)) β§ π β (π₯π»π¦)) β π β (π₯ RingHom π¦)) |
56 | 46, 47 | rhmf 20011 |
. . . . . . . . . . . . 13
β’ (π β (π₯ RingHom π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
β’ (((π¦ β π΅ β§ (π β§ π₯ β π΅)) β§ π β (π₯π»π¦)) β π:(Baseβπ₯)βΆ(Baseβπ¦)) |
58 | 57 | ex 414 |
. . . . . . . . . . 11
β’ ((π¦ β π΅ β§ (π β§ π₯ β π΅)) β (π β (π₯π»π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦))) |
59 | 58 | ex 414 |
. . . . . . . . . 10
β’ (π¦ β π΅ β ((π β§ π₯ β π΅) β (π β (π₯π»π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦)))) |
60 | 59 | adantr 482 |
. . . . . . . . 9
β’ ((π¦ β π΅ β§ π§ β π΅) β ((π β§ π₯ β π΅) β (π β (π₯π»π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦)))) |
61 | 60 | impcom 409 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π β (π₯π»π¦) β π:(Baseβπ₯)βΆ(Baseβπ¦))) |
62 | 61 | com12 32 |
. . . . . . 7
β’ (π β (π₯π»π¦) β (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β π:(Baseβπ₯)βΆ(Baseβπ¦))) |
63 | 62 | adantr 482 |
. . . . . 6
β’ ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β π:(Baseβπ₯)βΆ(Baseβπ¦))) |
64 | 63 | impcom 409 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π:(Baseβπ₯)βΆ(Baseβπ¦)) |
65 | 9 | 3expa 1118 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β (π¦π»π§)) β π β (π¦ RingHom π§)) |
66 | 47, 48 | rhmf 20011 |
. . . . . . . . . 10
β’ (π β (π¦ RingHom π§) β π:(Baseβπ¦)βΆ(Baseβπ§)) |
67 | 65, 66 | syl 17 |
. . . . . . . . 9
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π β (π¦π»π§)) β π:(Baseβπ¦)βΆ(Baseβπ§)) |
68 | 67 | ex 414 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π β (π¦π»π§) β π:(Baseβπ¦)βΆ(Baseβπ§))) |
69 | 68 | adantlr 713 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π β (π¦π»π§) β π:(Baseβπ¦)βΆ(Baseβπ§))) |
70 | 69 | adantld 492 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β ((π β (π₯π»π¦) β§ π β (π¦π»π§)) β π:(Baseβπ¦)βΆ(Baseβπ§))) |
71 | 70 | imp 408 |
. . . . 5
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β π:(Baseβπ¦)βΆ(Baseβπ§)) |
72 | 20, 22, 23, 30, 38, 45, 46, 47, 48, 64, 71 | estrcco 17887 |
. . . 4
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) = (π β π)) |
73 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β π» = ( RingHom βΎ (π΅ Γ π΅))) |
74 | 73 | oveqdr 7331 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π₯π»π§) = (π₯( RingHom βΎ (π΅ Γ π΅))π§)) |
75 | | ovres 7466 |
. . . . . . 7
β’ ((π₯ β π΅ β§ π§ β π΅) β (π₯( RingHom βΎ (π΅ Γ π΅))π§) = (π₯ RingHom π§)) |
76 | 75 | ad2ant2l 744 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π₯( RingHom βΎ (π΅ Γ π΅))π§) = (π₯ RingHom π§)) |
77 | 74, 76 | eqtrd 2776 |
. . . . 5
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β (π₯π»π§) = (π₯ RingHom π§)) |
78 | 77 | adantr 482 |
. . . 4
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π₯π»π§) = (π₯ RingHom π§)) |
79 | 19, 72, 78 | 3eltr4d 2852 |
. . 3
β’ ((((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β§ (π β (π₯π»π¦) β§ π β (π¦π»π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) |
80 | 79 | ralrimivva 3194 |
. 2
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π΅)) β βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) |
81 | 80 | ralrimivva 3194 |
1
β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π΅ βπ β (π₯π»π¦)βπ β (π¦π»π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π»π§)) |