Step | Hyp | Ref
| Expression |
1 | | dchrval.g |
. 2
β’ πΊ = (DChrβπ) |
2 | | df-dchr 26597 |
. . 3
β’ DChr =
(π β β β¦
β¦(β€/nβ€βπ) / π§β¦β¦{π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯} / πβ¦{β¨(Baseβndx), πβ©,
β¨(+gβndx), ( βf Β· βΎ (π Γ π))β©}) |
3 | | fvexd 6862 |
. . . 4
β’ ((π β§ π = π) β
(β€/nβ€βπ) β V) |
4 | | ovex 7395 |
. . . . . . 7
β’
((mulGrpβπ§)
MndHom (mulGrpββfld)) β V |
5 | 4 | rabex 5294 |
. . . . . 6
β’ {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯} β V |
6 | 5 | a1i 11 |
. . . . 5
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯} β V) |
7 | | dchrval.d |
. . . . . . . . . . 11
β’ (π β π· = {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}) |
8 | 7 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β π· = {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}) |
9 | | dchrval.z |
. . . . . . . . . . . . . . . 16
β’ π =
(β€/nβ€βπ) |
10 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π = π) β π = π) |
11 | 10 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π = π) β
(β€/nβ€βπ) = (β€/nβ€βπ)) |
12 | 9, 11 | eqtr4id 2796 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π = π) β π = (β€/nβ€βπ)) |
13 | 12 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
β’ ((π β§ π = π) β (π§ = π β π§ = (β€/nβ€βπ))) |
14 | 13 | biimpar 479 |
. . . . . . . . . . . . 13
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β π§ = π) |
15 | 14 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β (mulGrpβπ§) = (mulGrpβπ)) |
16 | 15 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β ((mulGrpβπ§) MndHom
(mulGrpββfld)) = ((mulGrpβπ) MndHom
(mulGrpββfld))) |
17 | 14 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β (Baseβπ§) = (Baseβπ)) |
18 | | dchrval.b |
. . . . . . . . . . . . . . 15
β’ π΅ = (Baseβπ) |
19 | 17, 18 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β (Baseβπ§) = π΅) |
20 | 14 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β (Unitβπ§) = (Unitβπ)) |
21 | | dchrval.u |
. . . . . . . . . . . . . . 15
β’ π = (Unitβπ) |
22 | 20, 21 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β (Unitβπ§) = π) |
23 | 19, 22 | difeq12d 4088 |
. . . . . . . . . . . . 13
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β ((Baseβπ§) β (Unitβπ§)) = (π΅ β π)) |
24 | 23 | xpeq1d 5667 |
. . . . . . . . . . . 12
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β (((Baseβπ§) β (Unitβπ§)) Γ {0}) = ((π΅ β π) Γ {0})) |
25 | 24 | sseq1d 3980 |
. . . . . . . . . . 11
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β ((((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯ β ((π΅ β π) Γ {0}) β π₯)) |
26 | 16, 25 | rabeqbidv 3427 |
. . . . . . . . . 10
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯} = {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}) |
27 | 8, 26 | eqtr4d 2780 |
. . . . . . . . 9
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β π· = {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯}) |
28 | 27 | eqeq2d 2748 |
. . . . . . . 8
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β (π = π· β π = {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯})) |
29 | 28 | biimpar 479 |
. . . . . . 7
β’ ((((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β§ π = {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯}) β π = π·) |
30 | 29 | opeq2d 4842 |
. . . . . 6
β’ ((((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β§ π = {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯}) β β¨(Baseβndx), πβ© = β¨(Baseβndx),
π·β©) |
31 | 29 | sqxpeqd 5670 |
. . . . . . . 8
β’ ((((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β§ π = {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯}) β (π Γ π) = (π· Γ π·)) |
32 | 31 | reseq2d 5942 |
. . . . . . 7
β’ ((((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β§ π = {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯}) β ( βf Β·
βΎ (π Γ π)) = ( βf
Β· βΎ (π· Γ
π·))) |
33 | 32 | opeq2d 4842 |
. . . . . 6
β’ ((((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β§ π = {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯}) β β¨(+gβndx), (
βf Β· βΎ (π Γ π))β© = β¨(+gβndx), (
βf Β· βΎ (π· Γ π·))β©) |
34 | 30, 33 | preq12d 4707 |
. . . . 5
β’ ((((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β§ π = {π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯}) β {β¨(Baseβndx), πβ©,
β¨(+gβndx), ( βf Β· βΎ (π Γ π))β©} = {β¨(Baseβndx), π·β©,
β¨(+gβndx), ( βf Β· βΎ (π· Γ π·))β©}) |
35 | 6, 34 | csbied 3898 |
. . . 4
β’ (((π β§ π = π) β§ π§ = (β€/nβ€βπ)) β β¦{π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯} / πβ¦{β¨(Baseβndx), πβ©,
β¨(+gβndx), ( βf Β· βΎ (π Γ π))β©} = {β¨(Baseβndx), π·β©,
β¨(+gβndx), ( βf Β· βΎ (π· Γ π·))β©}) |
36 | 3, 35 | csbied 3898 |
. . 3
β’ ((π β§ π = π) β
β¦(β€/nβ€βπ) / π§β¦β¦{π₯ β ((mulGrpβπ§) MndHom
(mulGrpββfld)) β£ (((Baseβπ§) β (Unitβπ§)) Γ {0}) β π₯} / πβ¦{β¨(Baseβndx), πβ©,
β¨(+gβndx), ( βf Β· βΎ (π Γ π))β©} = {β¨(Baseβndx), π·β©,
β¨(+gβndx), ( βf Β· βΎ (π· Γ π·))β©}) |
37 | | dchrval.n |
. . 3
β’ (π β π β β) |
38 | | prex 5394 |
. . . 4
β’
{β¨(Baseβndx), π·β©, β¨(+gβndx), (
βf Β· βΎ (π· Γ π·))β©} β V |
39 | 38 | a1i 11 |
. . 3
β’ (π β {β¨(Baseβndx),
π·β©,
β¨(+gβndx), ( βf Β· βΎ (π· Γ π·))β©} β V) |
40 | 2, 36, 37, 39 | fvmptd2 6961 |
. 2
β’ (π β (DChrβπ) = {β¨(Baseβndx),
π·β©,
β¨(+gβndx), ( βf Β· βΎ (π· Γ π·))β©}) |
41 | 1, 40 | eqtrid 2789 |
1
β’ (π β πΊ = {β¨(Baseβndx), π·β©,
β¨(+gβndx), ( βf Β· βΎ (π· Γ π·))β©}) |