Step | Hyp | Ref
| Expression |
1 | | hdmapval0.h |
. . 3
โข ๐ป = (LHypโ๐พ) |
2 | | hdmapval0.u |
. . 3
โข ๐ = ((DVecHโ๐พ)โ๐) |
3 | | eqid 2731 |
. . 3
โข
(Baseโ๐) =
(Baseโ๐) |
4 | | eqid 2731 |
. . 3
โข
(LSpanโ๐) =
(LSpanโ๐) |
5 | | hdmapval0.k |
. . 3
โข (๐ โ (๐พ โ HL โง ๐ โ ๐ป)) |
6 | | eqid 2731 |
. . . . 5
โข
(Baseโ๐พ) =
(Baseโ๐พ) |
7 | | eqid 2731 |
. . . . 5
โข
((LTrnโ๐พ)โ๐) = ((LTrnโ๐พ)โ๐) |
8 | | hdmapval0.o |
. . . . 5
โข 0 =
(0gโ๐) |
9 | | eqid 2731 |
. . . . 5
โข โจ( I
โพ (Baseโ๐พ)), (
I โพ ((LTrnโ๐พ)โ๐))โฉ = โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ |
10 | 1, 6, 7, 2, 3, 8, 9, 5 | dvheveccl 40287 |
. . . 4
โข (๐ โ โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ โ ((Baseโ๐) โ { 0 })) |
11 | 10 | eldifad 3960 |
. . 3
โข (๐ โ โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ โ (Baseโ๐)) |
12 | 1, 2, 5 | dvhlmod 40285 |
. . . 4
โข (๐ โ ๐ โ LMod) |
13 | 3, 8 | lmod0vcl 20646 |
. . . 4
โข (๐ โ LMod โ 0 โ
(Baseโ๐)) |
14 | 12, 13 | syl 17 |
. . 3
โข (๐ โ 0 โ (Baseโ๐)) |
15 | 1, 2, 3, 4, 5, 11,
14 | dvh3dim 40621 |
. 2
โข (๐ โ โ๐ฅ โ (Baseโ๐) ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) |
16 | | hdmapval0.c |
. . . . 5
โข ๐ถ = ((LCDualโ๐พ)โ๐) |
17 | | eqid 2731 |
. . . . 5
โข
(Baseโ๐ถ) =
(Baseโ๐ถ) |
18 | | eqid 2731 |
. . . . 5
โข
((HVMapโ๐พ)โ๐) = ((HVMapโ๐พ)โ๐) |
19 | | eqid 2731 |
. . . . 5
โข
((HDMap1โ๐พ)โ๐) = ((HDMap1โ๐พ)โ๐) |
20 | | hdmapval0.s |
. . . . 5
โข ๐ = ((HDMapโ๐พ)โ๐) |
21 | 5 | 3ad2ant1 1132 |
. . . . 5
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ (๐พ โ HL โง ๐ โ ๐ป)) |
22 | 14 | 3ad2ant1 1132 |
. . . . 5
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ 0 โ
(Baseโ๐)) |
23 | | simp2 1136 |
. . . . 5
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ ๐ฅ โ (Baseโ๐)) |
24 | | eqid 2731 |
. . . . . . . . . 10
โข
(LSubSpโ๐) =
(LSubSpโ๐) |
25 | 3, 24, 4, 12, 11, 14 | lspprcl 20734 |
. . . . . . . . . 10
โข (๐ โ ((LSpanโ๐)โ{โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ, 0 }) โ
(LSubSpโ๐)) |
26 | 3, 4, 12, 11, 14 | lspprid1 20753 |
. . . . . . . . . 10
โข (๐ โ โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ โ ((LSpanโ๐)โ{โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ, 0 })) |
27 | 24, 4, 12, 25, 26 | lspsnel5a 20752 |
. . . . . . . . 9
โข (๐ โ ((LSpanโ๐)โ{โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ}) โ ((LSpanโ๐)โ{โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ, 0 })) |
28 | 3, 4, 12, 11, 14 | lspprid2 20754 |
. . . . . . . . . 10
โข (๐ โ 0 โ ((LSpanโ๐)โ{โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ, 0 })) |
29 | 24, 4, 12, 25, 28 | lspsnel5a 20752 |
. . . . . . . . 9
โข (๐ โ ((LSpanโ๐)โ{ 0 }) โ
((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) |
30 | 27, 29 | unssd 4186 |
. . . . . . . 8
โข (๐ โ (((LSpanโ๐)โ{โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ}) โช ((LSpanโ๐)โ{ 0 })) โ
((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) |
31 | 30 | ssneld 3984 |
. . . . . . 7
โข (๐ โ (ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 }) โ ยฌ ๐ฅ โ (((LSpanโ๐)โ{โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ}) โช ((LSpanโ๐)โ{ 0 })))) |
32 | 31 | adantr 480 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (Baseโ๐)) โ (ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 }) โ ยฌ ๐ฅ โ (((LSpanโ๐)โ{โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ}) โช ((LSpanโ๐)โ{ 0 })))) |
33 | 32 | 3impia 1116 |
. . . . 5
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ ยฌ ๐ฅ โ (((LSpanโ๐)โ{โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ}) โช ((LSpanโ๐)โ{ 0 }))) |
34 | 1, 9, 2, 3, 4, 16,
17, 18, 19, 20, 21, 22, 23, 33 | hdmapval2 41007 |
. . . 4
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ (๐โ 0 ) = (((HDMap1โ๐พ)โ๐)โโจ๐ฅ, (((HDMap1โ๐พ)โ๐)โโจโจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ, (((HVMapโ๐พ)โ๐)โโจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ), ๐ฅโฉ), 0 โฉ)) |
35 | | hdmapval0.q |
. . . . 5
โข ๐ = (0gโ๐ถ) |
36 | | eqid 2731 |
. . . . . 6
โข
(LSpanโ๐ถ) =
(LSpanโ๐ถ) |
37 | | eqid 2731 |
. . . . . 6
โข
((mapdโ๐พ)โ๐) = ((mapdโ๐พ)โ๐) |
38 | 1, 2, 3, 8, 16, 17, 35, 18, 5, 10 | hvmapcl2 40941 |
. . . . . . . 8
โข (๐ โ (((HVMapโ๐พ)โ๐)โโจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ) โ
((Baseโ๐ถ) โ
{๐})) |
39 | 38 | eldifad 3960 |
. . . . . . 7
โข (๐ โ (((HVMapโ๐พ)โ๐)โโจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ) โ
(Baseโ๐ถ)) |
40 | 39 | 3ad2ant1 1132 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ
(((HVMapโ๐พ)โ๐)โโจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ) โ
(Baseโ๐ถ)) |
41 | 1, 2, 3, 8, 4, 16,
36, 37, 18, 5, 10 | mapdhvmap 40944 |
. . . . . . 7
โข (๐ โ (((mapdโ๐พ)โ๐)โ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ})) =
((LSpanโ๐ถ)โ{(((HVMapโ๐พ)โ๐)โโจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ)})) |
42 | 41 | 3ad2ant1 1132 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ
(((mapdโ๐พ)โ๐)โ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ})) =
((LSpanโ๐ถ)โ{(((HVMapโ๐พ)โ๐)โโจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ)})) |
43 | 1, 2, 5 | dvhlvec 40284 |
. . . . . . . . . 10
โข (๐ โ ๐ โ LVec) |
44 | 43 | 3ad2ant1 1132 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ ๐ โ LVec) |
45 | 11 | 3ad2ant1 1132 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ โจ( I
โพ (Baseโ๐พ)), (
I โพ ((LTrnโ๐พ)โ๐))โฉ โ (Baseโ๐)) |
46 | | simp3 1137 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ, 0 })) |
47 | 3, 4, 44, 23, 45, 22, 46 | lspindpi 20891 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ
(((LSpanโ๐)โ{๐ฅ}) โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ}) โง
((LSpanโ๐)โ{๐ฅ}) โ ((LSpanโ๐)โ{ 0 }))) |
48 | 47 | simpld 494 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ
((LSpanโ๐)โ{๐ฅ}) โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ})) |
49 | 48 | necomd 2995 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ
((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ}) โ
((LSpanโ๐)โ{๐ฅ})) |
50 | 10 | 3ad2ant1 1132 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ โจ( I
โพ (Baseโ๐พ)), (
I โพ ((LTrnโ๐พ)โ๐))โฉ โ ((Baseโ๐) โ { 0 })) |
51 | 1, 2, 3, 8, 4, 16,
17, 36, 37, 19, 21, 40, 42, 49, 50, 23 | hdmap1cl 40979 |
. . . . 5
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ
(((HDMap1โ๐พ)โ๐)โโจโจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ, (((HVMapโ๐พ)โ๐)โโจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ), ๐ฅโฉ) โ (Baseโ๐ถ)) |
52 | 1, 2, 3, 8, 16, 17, 35, 19, 21, 51, 23 | hdmap1val0 40974 |
. . . 4
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ
(((HDMap1โ๐พ)โ๐)โโจ๐ฅ, (((HDMap1โ๐พ)โ๐)โโจโจ( I โพ
(Baseโ๐พ)), ( I
โพ ((LTrnโ๐พ)โ๐))โฉ, (((HVMapโ๐พ)โ๐)โโจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ), ๐ฅโฉ), 0 โฉ) = ๐) |
53 | 34, 52 | eqtrd 2771 |
. . 3
โข ((๐ โง ๐ฅ โ (Baseโ๐) โง ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 })) โ (๐โ 0 ) = ๐) |
54 | 53 | rexlimdv3a 3158 |
. 2
โข (๐ โ (โ๐ฅ โ (Baseโ๐) ยฌ ๐ฅ โ ((LSpanโ๐)โ{โจ( I โพ (Baseโ๐พ)), ( I โพ
((LTrnโ๐พ)โ๐))โฉ, 0 }) โ (๐โ 0 ) = ๐)) |
55 | 15, 54 | mpd 15 |
1
โข (๐ โ (๐โ 0 ) = ๐) |