Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})) =
((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})) |
2 | | eqid 2733 |
. . 3
β’
(Baseβ((Scalarβ(βfld βΎs
π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))
= (Baseβ((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)}))) |
3 | | eqid 2733 |
. . 3
β’
(Baseβ((πΌ
Γ {(βfld βΎs π΄)})βπ₯)) = (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) |
4 | | eqid 2733 |
. . 3
β’
((distβ((πΌ
Γ {(βfld βΎs π΄)})βπ₯)) βΎ ((Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) Γ (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)))) = ((distβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) βΎ ((Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) Γ (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)))) |
5 | | eqid 2733 |
. . 3
β’
(distβ((Scalarβ(βfld βΎs
π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))
= (distβ((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)}))) |
6 | | fvexd 6861 |
. . 3
β’ ((π΄ β β β§ πΌ β Fin) β
(Scalarβ(βfld βΎs π΄)) β V) |
7 | | simpr 486 |
. . 3
β’ ((π΄ β β β§ πΌ β Fin) β πΌ β Fin) |
8 | | ovex 7394 |
. . . 4
β’
(βfld βΎs π΄) β V |
9 | | fnconstg 6734 |
. . . 4
β’
((βfld βΎs π΄) β V β (πΌ Γ {(βfld
βΎs π΄)}) Fn
πΌ) |
10 | 8, 9 | mp1i 13 |
. . 3
β’ ((π΄ β β β§ πΌ β Fin) β (πΌ Γ {(βfld
βΎs π΄)}) Fn
πΌ) |
11 | | eqid 2733 |
. . 3
β’
((distβ((Scalarβ(βfld βΎs
π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))
βΎ (π Γ π)) =
((distβ((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))
βΎ (π Γ π)) |
12 | | cnfldms 24162 |
. . . . . 6
β’
βfld β MetSp |
13 | | cnex 11140 |
. . . . . . . 8
β’ β
β V |
14 | 13 | ssex 5282 |
. . . . . . 7
β’ (π΄ β β β π΄ β V) |
15 | 14 | ad2antrr 725 |
. . . . . 6
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β π΄ β V) |
16 | | ressms 23905 |
. . . . . 6
β’
((βfld β MetSp β§ π΄ β V) β (βfld
βΎs π΄)
β MetSp) |
17 | 12, 15, 16 | sylancr 588 |
. . . . 5
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β (βfld
βΎs π΄)
β MetSp) |
18 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(βfld βΎs π΄)) = (Baseβ(βfld
βΎs π΄)) |
19 | | eqid 2733 |
. . . . . 6
β’
((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) = ((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) |
20 | 18, 19 | msmet 23833 |
. . . . 5
β’
((βfld βΎs π΄) β MetSp β
((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) β
(Metβ(Baseβ(βfld βΎs π΄)))) |
21 | 17, 20 | syl 17 |
. . . 4
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β ((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) β
(Metβ(Baseβ(βfld βΎs π΄)))) |
22 | 8 | fvconst2 7157 |
. . . . . . 7
β’ (π₯ β πΌ β ((πΌ Γ {(βfld
βΎs π΄)})βπ₯) = (βfld
βΎs π΄)) |
23 | 22 | adantl 483 |
. . . . . 6
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β ((πΌ Γ {(βfld
βΎs π΄)})βπ₯) = (βfld
βΎs π΄)) |
24 | 23 | fveq2d 6850 |
. . . . 5
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β (distβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) = (distβ(βfld
βΎs π΄))) |
25 | 23 | fveq2d 6850 |
. . . . . 6
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) = (Baseβ(βfld
βΎs π΄))) |
26 | 25 | sqxpeqd 5669 |
. . . . 5
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β ((Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) Γ (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯))) = ((Baseβ(βfld
βΎs π΄))
Γ (Baseβ(βfld βΎs π΄)))) |
27 | 24, 26 | reseq12d 5942 |
. . . 4
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β ((distβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) βΎ ((Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) Γ (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)))) = ((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄))))) |
28 | 25 | fveq2d 6850 |
. . . 4
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β (Metβ(Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯))) =
(Metβ(Baseβ(βfld βΎs π΄)))) |
29 | 21, 27, 28 | 3eltr4d 2849 |
. . 3
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β ((distβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) βΎ ((Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) Γ (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)))) β (Metβ(Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)))) |
30 | | totbndbnd 36298 |
. . . . . 6
β’
((((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β (((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦)) |
31 | | eqid 2733 |
. . . . . . . . . . 11
β’
(βfld βΎs π΄) = (βfld
βΎs π΄) |
32 | | cnfldbas 20823 |
. . . . . . . . . . 11
β’ β =
(Baseββfld) |
33 | 31, 32 | ressbas2 17128 |
. . . . . . . . . 10
β’ (π΄ β β β π΄ =
(Baseβ(βfld βΎs π΄))) |
34 | 33 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β π΄ = (Baseβ(βfld
βΎs π΄))) |
35 | 34 | fveq2d 6850 |
. . . . . . . 8
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β (Metβπ΄) =
(Metβ(Baseβ(βfld βΎs π΄)))) |
36 | 21, 35 | eleqtrrd 2837 |
. . . . . . 7
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β ((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) β (Metβπ΄)) |
37 | | eqid 2733 |
. . . . . . . . 9
β’
(((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) = (((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) |
38 | 37 | bnd2lem 36300 |
. . . . . . . 8
β’
((((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) β (Metβπ΄) β§ (((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦)) β π¦ β π΄) |
39 | 38 | ex 414 |
. . . . . . 7
β’
(((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) β (Metβπ΄) β
((((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦) β π¦ β π΄)) |
40 | 36, 39 | syl 17 |
. . . . . 6
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β
((((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦) β π¦ β π΄)) |
41 | 30, 40 | syl5 34 |
. . . . 5
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β
((((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β π¦ β π΄)) |
42 | | eqid 2733 |
. . . . . . . . 9
β’ ((abs
β β ) βΎ (π¦ Γ π¦)) = ((abs β β ) βΎ (π¦ Γ π¦)) |
43 | 42 | cntotbnd 36305 |
. . . . . . . 8
β’ (((abs
β β ) βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β ((abs β β ) βΎ
(π¦ Γ π¦)) β (Bndβπ¦)) |
44 | 43 | a1i 11 |
. . . . . . 7
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β (((abs β β ) βΎ
(π¦ Γ π¦)) β (TotBndβπ¦) β ((abs β β )
βΎ (π¦ Γ π¦)) β (Bndβπ¦))) |
45 | 34 | sseq2d 3980 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β (π¦ β π΄ β π¦ β (Baseβ(βfld
βΎs π΄)))) |
46 | 45 | biimpa 478 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β π¦ β (Baseβ(βfld
βΎs π΄))) |
47 | | xpss12 5652 |
. . . . . . . . . . 11
β’ ((π¦ β
(Baseβ(βfld βΎs π΄)) β§ π¦ β (Baseβ(βfld
βΎs π΄)))
β (π¦ Γ π¦) β
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) |
48 | 46, 46, 47 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β (π¦ Γ π¦) β ((Baseβ(βfld
βΎs π΄))
Γ (Baseβ(βfld βΎs π΄)))) |
49 | 48 | resabs1d 5972 |
. . . . . . . . 9
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β
(((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) = ((distβ(βfld
βΎs π΄))
βΎ (π¦ Γ π¦))) |
50 | 15 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β π΄ β V) |
51 | | cnfldds 20829 |
. . . . . . . . . . . 12
β’ (abs
β β ) = (distββfld) |
52 | 31, 51 | ressds 17299 |
. . . . . . . . . . 11
β’ (π΄ β V β (abs β
β ) = (distβ(βfld βΎs π΄))) |
53 | 50, 52 | syl 17 |
. . . . . . . . . 10
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β (abs β β ) =
(distβ(βfld βΎs π΄))) |
54 | 53 | reseq1d 5940 |
. . . . . . . . 9
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β ((abs β β ) βΎ
(π¦ Γ π¦)) =
((distβ(βfld βΎs π΄)) βΎ (π¦ Γ π¦))) |
55 | 49, 54 | eqtr4d 2776 |
. . . . . . . 8
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β
(((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) = ((abs β β ) βΎ (π¦ Γ π¦))) |
56 | 55 | eleq1d 2819 |
. . . . . . 7
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β
((((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β ((abs β β ) βΎ
(π¦ Γ π¦)) β (TotBndβπ¦))) |
57 | 55 | eleq1d 2819 |
. . . . . . 7
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β
((((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦) β ((abs β β ) βΎ
(π¦ Γ π¦)) β (Bndβπ¦))) |
58 | 44, 56, 57 | 3bitr4d 311 |
. . . . . 6
β’ ((((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β§ π¦ β π΄) β
((((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β (((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦))) |
59 | 58 | ex 414 |
. . . . 5
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β (π¦ β π΄ β
((((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β (((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦)))) |
60 | 41, 40, 59 | pm5.21ndd 381 |
. . . 4
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β
((((distβ(βfld βΎs π΄)) βΎ
((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β (((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦))) |
61 | 27 | reseq1d 5940 |
. . . . 5
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β (((distβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) βΎ ((Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) Γ (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)))) βΎ (π¦ Γ π¦)) = (((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦))) |
62 | 61 | eleq1d 2819 |
. . . 4
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β ((((distβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) βΎ ((Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) Γ (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)))) βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β (((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (TotBndβπ¦))) |
63 | 61 | eleq1d 2819 |
. . . 4
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β ((((distβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) βΎ ((Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) Γ (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦) β (((distβ(βfld
βΎs π΄))
βΎ ((Baseβ(βfld βΎs π΄)) Γ
(Baseβ(βfld βΎs π΄)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦))) |
64 | 60, 62, 63 | 3bitr4d 311 |
. . 3
β’ (((π΄ β β β§ πΌ β Fin) β§ π₯ β πΌ) β ((((distβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) βΎ ((Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) Γ (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)))) βΎ (π¦ Γ π¦)) β (TotBndβπ¦) β (((distβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) βΎ ((Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)) Γ (Baseβ((πΌ Γ {(βfld
βΎs π΄)})βπ₯)))) βΎ (π¦ Γ π¦)) β (Bndβπ¦))) |
65 | 1, 2, 3, 4, 5, 6, 7, 10, 11, 29, 64 | prdsbnd2 36304 |
. 2
β’ ((π΄ β β β§ πΌ β Fin) β
(((distβ((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))
βΎ (π Γ π)) β (TotBndβπ) β
((distβ((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))
βΎ (π Γ π)) β (Bndβπ))) |
66 | | cnpwstotbnd.d |
. . . 4
β’ π· = ((distβπ) βΎ (π Γ π)) |
67 | | cnpwstotbnd.y |
. . . . . . . 8
β’ π = ((βfld
βΎs π΄)
βs πΌ) |
68 | | eqid 2733 |
. . . . . . . 8
β’
(Scalarβ(βfld βΎs π΄)) =
(Scalarβ(βfld βΎs π΄)) |
69 | 67, 68 | pwsval 17376 |
. . . . . . 7
β’
(((βfld βΎs π΄) β V β§ πΌ β Fin) β π = ((Scalarβ(βfld
βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)}))) |
70 | 8, 7, 69 | sylancr 588 |
. . . . . 6
β’ ((π΄ β β β§ πΌ β Fin) β π =
((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)}))) |
71 | 70 | fveq2d 6850 |
. . . . 5
β’ ((π΄ β β β§ πΌ β Fin) β
(distβπ) =
(distβ((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))) |
72 | 71 | reseq1d 5940 |
. . . 4
β’ ((π΄ β β β§ πΌ β Fin) β
((distβπ) βΎ
(π Γ π)) =
((distβ((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))
βΎ (π Γ π))) |
73 | 66, 72 | eqtrid 2785 |
. . 3
β’ ((π΄ β β β§ πΌ β Fin) β π· =
((distβ((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))
βΎ (π Γ π))) |
74 | 73 | eleq1d 2819 |
. 2
β’ ((π΄ β β β§ πΌ β Fin) β (π· β (TotBndβπ) β
((distβ((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))
βΎ (π Γ π)) β (TotBndβπ))) |
75 | 73 | eleq1d 2819 |
. 2
β’ ((π΄ β β β§ πΌ β Fin) β (π· β (Bndβπ) β
((distβ((Scalarβ(βfld βΎs π΄))Xs(πΌ Γ {(βfld
βΎs π΄)})))
βΎ (π Γ π)) β (Bndβπ))) |
76 | 65, 74, 75 | 3bitr4d 311 |
1
β’ ((π΄ β β β§ πΌ β Fin) β (π· β (TotBndβπ) β π· β (Bndβπ))) |