Step |
Hyp |
Ref |
Expression |
1 |
|
hdmap14lem1.h |
โข ๐ป = ( LHyp โ ๐พ ) |
2 |
|
hdmap14lem1.u |
โข ๐ = ( ( DVecH โ ๐พ ) โ ๐ ) |
3 |
|
hdmap14lem1.v |
โข ๐ = ( Base โ ๐ ) |
4 |
|
hdmap14lem1.t |
โข ยท = ( ยท๐ โ ๐ ) |
5 |
|
hdmap14lem3.o |
โข 0 = ( 0g โ ๐ ) |
6 |
|
hdmap14lem1.r |
โข ๐
= ( Scalar โ ๐ ) |
7 |
|
hdmap14lem1.b |
โข ๐ต = ( Base โ ๐
) |
8 |
|
hdmap14lem1.z |
โข ๐ = ( 0g โ ๐
) |
9 |
|
hdmap14lem1.c |
โข ๐ถ = ( ( LCDual โ ๐พ ) โ ๐ ) |
10 |
|
hdmap14lem2.e |
โข โ = ( ยท๐ โ ๐ถ ) |
11 |
|
hdmap14lem1.l |
โข ๐ฟ = ( LSpan โ ๐ถ ) |
12 |
|
hdmap14lem2.p |
โข ๐ = ( Scalar โ ๐ถ ) |
13 |
|
hdmap14lem2.a |
โข ๐ด = ( Base โ ๐ ) |
14 |
|
hdmap14lem2.q |
โข ๐ = ( 0g โ ๐ ) |
15 |
|
hdmap14lem1.s |
โข ๐ = ( ( HDMap โ ๐พ ) โ ๐ ) |
16 |
|
hdmap14lem1.k |
โข ( ๐ โ ( ๐พ โ HL โง ๐ โ ๐ป ) ) |
17 |
|
hdmap14lem3.x |
โข ( ๐ โ ๐ โ ( ๐ โ { 0 } ) ) |
18 |
|
hdmap14lem1.f |
โข ( ๐ โ ๐น โ ( ๐ต โ { ๐ } ) ) |
19 |
|
eqid |
โข ( 0g โ ๐ถ ) = ( 0g โ ๐ถ ) |
20 |
|
eqid |
โข ( Base โ ๐ถ ) = ( Base โ ๐ถ ) |
21 |
1 2 16
|
dvhlmod |
โข ( ๐ โ ๐ โ LMod ) |
22 |
18
|
eldifad |
โข ( ๐ โ ๐น โ ๐ต ) |
23 |
17
|
eldifad |
โข ( ๐ โ ๐ โ ๐ ) |
24 |
3 6 4 7
|
lmodvscl |
โข ( ( ๐ โ LMod โง ๐น โ ๐ต โง ๐ โ ๐ ) โ ( ๐น ยท ๐ ) โ ๐ ) |
25 |
21 22 23 24
|
syl3anc |
โข ( ๐ โ ( ๐น ยท ๐ ) โ ๐ ) |
26 |
|
eldifsni |
โข ( ๐น โ ( ๐ต โ { ๐ } ) โ ๐น โ ๐ ) |
27 |
18 26
|
syl |
โข ( ๐ โ ๐น โ ๐ ) |
28 |
|
eldifsni |
โข ( ๐ โ ( ๐ โ { 0 } ) โ ๐ โ 0 ) |
29 |
17 28
|
syl |
โข ( ๐ โ ๐ โ 0 ) |
30 |
1 2 16
|
dvhlvec |
โข ( ๐ โ ๐ โ LVec ) |
31 |
3 4 6 7 8 5 30 22 23
|
lvecvsn0 |
โข ( ๐ โ ( ( ๐น ยท ๐ ) โ 0 โ ( ๐น โ ๐ โง ๐ โ 0 ) ) ) |
32 |
27 29 31
|
mpbir2and |
โข ( ๐ โ ( ๐น ยท ๐ ) โ 0 ) |
33 |
|
eldifsn |
โข ( ( ๐น ยท ๐ ) โ ( ๐ โ { 0 } ) โ ( ( ๐น ยท ๐ ) โ ๐ โง ( ๐น ยท ๐ ) โ 0 ) ) |
34 |
25 32 33
|
sylanbrc |
โข ( ๐ โ ( ๐น ยท ๐ ) โ ( ๐ โ { 0 } ) ) |
35 |
1 2 3 5 9 19 20 15 16 34
|
hdmapnzcl |
โข ( ๐ โ ( ๐ โ ( ๐น ยท ๐ ) ) โ ( ( Base โ ๐ถ ) โ { ( 0g โ ๐ถ ) } ) ) |
36 |
|
eldifsni |
โข ( ( ๐ โ ( ๐น ยท ๐ ) ) โ ( ( Base โ ๐ถ ) โ { ( 0g โ ๐ถ ) } ) โ ( ๐ โ ( ๐น ยท ๐ ) ) โ ( 0g โ ๐ถ ) ) |
37 |
35 36
|
syl |
โข ( ๐ โ ( ๐ โ ( ๐น ยท ๐ ) ) โ ( 0g โ ๐ถ ) ) |
38 |
37
|
adantr |
โข ( ( ๐ โง ๐ โ { ๐ } ) โ ( ๐ โ ( ๐น ยท ๐ ) ) โ ( 0g โ ๐ถ ) ) |
39 |
|
elsni |
โข ( ๐ โ { ๐ } โ ๐ = ๐ ) |
40 |
39
|
oveq1d |
โข ( ๐ โ { ๐ } โ ( ๐ โ ( ๐ โ ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) ) |
41 |
1 9 16
|
lcdlmod |
โข ( ๐ โ ๐ถ โ LMod ) |
42 |
1 2 3 9 20 15 16 23
|
hdmapcl |
โข ( ๐ โ ( ๐ โ ๐ ) โ ( Base โ ๐ถ ) ) |
43 |
20 12 10 14 19
|
lmod0vs |
โข ( ( ๐ถ โ LMod โง ( ๐ โ ๐ ) โ ( Base โ ๐ถ ) ) โ ( ๐ โ ( ๐ โ ๐ ) ) = ( 0g โ ๐ถ ) ) |
44 |
41 42 43
|
syl2anc |
โข ( ๐ โ ( ๐ โ ( ๐ โ ๐ ) ) = ( 0g โ ๐ถ ) ) |
45 |
40 44
|
sylan9eqr |
โข ( ( ๐ โง ๐ โ { ๐ } ) โ ( ๐ โ ( ๐ โ ๐ ) ) = ( 0g โ ๐ถ ) ) |
46 |
38 45
|
neeqtrrd |
โข ( ( ๐ โง ๐ โ { ๐ } ) โ ( ๐ โ ( ๐น ยท ๐ ) ) โ ( ๐ โ ( ๐ โ ๐ ) ) ) |
47 |
46
|
neneqd |
โข ( ( ๐ โง ๐ โ { ๐ } ) โ ยฌ ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) ) |
48 |
47
|
nrexdv |
โข ( ๐ โ ยฌ โ ๐ โ { ๐ } ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) ) |
49 |
|
reuun2 |
โข ( ยฌ โ ๐ โ { ๐ } ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) โ ( โ! ๐ โ ( ( ๐ด โ { ๐ } ) โช { ๐ } ) ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) โ โ! ๐ โ ( ๐ด โ { ๐ } ) ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) ) ) |
50 |
48 49
|
syl |
โข ( ๐ โ ( โ! ๐ โ ( ( ๐ด โ { ๐ } ) โช { ๐ } ) ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) โ โ! ๐ โ ( ๐ด โ { ๐ } ) ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) ) ) |
51 |
12 13 14
|
lmod0cl |
โข ( ๐ถ โ LMod โ ๐ โ ๐ด ) |
52 |
|
difsnid |
โข ( ๐ โ ๐ด โ ( ( ๐ด โ { ๐ } ) โช { ๐ } ) = ๐ด ) |
53 |
|
reueq1 |
โข ( ( ( ๐ด โ { ๐ } ) โช { ๐ } ) = ๐ด โ ( โ! ๐ โ ( ( ๐ด โ { ๐ } ) โช { ๐ } ) ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) โ โ! ๐ โ ๐ด ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) ) ) |
54 |
41 51 52 53
|
4syl |
โข ( ๐ โ ( โ! ๐ โ ( ( ๐ด โ { ๐ } ) โช { ๐ } ) ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) โ โ! ๐ โ ๐ด ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) ) ) |
55 |
50 54
|
bitr3d |
โข ( ๐ โ ( โ! ๐ โ ( ๐ด โ { ๐ } ) ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) โ โ! ๐ โ ๐ด ( ๐ โ ( ๐น ยท ๐ ) ) = ( ๐ โ ( ๐ โ ๐ ) ) ) ) |