Step | Hyp | Ref
| Expression |
1 | | mapdval2.h |
. . 3
β’ π» = (LHypβπΎ) |
2 | | mapdval2.u |
. . 3
β’ π = ((DVecHβπΎ)βπ) |
3 | | mapdval2.s |
. . 3
β’ π = (LSubSpβπ) |
4 | | mapdval2.f |
. . 3
β’ πΉ = (LFnlβπ) |
5 | | mapdval2.l |
. . 3
β’ πΏ = (LKerβπ) |
6 | | mapdval2.o |
. . 3
β’ π = ((ocHβπΎ)βπ) |
7 | | mapdval2.m |
. . 3
β’ π = ((mapdβπΎ)βπ) |
8 | | mapdval2.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
9 | | mapdval2.t |
. . 3
β’ (π β π β π) |
10 | | mapdval2.c |
. . 3
β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | mapdvalc 41013 |
. 2
β’ (π β (πβπ) = {π β πΆ β£ (πβ(πΏβπ)) β π}) |
12 | 1, 2, 8 | dvhlmod 40494 |
. . . . . . . . 9
β’ (π β π β LMod) |
13 | 12 | ad3antrrr 727 |
. . . . . . . 8
β’ ((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β π β LMod) |
14 | | simplr 766 |
. . . . . . . 8
β’ ((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β (πβ(πΏβπ)) β (LSAtomsβπ)) |
15 | | eqid 2726 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
16 | | mapdval2.n |
. . . . . . . . 9
β’ π = (LSpanβπ) |
17 | | eqid 2726 |
. . . . . . . . 9
β’
(LSAtomsβπ) =
(LSAtomsβπ) |
18 | 15, 16, 17 | islsati 38377 |
. . . . . . . 8
β’ ((π β LMod β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β βπ£ β (Baseβπ)(πβ(πΏβπ)) = (πβ{π£})) |
19 | 13, 14, 18 | syl2anc 583 |
. . . . . . 7
β’ ((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β βπ£ β (Baseβπ)(πβ(πΏβπ)) = (πβ{π£})) |
20 | | simprr 770 |
. . . . . . . . 9
β’
(((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β§ (π£ β (Baseβπ) β§ (πβ(πΏβπ)) = (πβ{π£}))) β (πβ(πΏβπ)) = (πβ{π£})) |
21 | | simplr 766 |
. . . . . . . . 9
β’
(((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β§ (π£ β (Baseβπ) β§ (πβ(πΏβπ)) = (πβ{π£}))) β (πβ(πΏβπ)) β π) |
22 | 20, 21 | eqsstrrd 4016 |
. . . . . . . 8
β’
(((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β§ (π£ β (Baseβπ) β§ (πβ(πΏβπ)) = (πβ{π£}))) β (πβ{π£}) β π) |
23 | 12 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π β πΆ) β π β LMod) |
24 | 23 | ad3antrrr 727 |
. . . . . . . . 9
β’
(((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β§ (π£ β (Baseβπ) β§ (πβ(πΏβπ)) = (πβ{π£}))) β π β LMod) |
25 | 9 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π β πΆ) β π β π) |
26 | 25 | ad3antrrr 727 |
. . . . . . . . 9
β’
(((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β§ (π£ β (Baseβπ) β§ (πβ(πΏβπ)) = (πβ{π£}))) β π β π) |
27 | | simprl 768 |
. . . . . . . . 9
β’
(((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β§ (π£ β (Baseβπ) β§ (πβ(πΏβπ)) = (πβ{π£}))) β π£ β (Baseβπ)) |
28 | 15, 3, 16, 24, 26, 27 | lspsnel5 20842 |
. . . . . . . 8
β’
(((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β§ (π£ β (Baseβπ) β§ (πβ(πΏβπ)) = (πβ{π£}))) β (π£ β π β (πβ{π£}) β π)) |
29 | 22, 28 | mpbird 257 |
. . . . . . 7
β’
(((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β§ (π£ β (Baseβπ) β§ (πβ(πΏβπ)) = (πβ{π£}))) β π£ β π) |
30 | 19, 29, 20 | reximssdv 3166 |
. . . . . 6
β’ ((((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β§ (πβ(πΏβπ)) β π) β βπ£ β π (πβ(πΏβπ)) = (πβ{π£})) |
31 | 30 | ex 412 |
. . . . 5
β’ (((π β§ π β πΆ) β§ (πβ(πΏβπ)) β (LSAtomsβπ)) β ((πβ(πΏβπ)) β π β βπ£ β π (πβ(πΏβπ)) = (πβ{π£}))) |
32 | | eqid 2726 |
. . . . . . . . . . 11
β’
(0gβπ) = (0gβπ) |
33 | 32, 3 | lss0cl 20794 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β (0gβπ) β π) |
34 | 12, 9, 33 | syl2anc 583 |
. . . . . . . . 9
β’ (π β (0gβπ) β π) |
35 | 34 | adantr 480 |
. . . . . . . 8
β’ ((π β§ (πβ(πΏβπ)) = {(0gβπ)}) β (0gβπ) β π) |
36 | | simpr 484 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΏβπ)) = {(0gβπ)}) β (πβ(πΏβπ)) = {(0gβπ)}) |
37 | 12 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΏβπ)) = {(0gβπ)}) β π β LMod) |
38 | 32, 16 | lspsn0 20855 |
. . . . . . . . . 10
β’ (π β LMod β (πβ{(0gβπ)}) =
{(0gβπ)}) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΏβπ)) = {(0gβπ)}) β (πβ{(0gβπ)}) =
{(0gβπ)}) |
40 | 36, 39 | eqtr4d 2769 |
. . . . . . . 8
β’ ((π β§ (πβ(πΏβπ)) = {(0gβπ)}) β (πβ(πΏβπ)) = (πβ{(0gβπ)})) |
41 | | sneq 4633 |
. . . . . . . . . 10
β’ (π£ = (0gβπ) β {π£} = {(0gβπ)}) |
42 | 41 | fveq2d 6889 |
. . . . . . . . 9
β’ (π£ = (0gβπ) β (πβ{π£}) = (πβ{(0gβπ)})) |
43 | 42 | rspceeqv 3628 |
. . . . . . . 8
β’
(((0gβπ) β π β§ (πβ(πΏβπ)) = (πβ{(0gβπ)})) β βπ£ β π (πβ(πΏβπ)) = (πβ{π£})) |
44 | 35, 40, 43 | syl2anc 583 |
. . . . . . 7
β’ ((π β§ (πβ(πΏβπ)) = {(0gβπ)}) β βπ£ β π (πβ(πΏβπ)) = (πβ{π£})) |
45 | 44 | adantlr 712 |
. . . . . 6
β’ (((π β§ π β πΆ) β§ (πβ(πΏβπ)) = {(0gβπ)}) β βπ£ β π (πβ(πΏβπ)) = (πβ{π£})) |
46 | 45 | a1d 25 |
. . . . 5
β’ (((π β§ π β πΆ) β§ (πβ(πΏβπ)) = {(0gβπ)}) β ((πβ(πΏβπ)) β π β βπ£ β π (πβ(πΏβπ)) = (πβ{π£}))) |
47 | 8 | adantr 480 |
. . . . . 6
β’ ((π β§ π β πΆ) β (πΎ β HL β§ π β π»)) |
48 | 10 | lcfl1lem 40875 |
. . . . . . . 8
β’ (π β πΆ β (π β πΉ β§ (πβ(πβ(πΏβπ))) = (πΏβπ))) |
49 | 48 | simplbi 497 |
. . . . . . 7
β’ (π β πΆ β π β πΉ) |
50 | 49 | adantl 481 |
. . . . . 6
β’ ((π β§ π β πΆ) β π β πΉ) |
51 | 1, 6, 2, 32, 17, 4, 5, 47, 50 | dochsat0 40841 |
. . . . 5
β’ ((π β§ π β πΆ) β ((πβ(πΏβπ)) β (LSAtomsβπ) β¨ (πβ(πΏβπ)) = {(0gβπ)})) |
52 | 31, 46, 51 | mpjaodan 955 |
. . . 4
β’ ((π β§ π β πΆ) β ((πβ(πΏβπ)) β π β βπ£ β π (πβ(πΏβπ)) = (πβ{π£}))) |
53 | | simp3 1135 |
. . . . . 6
β’ (((π β§ π β πΆ) β§ π£ β π β§ (πβ(πΏβπ)) = (πβ{π£})) β (πβ(πΏβπ)) = (πβ{π£})) |
54 | 23 | 3ad2ant1 1130 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ π£ β π β§ (πβ(πΏβπ)) = (πβ{π£})) β π β LMod) |
55 | 25 | 3ad2ant1 1130 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ π£ β π β§ (πβ(πΏβπ)) = (πβ{π£})) β π β π) |
56 | | simp2 1134 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ π£ β π β§ (πβ(πΏβπ)) = (πβ{π£})) β π£ β π) |
57 | 3, 16, 54, 55, 56 | lspsnel5a 20843 |
. . . . . 6
β’ (((π β§ π β πΆ) β§ π£ β π β§ (πβ(πΏβπ)) = (πβ{π£})) β (πβ{π£}) β π) |
58 | 53, 57 | eqsstrd 4015 |
. . . . 5
β’ (((π β§ π β πΆ) β§ π£ β π β§ (πβ(πΏβπ)) = (πβ{π£})) β (πβ(πΏβπ)) β π) |
59 | 58 | rexlimdv3a 3153 |
. . . 4
β’ ((π β§ π β πΆ) β (βπ£ β π (πβ(πΏβπ)) = (πβ{π£}) β (πβ(πΏβπ)) β π)) |
60 | 52, 59 | impbid 211 |
. . 3
β’ ((π β§ π β πΆ) β ((πβ(πΏβπ)) β π β βπ£ β π (πβ(πΏβπ)) = (πβ{π£}))) |
61 | 60 | rabbidva 3433 |
. 2
β’ (π β {π β πΆ β£ (πβ(πΏβπ)) β π} = {π β πΆ β£ βπ£ β π (πβ(πΏβπ)) = (πβ{π£})}) |
62 | 11, 61 | eqtrd 2766 |
1
β’ (π β (πβπ) = {π β πΆ β£ βπ£ β π (πβ(πΏβπ)) = (πβ{π£})}) |