Step | Hyp | Ref
| Expression |
1 | | sspval.h |
. 2
โข ๐ป = (SubSpโ๐) |
2 | | fveq2 6847 |
. . . . . . 7
โข (๐ข = ๐ โ ( +๐ฃ โ๐ข) = ( +๐ฃ
โ๐)) |
3 | | sspval.g |
. . . . . . 7
โข ๐บ = ( +๐ฃ
โ๐) |
4 | 2, 3 | eqtr4di 2795 |
. . . . . 6
โข (๐ข = ๐ โ ( +๐ฃ โ๐ข) = ๐บ) |
5 | 4 | sseq2d 3981 |
. . . . 5
โข (๐ข = ๐ โ (( +๐ฃ
โ๐ค) โ (
+๐ฃ โ๐ข) โ ( +๐ฃ โ๐ค) โ ๐บ)) |
6 | | fveq2 6847 |
. . . . . . 7
โข (๐ข = ๐ โ (
ยท๐ OLD โ๐ข) = ( ยท๐ OLD
โ๐)) |
7 | | sspval.s |
. . . . . . 7
โข ๐ = (
ยท๐ OLD โ๐) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . 6
โข (๐ข = ๐ โ (
ยท๐ OLD โ๐ข) = ๐) |
9 | 8 | sseq2d 3981 |
. . . . 5
โข (๐ข = ๐ โ ((
ยท๐ OLD โ๐ค) โ (
ยท๐ OLD โ๐ข) โ (
ยท๐ OLD โ๐ค) โ ๐)) |
10 | | fveq2 6847 |
. . . . . . 7
โข (๐ข = ๐ โ (normCVโ๐ข) =
(normCVโ๐)) |
11 | | sspval.n |
. . . . . . 7
โข ๐ =
(normCVโ๐) |
12 | 10, 11 | eqtr4di 2795 |
. . . . . 6
โข (๐ข = ๐ โ (normCVโ๐ข) = ๐) |
13 | 12 | sseq2d 3981 |
. . . . 5
โข (๐ข = ๐ โ ((normCVโ๐ค) โ
(normCVโ๐ข)
โ (normCVโ๐ค) โ ๐)) |
14 | 5, 9, 13 | 3anbi123d 1437 |
. . . 4
โข (๐ข = ๐ โ ((( +๐ฃ
โ๐ค) โ (
+๐ฃ โ๐ข) โง (
ยท๐ OLD โ๐ค) โ (
ยท๐ OLD โ๐ข) โง (normCVโ๐ค) โ
(normCVโ๐ข)) โ (( +๐ฃ
โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ โง (normCVโ๐ค) โ ๐))) |
15 | 14 | rabbidv 3418 |
. . 3
โข (๐ข = ๐ โ {๐ค โ NrmCVec โฃ ((
+๐ฃ โ๐ค) โ ( +๐ฃ
โ๐ข) โง (
ยท๐ OLD โ๐ค) โ (
ยท๐ OLD โ๐ข) โง (normCVโ๐ค) โ
(normCVโ๐ข))} = {๐ค โ NrmCVec โฃ ((
+๐ฃ โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ โง (normCVโ๐ค) โ ๐)}) |
16 | | df-ssp 29706 |
. . 3
โข SubSp =
(๐ข โ NrmCVec โฆ
{๐ค โ NrmCVec โฃ
(( +๐ฃ โ๐ค) โ ( +๐ฃ
โ๐ข) โง (
ยท๐ OLD โ๐ค) โ (
ยท๐ OLD โ๐ข) โง (normCVโ๐ค) โ
(normCVโ๐ข))}) |
17 | 3 | fvexi 6861 |
. . . . . . 7
โข ๐บ โ V |
18 | 17 | pwex 5340 |
. . . . . 6
โข ๐ซ
๐บ โ V |
19 | 7 | fvexi 6861 |
. . . . . . 7
โข ๐ โ V |
20 | 19 | pwex 5340 |
. . . . . 6
โข ๐ซ
๐ โ V |
21 | 18, 20 | xpex 7692 |
. . . . 5
โข
(๐ซ ๐บ ร
๐ซ ๐) โ
V |
22 | 11 | fvexi 6861 |
. . . . . 6
โข ๐ โ V |
23 | 22 | pwex 5340 |
. . . . 5
โข ๐ซ
๐ โ V |
24 | 21, 23 | xpex 7692 |
. . . 4
โข
((๐ซ ๐บ
ร ๐ซ ๐)
ร ๐ซ ๐) โ
V |
25 | | rabss 4034 |
. . . . 5
โข ({๐ค โ NrmCVec โฃ ((
+๐ฃ โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ โง (normCVโ๐ค) โ ๐)} โ ((๐ซ ๐บ ร ๐ซ ๐) ร ๐ซ ๐) โ โ๐ค โ NrmCVec ((( +๐ฃ
โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ โง (normCVโ๐ค) โ ๐) โ ๐ค โ ((๐ซ ๐บ ร ๐ซ ๐) ร ๐ซ ๐))) |
26 | | fvex 6860 |
. . . . . . . . . 10
โข (
+๐ฃ โ๐ค) โ V |
27 | 26 | elpw 4569 |
. . . . . . . . 9
โข ((
+๐ฃ โ๐ค) โ ๐ซ ๐บ โ ( +๐ฃ โ๐ค) โ ๐บ) |
28 | | fvex 6860 |
. . . . . . . . . 10
โข (
ยท๐ OLD โ๐ค) โ V |
29 | 28 | elpw 4569 |
. . . . . . . . 9
โข ((
ยท๐ OLD โ๐ค) โ ๐ซ ๐ โ (
ยท๐ OLD โ๐ค) โ ๐) |
30 | | opelxpi 5675 |
. . . . . . . . 9
โข (((
+๐ฃ โ๐ค) โ ๐ซ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ซ ๐) โ โจ( +๐ฃ
โ๐ค), (
ยท๐ OLD โ๐ค)โฉ โ (๐ซ ๐บ ร ๐ซ ๐)) |
31 | 27, 29, 30 | syl2anbr 600 |
. . . . . . . 8
โข (((
+๐ฃ โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐) โ โจ( +๐ฃ
โ๐ค), (
ยท๐ OLD โ๐ค)โฉ โ (๐ซ ๐บ ร ๐ซ ๐)) |
32 | | fvex 6860 |
. . . . . . . . . 10
โข
(normCVโ๐ค) โ V |
33 | 32 | elpw 4569 |
. . . . . . . . 9
โข
((normCVโ๐ค) โ ๐ซ ๐ โ (normCVโ๐ค) โ ๐) |
34 | 33 | biimpri 227 |
. . . . . . . 8
โข
((normCVโ๐ค) โ ๐ โ (normCVโ๐ค) โ ๐ซ ๐) |
35 | | opelxpi 5675 |
. . . . . . . 8
โข ((โจ(
+๐ฃ โ๐ค), ( ยท๐ OLD
โ๐ค)โฉ โ
(๐ซ ๐บ ร
๐ซ ๐) โง
(normCVโ๐ค)
โ ๐ซ ๐) โ
โจโจ( +๐ฃ โ๐ค), ( ยท๐ OLD
โ๐ค)โฉ,
(normCVโ๐ค)โฉ โ ((๐ซ ๐บ ร ๐ซ ๐) ร ๐ซ ๐)) |
36 | 31, 34, 35 | syl2an 597 |
. . . . . . 7
โข ((((
+๐ฃ โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐) โง (normCVโ๐ค) โ ๐) โ โจโจ( +๐ฃ
โ๐ค), (
ยท๐ OLD โ๐ค)โฉ, (normCVโ๐ค)โฉ โ ((๐ซ ๐บ ร ๐ซ ๐) ร ๐ซ ๐)) |
37 | 36 | 3impa 1111 |
. . . . . 6
โข (((
+๐ฃ โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ โง (normCVโ๐ค) โ ๐) โ โจโจ( +๐ฃ
โ๐ค), (
ยท๐ OLD โ๐ค)โฉ, (normCVโ๐ค)โฉ โ ((๐ซ ๐บ ร ๐ซ ๐) ร ๐ซ ๐)) |
38 | | eqid 2737 |
. . . . . . . 8
โข (
+๐ฃ โ๐ค) = ( +๐ฃ โ๐ค) |
39 | | eqid 2737 |
. . . . . . . 8
โข (
ยท๐ OLD โ๐ค) = ( ยท๐ OLD
โ๐ค) |
40 | | eqid 2737 |
. . . . . . . 8
โข
(normCVโ๐ค) = (normCVโ๐ค) |
41 | 38, 39, 40 | nvop 29660 |
. . . . . . 7
โข (๐ค โ NrmCVec โ ๐ค = โจโจ(
+๐ฃ โ๐ค), ( ยท๐ OLD
โ๐ค)โฉ,
(normCVโ๐ค)โฉ) |
42 | 41 | eleq1d 2823 |
. . . . . 6
โข (๐ค โ NrmCVec โ (๐ค โ ((๐ซ ๐บ ร ๐ซ ๐) ร ๐ซ ๐) โ โจโจ(
+๐ฃ โ๐ค), ( ยท๐ OLD
โ๐ค)โฉ,
(normCVโ๐ค)โฉ โ ((๐ซ ๐บ ร ๐ซ ๐) ร ๐ซ ๐))) |
43 | 37, 42 | syl5ibr 246 |
. . . . 5
โข (๐ค โ NrmCVec โ (((
+๐ฃ โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ โง (normCVโ๐ค) โ ๐) โ ๐ค โ ((๐ซ ๐บ ร ๐ซ ๐) ร ๐ซ ๐))) |
44 | 25, 43 | mprgbir 3072 |
. . . 4
โข {๐ค โ NrmCVec โฃ ((
+๐ฃ โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ โง (normCVโ๐ค) โ ๐)} โ ((๐ซ ๐บ ร ๐ซ ๐) ร ๐ซ ๐) |
45 | 24, 44 | ssexi 5284 |
. . 3
โข {๐ค โ NrmCVec โฃ ((
+๐ฃ โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ โง (normCVโ๐ค) โ ๐)} โ V |
46 | 15, 16, 45 | fvmpt 6953 |
. 2
โข (๐ โ NrmCVec โ
(SubSpโ๐) = {๐ค โ NrmCVec โฃ ((
+๐ฃ โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ โง (normCVโ๐ค) โ ๐)}) |
47 | 1, 46 | eqtrid 2789 |
1
โข (๐ โ NrmCVec โ ๐ป = {๐ค โ NrmCVec โฃ ((
+๐ฃ โ๐ค) โ ๐บ โง (
ยท๐ OLD โ๐ค) โ ๐ โง (normCVโ๐ค) โ ๐)}) |