Step | Hyp | Ref
| Expression |
1 | | rrxsca.r |
. . . 4
β’ π» = (β^βπΌ) |
2 | | eqid 2737 |
. . . 4
β’
(Baseβπ») =
(Baseβπ») |
3 | 1, 2 | rrxprds 24756 |
. . 3
β’ (πΌ β π β π» =
(toβPreHilβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)))) |
4 | 3 | fveq2d 6847 |
. 2
β’ (πΌ β π β (Scalarβπ») =
(Scalarβ(toβPreHilβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))))) |
5 | | fvex 6856 |
. . . . 5
β’
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) β
V |
6 | 5 | mptex 7174 |
. . . 4
β’ (π₯ β
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) β¦
(ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯))) β V |
7 | | eqid 2737 |
. . . . . 6
β’
(((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)) toNrmGrp
(π₯ β
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) β¦
(ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯)))) = (((βfldXs(πΌ Γ
{((subringAlg ββfld)ββ)})) βΎs (Baseβπ»)) toNrmGrp (π₯ β (Baseβ((βfldXs(πΌ Γ
{((subringAlg ββfld)ββ)})) βΎs (Baseβπ»))) β¦ (ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯)))) |
8 | | eqid 2737 |
. . . . . 6
β’
(Scalarβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) =
(Scalarβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) |
9 | 7, 8 | tngsca 24008 |
. . . . 5
β’ ((π₯ β
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) β¦
(ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯))) β V β
(Scalarβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs (Baseβπ»))) = (Scalarβ(((βfldXs(πΌ Γ
{((subringAlg ββfld)ββ)})) βΎs (Baseβπ»)) toNrmGrp (π₯ β (Baseβ((βfldXs(πΌ Γ
{((subringAlg ββfld)ββ)})) βΎs (Baseβπ»))) β¦ (ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯)))))) |
10 | 9 | eqcomd 2743 |
. . . 4
β’ ((π₯ β
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) β¦
(ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯))) β V β
(Scalarβ(((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs (Baseβπ»)) toNrmGrp (π₯
β (Baseβ((βfldXs(πΌ Γ
{((subringAlg ββfld)ββ)})) βΎs (Baseβπ»))) β¦ (ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯))))) = (Scalarβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))) |
11 | 6, 10 | mp1i 13 |
. . 3
β’ (πΌ β π β
(Scalarβ(((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)) toNrmGrp
(π₯ β
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) β¦
(ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯))))) = (Scalarβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))) |
12 | | eqid 2737 |
. . . . . 6
β’
(toβPreHilβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) =
(toβPreHilβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) |
13 | | eqid 2737 |
. . . . . 6
β’
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) =
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) |
14 | | eqid 2737 |
. . . . . 6
β’
(Β·πβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) =
(Β·πβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) |
15 | 12, 13, 14 | tcphval 24585 |
. . . . 5
β’
(toβPreHilβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) =
(((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)) toNrmGrp
(π₯ β
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) β¦
(ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯)))) |
16 | 15 | fveq2i 6846 |
. . . 4
β’
(Scalarβ(toβPreHilβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)))) =
(Scalarβ(((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)) toNrmGrp
(π₯ β
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) β¦
(ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯))))) |
17 | 16 | a1i 11 |
. . 3
β’ (πΌ β π β
(Scalarβ(toβPreHilβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)))) =
(Scalarβ(((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)) toNrmGrp
(π₯ β
(Baseβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»))) β¦
(ββ(π₯(Β·πβ((βfldXs(πΌ Γ {((subringAlg ββfld)ββ)}))
βΎs (Baseβπ»)))π₯)))))) |
18 | | eqid 2737 |
. . . . 5
β’
(βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) = (βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) |
19 | | refld 21026 |
. . . . . 6
β’
βfld β Field |
20 | 19 | a1i 11 |
. . . . 5
β’ (πΌ β π β βfld β
Field) |
21 | | id 22 |
. . . . . 6
β’ (πΌ β π β πΌ β π) |
22 | | snex 5389 |
. . . . . . 7
β’
{((subringAlg ββfld)ββ)} β
V |
23 | 22 | a1i 11 |
. . . . . 6
β’ (πΌ β π β {((subringAlg
ββfld)ββ)} β V) |
24 | 21, 23 | xpexd 7686 |
. . . . 5
β’ (πΌ β π β (πΌ Γ {((subringAlg
ββfld)ββ)}) β V) |
25 | 18, 20, 24 | prdssca 17339 |
. . . 4
β’ (πΌ β π β βfld =
(Scalarβ(βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})))) |
26 | | fvex 6856 |
. . . . 5
β’
(Baseβπ»)
β V |
27 | | eqid 2737 |
. . . . . 6
β’
((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)) =
((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)) |
28 | | eqid 2737 |
. . . . . 6
β’
(Scalarβ(βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)}))) =
(Scalarβ(βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)}))) |
29 | 27, 28 | resssca 17225 |
. . . . 5
β’
((Baseβπ»)
β V β (Scalarβ(βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)}))) =
(Scalarβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)))) |
30 | 26, 29 | mp1i 13 |
. . . 4
β’ (πΌ β π β
(Scalarβ(βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)}))) =
(Scalarβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)))) |
31 | 25, 30 | eqtrd 2777 |
. . 3
β’ (πΌ β π β βfld =
(Scalarβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)))) |
32 | 11, 17, 31 | 3eqtr4d 2787 |
. 2
β’ (πΌ β π β
(Scalarβ(toβPreHilβ((βfldXs(πΌ Γ {((subringAlg
ββfld)ββ)})) βΎs
(Baseβπ»)))) =
βfld) |
33 | 4, 32 | eqtrd 2777 |
1
β’ (πΌ β π β (Scalarβπ») = βfld) |