Step | Hyp | Ref
| Expression |
1 | | subrgascl.c |
. . . 4
β’ πΆ = (algScβπ) |
2 | | eqid 2732 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
3 | | eqid 2732 |
. . . 4
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
4 | 1, 2, 3 | asclfn 21426 |
. . 3
β’ πΆ Fn
(Baseβ(Scalarβπ)) |
5 | | subrgascl.r |
. . . . . 6
β’ (π β π β (SubRingβπ
)) |
6 | | subrgascl.h |
. . . . . . 7
β’ π» = (π
βΎs π) |
7 | 6 | subrgbas 20364 |
. . . . . 6
β’ (π β (SubRingβπ
) β π = (Baseβπ»)) |
8 | 5, 7 | syl 17 |
. . . . 5
β’ (π β π = (Baseβπ»)) |
9 | | subrgascl.u |
. . . . . . 7
β’ π = (πΌ mPoly π») |
10 | | subrgascl.i |
. . . . . . 7
β’ (π β πΌ β π) |
11 | 6 | ovexi 7439 |
. . . . . . . 8
β’ π» β V |
12 | 11 | a1i 11 |
. . . . . . 7
β’ (π β π» β V) |
13 | 9, 10, 12 | mplsca 21563 |
. . . . . 6
β’ (π β π» = (Scalarβπ)) |
14 | 13 | fveq2d 6892 |
. . . . 5
β’ (π β (Baseβπ») =
(Baseβ(Scalarβπ))) |
15 | 8, 14 | eqtrd 2772 |
. . . 4
β’ (π β π = (Baseβ(Scalarβπ))) |
16 | 15 | fneq2d 6640 |
. . 3
β’ (π β (πΆ Fn π β πΆ Fn (Baseβ(Scalarβπ)))) |
17 | 4, 16 | mpbiri 257 |
. 2
β’ (π β πΆ Fn π) |
18 | | subrgascl.a |
. . . . 5
β’ π΄ = (algScβπ) |
19 | | eqid 2732 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
20 | | eqid 2732 |
. . . . 5
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
21 | 18, 19, 20 | asclfn 21426 |
. . . 4
β’ π΄ Fn
(Baseβ(Scalarβπ)) |
22 | | subrgascl.p |
. . . . . . 7
β’ π = (πΌ mPoly π
) |
23 | | subrgrcl 20360 |
. . . . . . . 8
β’ (π β (SubRingβπ
) β π
β Ring) |
24 | 5, 23 | syl 17 |
. . . . . . 7
β’ (π β π
β Ring) |
25 | 22, 10, 24 | mplsca 21563 |
. . . . . 6
β’ (π β π
= (Scalarβπ)) |
26 | 25 | fveq2d 6892 |
. . . . 5
β’ (π β (Baseβπ
) =
(Baseβ(Scalarβπ))) |
27 | 26 | fneq2d 6640 |
. . . 4
β’ (π β (π΄ Fn (Baseβπ
) β π΄ Fn (Baseβ(Scalarβπ)))) |
28 | 21, 27 | mpbiri 257 |
. . 3
β’ (π β π΄ Fn (Baseβπ
)) |
29 | | eqid 2732 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
30 | 29 | subrgss 20356 |
. . . 4
β’ (π β (SubRingβπ
) β π β (Baseβπ
)) |
31 | 5, 30 | syl 17 |
. . 3
β’ (π β π β (Baseβπ
)) |
32 | | fnssres 6670 |
. . 3
β’ ((π΄ Fn (Baseβπ
) β§ π β (Baseβπ
)) β (π΄ βΎ π) Fn π) |
33 | 28, 31, 32 | syl2anc 584 |
. 2
β’ (π β (π΄ βΎ π) Fn π) |
34 | | fvres 6907 |
. . . 4
β’ (π₯ β π β ((π΄ βΎ π)βπ₯) = (π΄βπ₯)) |
35 | 34 | adantl 482 |
. . 3
β’ ((π β§ π₯ β π) β ((π΄ βΎ π)βπ₯) = (π΄βπ₯)) |
36 | | eqid 2732 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
37 | 6, 36 | subrg0 20362 |
. . . . . . . 8
β’ (π β (SubRingβπ
) β
(0gβπ
) =
(0gβπ»)) |
38 | 5, 37 | syl 17 |
. . . . . . 7
β’ (π β (0gβπ
) = (0gβπ»)) |
39 | 38 | ifeq2d 4547 |
. . . . . 6
β’ (π β if(π¦ = (πΌ Γ {0}), π₯, (0gβπ
)) = if(π¦ = (πΌ Γ {0}), π₯, (0gβπ»))) |
40 | 39 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π) β if(π¦ = (πΌ Γ {0}), π₯, (0gβπ
)) = if(π¦ = (πΌ Γ {0}), π₯, (0gβπ»))) |
41 | 40 | mpteq2dv 5249 |
. . . 4
β’ ((π β§ π₯ β π) β (π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = (πΌ Γ {0}), π₯, (0gβπ
))) = (π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = (πΌ Γ {0}), π₯, (0gβπ»)))) |
42 | | eqid 2732 |
. . . . 5
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
43 | 10 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π) β πΌ β π) |
44 | 24 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π) β π
β Ring) |
45 | 31 | sselda 3981 |
. . . . 5
β’ ((π β§ π₯ β π) β π₯ β (Baseβπ
)) |
46 | 22, 42, 36, 29, 18, 43, 44, 45 | mplascl 21616 |
. . . 4
β’ ((π β§ π₯ β π) β (π΄βπ₯) = (π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = (πΌ Γ {0}), π₯, (0gβπ
)))) |
47 | | eqid 2732 |
. . . . 5
β’
(0gβπ») = (0gβπ») |
48 | | eqid 2732 |
. . . . 5
β’
(Baseβπ») =
(Baseβπ») |
49 | 6 | subrgring 20358 |
. . . . . . 7
β’ (π β (SubRingβπ
) β π» β Ring) |
50 | 5, 49 | syl 17 |
. . . . . 6
β’ (π β π» β Ring) |
51 | 50 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π) β π» β Ring) |
52 | 8 | eleq2d 2819 |
. . . . . 6
β’ (π β (π₯ β π β π₯ β (Baseβπ»))) |
53 | 52 | biimpa 477 |
. . . . 5
β’ ((π β§ π₯ β π) β π₯ β (Baseβπ»)) |
54 | 9, 42, 47, 48, 1, 43, 51, 53 | mplascl 21616 |
. . . 4
β’ ((π β§ π₯ β π) β (πΆβπ₯) = (π¦ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
if(π¦ = (πΌ Γ {0}), π₯, (0gβπ»)))) |
55 | 41, 46, 54 | 3eqtr4d 2782 |
. . 3
β’ ((π β§ π₯ β π) β (π΄βπ₯) = (πΆβπ₯)) |
56 | 35, 55 | eqtr2d 2773 |
. 2
β’ ((π β§ π₯ β π) β (πΆβπ₯) = ((π΄ βΎ π)βπ₯)) |
57 | 17, 33, 56 | eqfnfvd 7032 |
1
β’ (π β πΆ = (π΄ βΎ π)) |