Step | Hyp | Ref
| Expression |
1 | | elin 3931 |
. . . . . . 7
β’ (π β (DivRing β© CRing)
β (π β DivRing
β§ π β
CRing)) |
2 | 1 | simprbi 498 |
. . . . . 6
β’ (π β (DivRing β© CRing)
β π β
CRing) |
3 | | crngring 19983 |
. . . . . 6
β’ (π β CRing β π β Ring) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ (π β (DivRing β© CRing)
β π β
Ring) |
5 | | df-field 20202 |
. . . . 5
β’ Field =
(DivRing β© CRing) |
6 | 4, 5 | eleq2s 2856 |
. . . 4
β’ (π β Field β π β Ring) |
7 | 6 | rgen 3067 |
. . 3
β’
βπ β
Field π β
Ring |
8 | | fldhmsubcALTV.d |
. . 3
β’ π· = (π β© Field) |
9 | | fldhmsubcALTV.f |
. . 3
β’ πΉ = (π β π·, π β π· β¦ (π RingHom π )) |
10 | 7, 8, 9 | srhmsubcALTV 46466 |
. 2
β’ (π β π β πΉ β
(Subcatβ(RingCatALTVβπ))) |
11 | | inss1 4193 |
. . . . . . 7
β’ (DivRing
β© CRing) β DivRing |
12 | 5, 11 | eqsstri 3983 |
. . . . . 6
β’ Field
β DivRing |
13 | | sslin 4199 |
. . . . . 6
β’ (Field
β DivRing β (π
β© Field) β (π
β© DivRing)) |
14 | 12, 13 | ax-mp 5 |
. . . . 5
β’ (π β© Field) β (π β© DivRing) |
15 | 14 | a1i 11 |
. . . 4
β’ (π β π β (π β© Field) β (π β© DivRing)) |
16 | | drhmsubcALTV.c |
. . . . 5
β’ πΆ = (π β© DivRing) |
17 | 8, 16 | sseq12i 3979 |
. . . 4
β’ (π· β πΆ β (π β© Field) β (π β© DivRing)) |
18 | 15, 17 | sylibr 233 |
. . 3
β’ (π β π β π· β πΆ) |
19 | | ssidd 3972 |
. . . . 5
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β (π₯ RingHom π¦) β (π₯ RingHom π¦)) |
20 | 9 | a1i 11 |
. . . . . 6
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β πΉ = (π β π·, π β π· β¦ (π RingHom π ))) |
21 | | oveq12 7371 |
. . . . . . 7
β’ ((π = π₯ β§ π = π¦) β (π RingHom π ) = (π₯ RingHom π¦)) |
22 | 21 | adantl 483 |
. . . . . 6
β’ (((π β π β§ (π₯ β π· β§ π¦ β π·)) β§ (π = π₯ β§ π = π¦)) β (π RingHom π ) = (π₯ RingHom π¦)) |
23 | | simprl 770 |
. . . . . 6
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β π₯ β π·) |
24 | | simpr 486 |
. . . . . . 7
β’ ((π₯ β π· β§ π¦ β π·) β π¦ β π·) |
25 | 24 | adantl 483 |
. . . . . 6
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β π¦ β π·) |
26 | | ovexd 7397 |
. . . . . 6
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β (π₯ RingHom π¦) β V) |
27 | 20, 22, 23, 25, 26 | ovmpod 7512 |
. . . . 5
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β (π₯πΉπ¦) = (π₯ RingHom π¦)) |
28 | | drhmsubcALTV.j |
. . . . . . 7
β’ π½ = (π β πΆ, π β πΆ β¦ (π RingHom π )) |
29 | 28 | a1i 11 |
. . . . . 6
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β π½ = (π β πΆ, π β πΆ β¦ (π RingHom π ))) |
30 | 14, 17 | mpbir 230 |
. . . . . . . 8
β’ π· β πΆ |
31 | 30 | sseli 3945 |
. . . . . . 7
β’ (π₯ β π· β π₯ β πΆ) |
32 | 31 | ad2antrl 727 |
. . . . . 6
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β π₯ β πΆ) |
33 | 30 | sseli 3945 |
. . . . . . . 8
β’ (π¦ β π· β π¦ β πΆ) |
34 | 33 | adantl 483 |
. . . . . . 7
β’ ((π₯ β π· β§ π¦ β π·) β π¦ β πΆ) |
35 | 34 | adantl 483 |
. . . . . 6
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β π¦ β πΆ) |
36 | 29, 22, 32, 35, 26 | ovmpod 7512 |
. . . . 5
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β (π₯π½π¦) = (π₯ RingHom π¦)) |
37 | 19, 27, 36 | 3sstr4d 3996 |
. . . 4
β’ ((π β π β§ (π₯ β π· β§ π¦ β π·)) β (π₯πΉπ¦) β (π₯π½π¦)) |
38 | 37 | ralrimivva 3198 |
. . 3
β’ (π β π β βπ₯ β π· βπ¦ β π· (π₯πΉπ¦) β (π₯π½π¦)) |
39 | | ovex 7395 |
. . . . . 6
β’ (π RingHom π ) β V |
40 | 9, 39 | fnmpoi 8007 |
. . . . 5
β’ πΉ Fn (π· Γ π·) |
41 | 40 | a1i 11 |
. . . 4
β’ (π β π β πΉ Fn (π· Γ π·)) |
42 | 28, 39 | fnmpoi 8007 |
. . . . 5
β’ π½ Fn (πΆ Γ πΆ) |
43 | 42 | a1i 11 |
. . . 4
β’ (π β π β π½ Fn (πΆ Γ πΆ)) |
44 | | inex1g 5281 |
. . . . 5
β’ (π β π β (π β© DivRing) β V) |
45 | 16, 44 | eqeltrid 2842 |
. . . 4
β’ (π β π β πΆ β V) |
46 | 41, 43, 45 | isssc 17710 |
. . 3
β’ (π β π β (πΉ βcat π½ β (π· β πΆ β§ βπ₯ β π· βπ¦ β π· (π₯πΉπ¦) β (π₯π½π¦)))) |
47 | 18, 38, 46 | mpbir2and 712 |
. 2
β’ (π β π β πΉ βcat π½) |
48 | 16, 28 | drhmsubcALTV 46470 |
. . 3
β’ (π β π β π½ β
(Subcatβ(RingCatALTVβπ))) |
49 | | eqid 2737 |
. . . 4
β’
((RingCatALTVβπ) βΎcat π½) = ((RingCatALTVβπ) βΎcat π½) |
50 | 49 | subsubc 17746 |
. . 3
β’ (π½ β
(Subcatβ(RingCatALTVβπ)) β (πΉ β
(Subcatβ((RingCatALTVβπ) βΎcat π½)) β (πΉ β
(Subcatβ(RingCatALTVβπ)) β§ πΉ βcat π½))) |
51 | 48, 50 | syl 17 |
. 2
β’ (π β π β (πΉ β
(Subcatβ((RingCatALTVβπ) βΎcat π½)) β (πΉ β
(Subcatβ(RingCatALTVβπ)) β§ πΉ βcat π½))) |
52 | 10, 47, 51 | mpbir2and 712 |
1
β’ (π β π β πΉ β
(Subcatβ((RingCatALTVβπ) βΎcat π½))) |