Step | Hyp | Ref
| Expression |
1 | | mapdval4.h |
. . 3
β’ π» = (LHypβπΎ) |
2 | | mapdval4.u |
. . 3
β’ π = ((DVecHβπΎ)βπ) |
3 | | mapdval4.s |
. . 3
β’ π = (LSubSpβπ) |
4 | | eqid 2732 |
. . 3
β’
(LSpanβπ) =
(LSpanβπ) |
5 | | mapdval4.f |
. . 3
β’ πΉ = (LFnlβπ) |
6 | | mapdval4.l |
. . 3
β’ πΏ = (LKerβπ) |
7 | | mapdval4.o |
. . 3
β’ π = ((ocHβπΎ)βπ) |
8 | | mapdval4.m |
. . 3
β’ π = ((mapdβπΎ)βπ) |
9 | | mapdval4.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
10 | | mapdval4.t |
. . 3
β’ (π β π β π) |
11 | | eqid 2732 |
. . 3
β’ {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | mapdval2N 40587 |
. 2
β’ (π β (πβπ) = {π β {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β£ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£})}) |
13 | 11 | lcfl1lem 40448 |
. . . . . 6
β’ (π β {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β (π β πΉ β§ (πβ(πβ(πΏβπ))) = (πΏβπ))) |
14 | 13 | anbi1i 624 |
. . . . 5
β’ ((π β {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β§ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£})) β ((π β πΉ β§ (πβ(πβ(πΏβπ))) = (πΏβπ)) β§ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) |
15 | | anass 469 |
. . . . 5
β’ (((π β πΉ β§ (πβ(πβ(πΏβπ))) = (πΏβπ)) β§ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£})) β (π β πΉ β§ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£})))) |
16 | 14, 15 | bitri 274 |
. . . 4
β’ ((π β {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β§ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£})) β (π β πΉ β§ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£})))) |
17 | | r19.42v 3190 |
. . . . . 6
β’
(βπ£ β
π ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£})) β ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) |
18 | | simprr 771 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) β (πβ(πΏβπ)) = ((LSpanβπ)β{π£})) |
19 | 18 | fveq2d 6895 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) β (πβ(πβ(πΏβπ))) = (πβ((LSpanβπ)β{π£}))) |
20 | | simprl 769 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) β (πβ(πβ(πΏβπ))) = (πΏβπ)) |
21 | | eqid 2732 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
22 | 9 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΉ) β (πΎ β HL β§ π β π»)) |
23 | 22 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π β πΉ) β§ π£ β π) β (πΎ β HL β§ π β π»)) |
24 | 23 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) β (πΎ β HL β§ π β π»)) |
25 | 10 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΉ) β π β π) |
26 | 21, 3 | lssel 20553 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π£ β π) β π£ β (Baseβπ)) |
27 | 25, 26 | sylan 580 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΉ) β§ π£ β π) β π£ β (Baseβπ)) |
28 | 27 | snssd 4812 |
. . . . . . . . . . 11
β’ (((π β§ π β πΉ) β§ π£ β π) β {π£} β (Baseβπ)) |
29 | 28 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) β {π£} β (Baseβπ)) |
30 | 1, 2, 7, 21, 4, 24, 29 | dochocsp 40336 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) β (πβ((LSpanβπ)β{π£})) = (πβ{π£})) |
31 | 19, 20, 30 | 3eqtr3rd 2781 |
. . . . . . . 8
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) β (πβ{π£}) = (πΏβπ)) |
32 | 27 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β π£ β (Baseβπ)) |
33 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β (πβ{π£}) = (πΏβπ)) |
34 | 33 | eqcomd 2738 |
. . . . . . . . . . 11
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β (πΏβπ) = (πβ{π£})) |
35 | | sneq 4638 |
. . . . . . . . . . . . 13
β’ (π€ = π£ β {π€} = {π£}) |
36 | 35 | fveq2d 6895 |
. . . . . . . . . . . 12
β’ (π€ = π£ β (πβ{π€}) = (πβ{π£})) |
37 | 36 | rspceeqv 3633 |
. . . . . . . . . . 11
β’ ((π£ β (Baseβπ) β§ (πΏβπ) = (πβ{π£})) β βπ€ β (Baseβπ)(πΏβπ) = (πβ{π€})) |
38 | 32, 34, 37 | syl2anc 584 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β βπ€ β (Baseβπ)(πΏβπ) = (πβ{π€})) |
39 | 23 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β (πΎ β HL β§ π β π»)) |
40 | | simpllr 774 |
. . . . . . . . . . 11
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β π β πΉ) |
41 | 1, 7, 2, 21, 5, 6,
39, 40 | lcfl8a 40460 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β ((πβ(πβ(πΏβπ))) = (πΏβπ) β βπ€ β (Baseβπ)(πΏβπ) = (πβ{π€}))) |
42 | 38, 41 | mpbird 256 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β (πβ(πβ(πΏβπ))) = (πΏβπ)) |
43 | 1, 2, 7, 21, 4, 23, 27 | dochocsn 40338 |
. . . . . . . . . . 11
β’ (((π β§ π β πΉ) β§ π£ β π) β (πβ(πβ{π£})) = ((LSpanβπ)β{π£})) |
44 | | fveq2 6891 |
. . . . . . . . . . 11
β’ ((πβ{π£}) = (πΏβπ) β (πβ(πβ{π£})) = (πβ(πΏβπ))) |
45 | 43, 44 | sylan9req 2793 |
. . . . . . . . . 10
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β ((LSpanβπ)β{π£}) = (πβ(πΏβπ))) |
46 | 45 | eqcomd 2738 |
. . . . . . . . 9
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β (πβ(πΏβπ)) = ((LSpanβπ)β{π£})) |
47 | 42, 46 | jca 512 |
. . . . . . . 8
β’ ((((π β§ π β πΉ) β§ π£ β π) β§ (πβ{π£}) = (πΏβπ)) β ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) |
48 | 31, 47 | impbida 799 |
. . . . . . 7
β’ (((π β§ π β πΉ) β§ π£ β π) β (((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£})) β (πβ{π£}) = (πΏβπ))) |
49 | 48 | rexbidva 3176 |
. . . . . 6
β’ ((π β§ π β πΉ) β (βπ£ β π ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) = ((LSpanβπ)β{π£})) β βπ£ β π (πβ{π£}) = (πΏβπ))) |
50 | 17, 49 | bitr3id 284 |
. . . . 5
β’ ((π β§ π β πΉ) β (((πβ(πβ(πΏβπ))) = (πΏβπ) β§ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£})) β βπ£ β π (πβ{π£}) = (πΏβπ))) |
51 | 50 | pm5.32da 579 |
. . . 4
β’ (π β ((π β πΉ β§ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£}))) β (π β πΉ β§ βπ£ β π (πβ{π£}) = (πΏβπ)))) |
52 | 16, 51 | bitrid 282 |
. . 3
β’ (π β ((π β {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β§ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£})) β (π β πΉ β§ βπ£ β π (πβ{π£}) = (πΏβπ)))) |
53 | 52 | rabbidva2 3434 |
. 2
β’ (π β {π β {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β£ βπ£ β π (πβ(πΏβπ)) = ((LSpanβπ)β{π£})} = {π β πΉ β£ βπ£ β π (πβ{π£}) = (πΏβπ)}) |
54 | 12, 53 | eqtrd 2772 |
1
β’ (π β (πβπ) = {π β πΉ β£ βπ£ β π (πβ{π£}) = (πΏβπ)}) |