Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(BaseSetβπ) =
(BaseSetβπ) |
2 | | eqid 2733 |
. . . 4
β’ (
+π£ βπ) = ( +π£ βπ) |
3 | 1, 2 | bafval 29595 |
. . 3
β’
(BaseSetβπ) =
ran ( +π£ βπ) |
4 | | hhsst.1 |
. . . . . . 7
β’ π = β¨β¨
+β , Β·β β©,
normββ© |
5 | 4 | hhnv 30156 |
. . . . . 6
β’ π β NrmCVec |
6 | | hhssp3.3 |
. . . . . 6
β’ π β (SubSpβπ) |
7 | | eqid 2733 |
. . . . . . 7
β’
(SubSpβπ) =
(SubSpβπ) |
8 | 7 | sspnv 29717 |
. . . . . 6
β’ ((π β NrmCVec β§ π β (SubSpβπ)) β π β NrmCVec) |
9 | 5, 6, 8 | mp2an 691 |
. . . . 5
β’ π β NrmCVec |
10 | 2 | nvgrp 29608 |
. . . . 5
β’ (π β NrmCVec β (
+π£ βπ) β GrpOp) |
11 | | grporndm 29501 |
. . . . 5
β’ ((
+π£ βπ) β GrpOp β ran (
+π£ βπ) = dom dom ( +π£
βπ)) |
12 | 9, 10, 11 | mp2b 10 |
. . . 4
β’ ran (
+π£ βπ) = dom dom ( +π£
βπ) |
13 | | hhsst.2 |
. . . . . . . . . 10
β’ π = β¨β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© |
14 | 13 | fveq2i 6849 |
. . . . . . . . 9
β’ (
+π£ βπ) = ( +π£
ββ¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β©) |
15 | | eqid 2733 |
. . . . . . . . . . 11
β’ (
+π£ ββ¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β©) = (
+π£ ββ¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β©) |
16 | 15 | vafval 29594 |
. . . . . . . . . 10
β’ (
+π£ ββ¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β©) = (1st
β(1st ββ¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β©)) |
17 | | opex 5425 |
. . . . . . . . . . . . 13
β’ β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β© β V |
18 | | normf 30114 |
. . . . . . . . . . . . . . 15
β’
normβ: ββΆβ |
19 | | ax-hilex 29990 |
. . . . . . . . . . . . . . 15
β’ β
β V |
20 | | fex 7180 |
. . . . . . . . . . . . . . 15
β’
((normβ: ββΆβ β§ β β
V) β normβ β V) |
21 | 18, 19, 20 | mp2an 691 |
. . . . . . . . . . . . . 14
β’
normβ β V |
22 | 21 | resex 5989 |
. . . . . . . . . . . . 13
β’
(normβ βΎ π») β V |
23 | 17, 22 | op1st 7933 |
. . . . . . . . . . . 12
β’
(1st ββ¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β©) = β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β© |
24 | 23 | fveq2i 6849 |
. . . . . . . . . . 11
β’
(1st β(1st ββ¨β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β©)) =
(1st ββ¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©) |
25 | | hilablo 30151 |
. . . . . . . . . . . . 13
β’
+β β AbelOp |
26 | | resexg 5987 |
. . . . . . . . . . . . 13
β’ (
+β β AbelOp β ( +β βΎ (π» Γ π»)) β V) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (
+β βΎ (π» Γ π»)) β V |
28 | | hvmulex 30002 |
. . . . . . . . . . . . 13
β’
Β·β β V |
29 | 28 | resex 5989 |
. . . . . . . . . . . 12
β’ (
Β·β βΎ (β Γ π»)) β V |
30 | 27, 29 | op1st 7933 |
. . . . . . . . . . 11
β’
(1st ββ¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©) = ( +β βΎ
(π» Γ π»)) |
31 | 24, 30 | eqtri 2761 |
. . . . . . . . . 10
β’
(1st β(1st ββ¨β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β©)) = (
+β βΎ (π» Γ π»)) |
32 | 16, 31 | eqtri 2761 |
. . . . . . . . 9
β’ (
+π£ ββ¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β©) = (
+β βΎ (π» Γ π»)) |
33 | 14, 32 | eqtri 2761 |
. . . . . . . 8
β’ (
+π£ βπ) = ( +β βΎ (π» Γ π»)) |
34 | 33 | dmeqi 5864 |
. . . . . . 7
β’ dom (
+π£ βπ) = dom ( +β βΎ
(π» Γ π»)) |
35 | | hhssp3.4 |
. . . . . . . . . 10
β’ π» β
β |
36 | | xpss12 5652 |
. . . . . . . . . 10
β’ ((π» β β β§ π» β β) β (π» Γ π») β ( β Γ
β)) |
37 | 35, 35, 36 | mp2an 691 |
. . . . . . . . 9
β’ (π» Γ π») β ( β Γ
β) |
38 | | ax-hfvadd 29991 |
. . . . . . . . . 10
β’
+β :( β Γ β)βΆ
β |
39 | 38 | fdmi 6684 |
. . . . . . . . 9
β’ dom
+β = ( β Γ β) |
40 | 37, 39 | sseqtrri 3985 |
. . . . . . . 8
β’ (π» Γ π») β dom
+β |
41 | | ssdmres 5964 |
. . . . . . . 8
β’ ((π» Γ π») β dom +β β
dom ( +β βΎ (π» Γ π»)) = (π» Γ π»)) |
42 | 40, 41 | mpbi 229 |
. . . . . . 7
β’ dom (
+β βΎ (π» Γ π»)) = (π» Γ π») |
43 | 34, 42 | eqtri 2761 |
. . . . . 6
β’ dom (
+π£ βπ) = (π» Γ π») |
44 | 43 | dmeqi 5864 |
. . . . 5
β’ dom dom (
+π£ βπ) = dom (π» Γ π») |
45 | | dmxpid 5889 |
. . . . 5
β’ dom
(π» Γ π») = π» |
46 | 44, 45 | eqtri 2761 |
. . . 4
β’ dom dom (
+π£ βπ) = π» |
47 | 12, 46 | eqtri 2761 |
. . 3
β’ ran (
+π£ βπ) = π» |
48 | 3, 47 | eqtri 2761 |
. 2
β’
(BaseSetβπ) =
π» |
49 | 48 | eqcomi 2742 |
1
β’ π» = (BaseSetβπ) |