Step | Hyp | Ref
| Expression |
1 | | simplll 774 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β π΅) β§ π’ β π§) β§ π£ β (π β {(0gβπΉ)})) β π) |
2 | | eldifi 4087 |
. . . . . . . . . . . . . 14
β’ (π£ β (π β {(0gβπΉ)}) β π£ β π) |
3 | 2 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β π΅) β§ π’ β π§) β§ π£ β (π β {(0gβπΉ)})) β π£ β π) |
4 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π΅) β π§ β π΅) |
5 | 4 | sselda 3945 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π΅) β§ π’ β π§) β π’ β π΅) |
6 | 5 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β π΅) β§ π’ β π§) β§ π£ β (π β {(0gβπΉ)})) β π’ β π΅) |
7 | | lbspropd.s2 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) = (π₯( Β·π
βπΏ)π¦)) |
8 | 7 | oveqrspc2v 7385 |
. . . . . . . . . . . . 13
β’ ((π β§ (π£ β π β§ π’ β π΅)) β (π£( Β·π
βπΎ)π’) = (π£( Β·π
βπΏ)π’)) |
9 | 1, 3, 6, 8 | syl12anc 836 |
. . . . . . . . . . . 12
β’ ((((π β§ π§ β π΅) β§ π’ β π§) β§ π£ β (π β {(0gβπΉ)})) β (π£( Β·π
βπΎ)π’) = (π£( Β·π
βπΏ)π’)) |
10 | | lbspropd.b1 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ = (BaseβπΎ)) |
11 | | lbspropd.b2 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ = (BaseβπΏ)) |
12 | | lbspropd.w |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β π) |
13 | | lbspropd.p |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) |
14 | | lbspropd.s1 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) β π) |
15 | | lbspropd.p1 |
. . . . . . . . . . . . . . . 16
β’ (π β π = (BaseβπΉ)) |
16 | | lbspropd.f |
. . . . . . . . . . . . . . . . 17
β’ πΉ = (ScalarβπΎ) |
17 | 16 | fveq2i 6846 |
. . . . . . . . . . . . . . . 16
β’
(BaseβπΉ) =
(Baseβ(ScalarβπΎ)) |
18 | 15, 17 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
β’ (π β π = (Baseβ(ScalarβπΎ))) |
19 | | lbspropd.p2 |
. . . . . . . . . . . . . . . 16
β’ (π β π = (BaseβπΊ)) |
20 | | lbspropd.g |
. . . . . . . . . . . . . . . . 17
β’ πΊ = (ScalarβπΏ) |
21 | 20 | fveq2i 6846 |
. . . . . . . . . . . . . . . 16
β’
(BaseβπΊ) =
(Baseβ(ScalarβπΏ)) |
22 | 19, 21 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
β’ (π β π = (Baseβ(ScalarβπΏ))) |
23 | | lbspropd.v1 |
. . . . . . . . . . . . . . 15
β’ (π β πΎ β π) |
24 | | lbspropd.v2 |
. . . . . . . . . . . . . . 15
β’ (π β πΏ β π) |
25 | 10, 11, 12, 13, 14, 7, 18, 22, 23, 24 | lsppropd 20494 |
. . . . . . . . . . . . . 14
β’ (π β (LSpanβπΎ) = (LSpanβπΏ)) |
26 | 1, 25 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β π΅) β§ π’ β π§) β§ π£ β (π β {(0gβπΉ)})) β (LSpanβπΎ) = (LSpanβπΏ)) |
27 | 26 | fveq1d 6845 |
. . . . . . . . . . . 12
β’ ((((π β§ π§ β π΅) β§ π’ β π§) β§ π£ β (π β {(0gβπΉ)})) β ((LSpanβπΎ)β(π§ β {π’})) = ((LSpanβπΏ)β(π§ β {π’}))) |
28 | 9, 27 | eleq12d 2828 |
. . . . . . . . . . 11
β’ ((((π β§ π§ β π΅) β§ π’ β π§) β§ π£ β (π β {(0gβπΉ)})) β ((π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})) β (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})))) |
29 | 28 | notbid 318 |
. . . . . . . . . 10
β’ ((((π β§ π§ β π΅) β§ π’ β π§) β§ π£ β (π β {(0gβπΉ)})) β (Β¬ (π£(
Β·π βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})) β Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})))) |
30 | 29 | ralbidva 3169 |
. . . . . . . . 9
β’ (((π β§ π§ β π΅) β§ π’ β π§) β (βπ£ β (π β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})) β βπ£ β (π β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})))) |
31 | 15 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π΅) β§ π’ β π§) β π = (BaseβπΉ)) |
32 | 31 | difeq1d 4082 |
. . . . . . . . . 10
β’ (((π β§ π§ β π΅) β§ π’ β π§) β (π β {(0gβπΉ)}) = ((BaseβπΉ) β
{(0gβπΉ)})) |
33 | 32 | raleqdv 3312 |
. . . . . . . . 9
β’ (((π β§ π§ β π΅) β§ π’ β π§) β (βπ£ β (π β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})) β βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})))) |
34 | 19 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π΅) β§ π’ β π§) β π = (BaseβπΊ)) |
35 | | lbspropd.a |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΉ)π¦) = (π₯(+gβπΊ)π¦)) |
36 | 15, 19, 35 | grpidpropd 18522 |
. . . . . . . . . . . . 13
β’ (π β (0gβπΉ) = (0gβπΊ)) |
37 | 36 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π΅) β§ π’ β π§) β (0gβπΉ) = (0gβπΊ)) |
38 | 37 | sneqd 4599 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π΅) β§ π’ β π§) β {(0gβπΉ)} = {(0gβπΊ)}) |
39 | 34, 38 | difeq12d 4084 |
. . . . . . . . . 10
β’ (((π β§ π§ β π΅) β§ π’ β π§) β (π β {(0gβπΉ)}) = ((BaseβπΊ) β
{(0gβπΊ)})) |
40 | 39 | raleqdv 3312 |
. . . . . . . . 9
β’ (((π β§ π§ β π΅) β§ π’ β π§) β (βπ£ β (π β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})) β βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})))) |
41 | 30, 33, 40 | 3bitr3d 309 |
. . . . . . . 8
β’ (((π β§ π§ β π΅) β§ π’ β π§) β (βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})) β βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})))) |
42 | 41 | ralbidva 3169 |
. . . . . . 7
β’ ((π β§ π§ β π΅) β (βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})) β βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})))) |
43 | 42 | anbi2d 630 |
. . . . . 6
β’ ((π β§ π§ β π΅) β ((((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’}))) β (((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’}))))) |
44 | 43 | pm5.32da 580 |
. . . . 5
β’ (π β ((π§ β π΅ β§ (((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})))) β (π§ β π΅ β§ (((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})))))) |
45 | 10 | sseq2d 3977 |
. . . . . 6
β’ (π β (π§ β π΅ β π§ β (BaseβπΎ))) |
46 | 45 | anbi1d 631 |
. . . . 5
β’ (π β ((π§ β π΅ β§ (((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})))) β (π§ β (BaseβπΎ) β§ (((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})))))) |
47 | 11 | sseq2d 3977 |
. . . . . 6
β’ (π β (π§ β π΅ β π§ β (BaseβπΏ))) |
48 | 25 | fveq1d 6845 |
. . . . . . . 8
β’ (π β ((LSpanβπΎ)βπ§) = ((LSpanβπΏ)βπ§)) |
49 | 10, 11 | eqtr3d 2775 |
. . . . . . . 8
β’ (π β (BaseβπΎ) = (BaseβπΏ)) |
50 | 48, 49 | eqeq12d 2749 |
. . . . . . 7
β’ (π β (((LSpanβπΎ)βπ§) = (BaseβπΎ) β ((LSpanβπΏ)βπ§) = (BaseβπΏ))) |
51 | 50 | anbi1d 631 |
. . . . . 6
β’ (π β ((((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’}))) β (((LSpanβπΏ)βπ§) = (BaseβπΏ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’}))))) |
52 | 47, 51 | anbi12d 632 |
. . . . 5
β’ (π β ((π§ β π΅ β§ (((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})))) β (π§ β (BaseβπΏ) β§ (((LSpanβπΏ)βπ§) = (BaseβπΏ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})))))) |
53 | 44, 46, 52 | 3bitr3d 309 |
. . . 4
β’ (π β ((π§ β (BaseβπΎ) β§ (((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’})))) β (π§ β (BaseβπΏ) β§ (((LSpanβπΏ)βπ§) = (BaseβπΏ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’})))))) |
54 | | 3anass 1096 |
. . . 4
β’ ((π§ β (BaseβπΎ) β§ ((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’}))) β (π§ β (BaseβπΎ) β§ (((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’}))))) |
55 | | 3anass 1096 |
. . . 4
β’ ((π§ β (BaseβπΏ) β§ ((LSpanβπΏ)βπ§) = (BaseβπΏ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’}))) β (π§ β (BaseβπΏ) β§ (((LSpanβπΏ)βπ§) = (BaseβπΏ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’}))))) |
56 | 53, 54, 55 | 3bitr4g 314 |
. . 3
β’ (π β ((π§ β (BaseβπΎ) β§ ((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’}))) β (π§ β (BaseβπΏ) β§ ((LSpanβπΏ)βπ§) = (BaseβπΏ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’}))))) |
57 | | eqid 2733 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
58 | | eqid 2733 |
. . . . 5
β’ (
Β·π βπΎ) = ( Β·π
βπΎ) |
59 | | eqid 2733 |
. . . . 5
β’
(BaseβπΉ) =
(BaseβπΉ) |
60 | | eqid 2733 |
. . . . 5
β’
(LBasisβπΎ) =
(LBasisβπΎ) |
61 | | eqid 2733 |
. . . . 5
β’
(LSpanβπΎ) =
(LSpanβπΎ) |
62 | | eqid 2733 |
. . . . 5
β’
(0gβπΉ) = (0gβπΉ) |
63 | 57, 16, 58, 59, 60, 61, 62 | islbs 20552 |
. . . 4
β’ (πΎ β π β (π§ β (LBasisβπΎ) β (π§ β (BaseβπΎ) β§ ((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’}))))) |
64 | 23, 63 | syl 17 |
. . 3
β’ (π β (π§ β (LBasisβπΎ) β (π§ β (BaseβπΎ) β§ ((LSpanβπΎ)βπ§) = (BaseβπΎ) β§ βπ’ β π§ βπ£ β ((BaseβπΉ) β {(0gβπΉ)}) Β¬ (π£( Β·π
βπΎ)π’) β ((LSpanβπΎ)β(π§ β {π’}))))) |
65 | | eqid 2733 |
. . . . 5
β’
(BaseβπΏ) =
(BaseβπΏ) |
66 | | eqid 2733 |
. . . . 5
β’ (
Β·π βπΏ) = ( Β·π
βπΏ) |
67 | | eqid 2733 |
. . . . 5
β’
(BaseβπΊ) =
(BaseβπΊ) |
68 | | eqid 2733 |
. . . . 5
β’
(LBasisβπΏ) =
(LBasisβπΏ) |
69 | | eqid 2733 |
. . . . 5
β’
(LSpanβπΏ) =
(LSpanβπΏ) |
70 | | eqid 2733 |
. . . . 5
β’
(0gβπΊ) = (0gβπΊ) |
71 | 65, 20, 66, 67, 68, 69, 70 | islbs 20552 |
. . . 4
β’ (πΏ β π β (π§ β (LBasisβπΏ) β (π§ β (BaseβπΏ) β§ ((LSpanβπΏ)βπ§) = (BaseβπΏ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’}))))) |
72 | 24, 71 | syl 17 |
. . 3
β’ (π β (π§ β (LBasisβπΏ) β (π§ β (BaseβπΏ) β§ ((LSpanβπΏ)βπ§) = (BaseβπΏ) β§ βπ’ β π§ βπ£ β ((BaseβπΊ) β {(0gβπΊ)}) Β¬ (π£( Β·π
βπΏ)π’) β ((LSpanβπΏ)β(π§ β {π’}))))) |
73 | 56, 64, 72 | 3bitr4d 311 |
. 2
β’ (π β (π§ β (LBasisβπΎ) β π§ β (LBasisβπΏ))) |
74 | 73 | eqrdv 2731 |
1
β’ (π β (LBasisβπΎ) = (LBasisβπΏ)) |