Step | Hyp | Ref
| Expression |
1 | | hhsst.1 |
. . . 4
β’ π = β¨β¨
+β , Β·β β©,
normββ© |
2 | | hhsst.2 |
. . . 4
β’ π = β¨β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© |
3 | 1, 2 | hhsst 30550 |
. . 3
β’ (π» β
Sβ β π β (SubSpβπ)) |
4 | | shss 30494 |
. . 3
β’ (π» β
Sβ β π» β β) |
5 | 3, 4 | jca 513 |
. 2
β’ (π» β
Sβ β (π β (SubSpβπ) β§ π» β β)) |
6 | | eleq1 2822 |
. . 3
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β (π» β Sβ
β if((π β
(SubSpβπ) β§ π» β β), π», β) β
Sβ )) |
7 | | eqid 2733 |
. . . 4
β’
β¨β¨( +β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π», β))β© =
β¨β¨( +β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π»,
β))β© |
8 | | xpeq1 5691 |
. . . . . . . . . . . . 13
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β (π» Γ π») = (if((π β (SubSpβπ) β§ π» β β), π», β) Γ π»)) |
9 | | xpeq2 5698 |
. . . . . . . . . . . . 13
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β (if((π β (SubSpβπ) β§ π» β β), π», β) Γ π») = (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))) |
10 | 8, 9 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β (π» Γ π») = (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))) |
11 | 10 | reseq2d 5982 |
. . . . . . . . . . 11
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β ( +β
βΎ (π» Γ π»)) = ( +β
βΎ (if((π β
(SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β)))) |
12 | | xpeq2 5698 |
. . . . . . . . . . . 12
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β (β Γ π») = (β Γ if((π β (SubSpβπ) β§ π» β β), π», β))) |
13 | 12 | reseq2d 5982 |
. . . . . . . . . . 11
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β (
Β·β βΎ (β Γ π»)) = ( Β·β
βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))) |
14 | 11, 13 | opeq12d 4882 |
. . . . . . . . . 10
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β© = β¨( +β
βΎ (if((π β
(SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©) |
15 | | reseq2 5977 |
. . . . . . . . . 10
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β (normβ
βΎ π») =
(normβ βΎ if((π β (SubSpβπ) β§ π» β β), π», β))) |
16 | 14, 15 | opeq12d 4882 |
. . . . . . . . 9
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β β¨β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© = β¨β¨(
+β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π»,
β))β©) |
17 | 2, 16 | eqtrid 2785 |
. . . . . . . 8
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β π = β¨β¨( +β
βΎ (if((π β
(SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π»,
β))β©) |
18 | 17 | eleq1d 2819 |
. . . . . . 7
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β (π β (SubSpβπ) β β¨β¨( +β
βΎ (if((π β
(SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π», β))β© β
(SubSpβπ))) |
19 | | sseq1 4008 |
. . . . . . 7
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β (π» β β β if((π β (SubSpβπ) β§ π» β β), π», β) β
β)) |
20 | 18, 19 | anbi12d 632 |
. . . . . 6
β’ (π» = if((π β (SubSpβπ) β§ π» β β), π», β) β ((π β (SubSpβπ) β§ π» β β) β (β¨β¨(
+β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π», β))β© β
(SubSpβπ) β§
if((π β
(SubSpβπ) β§ π» β β), π», β) β
β))) |
21 | | xpeq1 5691 |
. . . . . . . . . . . 12
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β ( β
Γ β) = (if((π
β (SubSpβπ)
β§ π» β β),
π», β) Γ
β)) |
22 | | xpeq2 5698 |
. . . . . . . . . . . 12
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β (if((π β (SubSpβπ) β§ π» β β), π», β) Γ β) = (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))) |
23 | 21, 22 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β ( β
Γ β) = (if((π
β (SubSpβπ)
β§ π» β β),
π», β) Γ
if((π β
(SubSpβπ) β§ π» β β), π», β))) |
24 | 23 | reseq2d 5982 |
. . . . . . . . . 10
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β (
+β βΎ ( β Γ β)) = (
+β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β)))) |
25 | | xpeq2 5698 |
. . . . . . . . . . 11
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β (β
Γ β) = (β Γ if((π β (SubSpβπ) β§ π» β β), π», β))) |
26 | 25 | reseq2d 5982 |
. . . . . . . . . 10
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β (
Β·β βΎ (β Γ β)) = (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))) |
27 | 24, 26 | opeq12d 4882 |
. . . . . . . . 9
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β β¨(
+β βΎ ( β Γ β)), (
Β·β βΎ (β Γ β))β© =
β¨( +β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©) |
28 | | reseq2 5977 |
. . . . . . . . 9
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β
(normβ βΎ β) = (normβ βΎ
if((π β
(SubSpβπ) β§ π» β β), π», β))) |
29 | 27, 28 | opeq12d 4882 |
. . . . . . . 8
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β β¨β¨(
+β βΎ ( β Γ β)), (
Β·β βΎ (β Γ β))β©,
(normβ βΎ β)β© = β¨β¨(
+β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π»,
β))β©) |
30 | 29 | eleq1d 2819 |
. . . . . . 7
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β (β¨β¨(
+β βΎ ( β Γ β)), (
Β·β βΎ (β Γ β))β©,
(normβ βΎ β)β© β (SubSpβπ) β β¨β¨(
+β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π», β))β© β
(SubSpβπ))) |
31 | | sseq1 4008 |
. . . . . . 7
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β ( β
β β β if((π β (SubSpβπ) β§ π» β β), π», β) β
β)) |
32 | 30, 31 | anbi12d 632 |
. . . . . 6
β’ ( β
= if((π β
(SubSpβπ) β§ π» β β), π», β) β
((β¨β¨( +β βΎ ( β Γ β)), (
Β·β βΎ (β Γ β))β©,
(normβ βΎ β)β© β (SubSpβπ) β§ β β β)
β (β¨β¨( +β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π», β))β© β
(SubSpβπ) β§
if((π β
(SubSpβπ) β§ π» β β), π», β) β
β))) |
33 | | ax-hfvadd 30284 |
. . . . . . . . . . . 12
β’
+β :( β Γ β)βΆ
β |
34 | | ffn 6718 |
. . . . . . . . . . . 12
β’ (
+β :( β Γ β)βΆ β β
+β Fn ( β Γ β)) |
35 | | fnresdm 6670 |
. . . . . . . . . . . 12
β’ (
+β Fn ( β Γ β) β (
+β βΎ ( β Γ β)) = +β
) |
36 | 33, 34, 35 | mp2b 10 |
. . . . . . . . . . 11
β’ (
+β βΎ ( β Γ β)) =
+β |
37 | | ax-hfvmul 30289 |
. . . . . . . . . . . 12
β’
Β·β :(β Γ β)βΆ
β |
38 | | ffn 6718 |
. . . . . . . . . . . 12
β’ (
Β·β :(β Γ β)βΆ β
β Β·β Fn (β Γ
β)) |
39 | | fnresdm 6670 |
. . . . . . . . . . . 12
β’ (
Β·β Fn (β Γ β) β (
Β·β βΎ (β Γ β)) =
Β·β ) |
40 | 37, 38, 39 | mp2b 10 |
. . . . . . . . . . 11
β’ (
Β·β βΎ (β Γ β)) =
Β·β |
41 | 36, 40 | opeq12i 4879 |
. . . . . . . . . 10
β’ β¨(
+β βΎ ( β Γ β)), (
Β·β βΎ (β Γ β))β© =
β¨ +β , Β·β
β© |
42 | | normf 30407 |
. . . . . . . . . . 11
β’
normβ: ββΆβ |
43 | | ffn 6718 |
. . . . . . . . . . 11
β’
(normβ: ββΆβ β
normβ Fn β) |
44 | | fnresdm 6670 |
. . . . . . . . . . 11
β’
(normβ Fn β β (normβ
βΎ β) = normβ) |
45 | 42, 43, 44 | mp2b 10 |
. . . . . . . . . 10
β’
(normβ βΎ β) =
normβ |
46 | 41, 45 | opeq12i 4879 |
. . . . . . . . 9
β’
β¨β¨( +β βΎ ( β Γ β)),
( Β·β βΎ (β Γ β))β©,
(normβ βΎ β)β© = β¨β¨
+β , Β·β β©,
normββ© |
47 | 46, 1 | eqtr4i 2764 |
. . . . . . . 8
β’
β¨β¨( +β βΎ ( β Γ β)),
( Β·β βΎ (β Γ β))β©,
(normβ βΎ β)β© = π |
48 | 1 | hhnv 30449 |
. . . . . . . . 9
β’ π β NrmCVec |
49 | | eqid 2733 |
. . . . . . . . . 10
β’
(SubSpβπ) =
(SubSpβπ) |
50 | 49 | sspid 30009 |
. . . . . . . . 9
β’ (π β NrmCVec β π β (SubSpβπ)) |
51 | 48, 50 | ax-mp 5 |
. . . . . . . 8
β’ π β (SubSpβπ) |
52 | 47, 51 | eqeltri 2830 |
. . . . . . 7
β’
β¨β¨( +β βΎ ( β Γ β)),
( Β·β βΎ (β Γ β))β©,
(normβ βΎ β)β© β (SubSpβπ) |
53 | | ssid 4005 |
. . . . . . 7
β’ β
β β |
54 | 52, 53 | pm3.2i 472 |
. . . . . 6
β’
(β¨β¨( +β βΎ ( β Γ β)),
( Β·β βΎ (β Γ β))β©,
(normβ βΎ β)β© β (SubSpβπ) β§ β β
β) |
55 | 20, 32, 54 | elimhyp 4594 |
. . . . 5
β’
(β¨β¨( +β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π», β))β© β
(SubSpβπ) β§
if((π β
(SubSpβπ) β§ π» β β), π», β) β
β) |
56 | 55 | simpli 485 |
. . . 4
β’
β¨β¨( +β βΎ (if((π β (SubSpβπ) β§ π» β β), π», β) Γ if((π β (SubSpβπ) β§ π» β β), π», β))), (
Β·β βΎ (β Γ if((π β (SubSpβπ) β§ π» β β), π», β)))β©, (normβ
βΎ if((π β
(SubSpβπ) β§ π» β β), π», β))β© β
(SubSpβπ) |
57 | 55 | simpri 487 |
. . . 4
β’ if((π β (SubSpβπ) β§ π» β β), π», β) β β |
58 | 1, 7, 56, 57 | hhshsslem2 30552 |
. . 3
β’ if((π β (SubSpβπ) β§ π» β β), π», β) β
Sβ |
59 | 6, 58 | dedth 4587 |
. 2
β’ ((π β (SubSpβπ) β§ π» β β) β π» β Sβ
) |
60 | 5, 59 | impbii 208 |
1
β’ (π» β
Sβ β (π β (SubSpβπ) β§ π» β β)) |