Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. 2
β’ ((π΄ β π΅ β§ π΅ β (π΄ β¨β (spanβ{πΆ}))) β π΅ β (π΄ β¨β (spanβ{πΆ}))) |
2 | | pssss 4036 |
. . . 4
β’ (π΄ β π΅ β π΄ β π΅) |
3 | 2 | adantr 482 |
. . 3
β’ ((π΄ β π΅ β§ π΅ β (π΄ β¨β (spanβ{πΆ}))) β π΄ β π΅) |
4 | | pssnel 4410 |
. . . . . . 7
β’ (π΄ β π΅ β βπ₯(π₯ β π΅ β§ Β¬ π₯ β π΄)) |
5 | | ssel2 3921 |
. . . . . . . . . . . 12
β’ ((π΅ β (π΄ β¨β (spanβ{πΆ})) β§ π₯ β π΅) β π₯ β (π΄ β¨β (spanβ{πΆ}))) |
6 | | spansncv.1 |
. . . . . . . . . . . . . . . 16
β’ π΄ β
Cβ |
7 | | spansncv.3 |
. . . . . . . . . . . . . . . 16
β’ πΆ β β |
8 | 6, 7 | spansnji 30049 |
. . . . . . . . . . . . . . 15
β’ (π΄ +β
(spanβ{πΆ})) = (π΄ β¨β
(spanβ{πΆ})) |
9 | 8 | eleq2i 2828 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄ +β (spanβ{πΆ})) β π₯ β (π΄ β¨β (spanβ{πΆ}))) |
10 | 7 | spansnchi 29965 |
. . . . . . . . . . . . . . 15
β’
(spanβ{πΆ})
β Cβ |
11 | 6, 10 | chseli 29862 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄ +β (spanβ{πΆ})) β βπ¦ β π΄ βπ§ β (spanβ{πΆ})π₯ = (π¦ +β π§)) |
12 | 9, 11 | bitr3i 278 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄ β¨β (spanβ{πΆ})) β βπ¦ β π΄ βπ§ β (spanβ{πΆ})π₯ = (π¦ +β π§)) |
13 | | eleq1 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ = (π¦ +β π§) β (π₯ β π΅ β (π¦ +β π§) β π΅)) |
14 | 13 | biimpac 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π₯ β π΅ β§ π₯ = (π¦ +β π§)) β (π¦ +β π§) β π΅) |
15 | 2 | sselda 3926 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π΄ β π΅ β§ π¦ β π΄) β π¦ β π΅) |
16 | | spansncv.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ π΅ β
Cβ |
17 | 16 | chshii 29630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ π΅ β
Sβ |
18 | | shsubcl 29623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π΅ β
Sβ β§ (π¦ +β π§) β π΅ β§ π¦ β π΅) β ((π¦ +β π§) ββ π¦) β π΅) |
19 | 17, 18 | mp3an1 1448 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π¦ +β π§) β π΅ β§ π¦ β π΅) β ((π¦ +β π§) ββ π¦) β π΅) |
20 | 14, 15, 19 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π₯ β π΅ β§ π₯ = (π¦ +β π§)) β§ (π΄ β π΅ β§ π¦ β π΄)) β ((π¦ +β π§) ββ π¦) β π΅) |
21 | 20 | exp43 438 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β π΅ β (π₯ = (π¦ +β π§) β (π΄ β π΅ β (π¦ β π΄ β ((π¦ +β π§) ββ π¦) β π΅)))) |
22 | 21 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ β π΄ β (π₯ = (π¦ +β π§) β (π΄ β π΅ β (π₯ β π΅ β ((π¦ +β π§) ββ π¦) β π΅)))) |
23 | 22 | imp45 431 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β π΄ β§ (π₯ = (π¦ +β π§) β§ (π΄ β π΅ β§ π₯ β π΅))) β ((π¦ +β π§) ββ π¦) β π΅) |
24 | 6 | cheli 29635 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ β π΄ β π¦ β β) |
25 | 10 | cheli 29635 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π§ β (spanβ{πΆ}) β π§ β β) |
26 | | hvpncan2 29443 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β β β§ π§ β β) β ((π¦ +β π§) ββ
π¦) = π§) |
27 | 24, 25, 26 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β π΄ β§ π§ β (spanβ{πΆ})) β ((π¦ +β π§) ββ π¦) = π§) |
28 | 27 | eleq1d 2821 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β π΄ β§ π§ β (spanβ{πΆ})) β (((π¦ +β π§) ββ π¦) β π΅ β π§ β π΅)) |
29 | 23, 28 | syl5ib 245 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ β π΄ β§ π§ β (spanβ{πΆ})) β ((π¦ β π΄ β§ (π₯ = (π¦ +β π§) β§ (π΄ β π΅ β§ π₯ β π΅))) β π§ β π΅)) |
30 | 29 | imp 408 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ β π΄ β§ π§ β (spanβ{πΆ})) β§ (π¦ β π΄ β§ (π₯ = (π¦ +β π§) β§ (π΄ β π΅ β§ π₯ β π΅)))) β π§ β π΅) |
31 | 30 | anandis 676 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β π΄ β§ (π§ β (spanβ{πΆ}) β§ (π₯ = (π¦ +β π§) β§ (π΄ β π΅ β§ π₯ β π΅)))) β π§ β π΅) |
32 | 31 | exp45 440 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β π΄ β (π§ β (spanβ{πΆ}) β (π₯ = (π¦ +β π§) β ((π΄ β π΅ β§ π₯ β π΅) β π§ β π΅)))) |
33 | 32 | imp41 427 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β π΄ β§ π§ β (spanβ{πΆ})) β§ π₯ = (π¦ +β π§)) β§ (π΄ β π΅ β§ π₯ β π΅)) β π§ β π΅) |
34 | 33 | adantrr 715 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ β π΄ β§ π§ β (spanβ{πΆ})) β§ π₯ = (π¦ +β π§)) β§ ((π΄ β π΅ β§ π₯ β π΅) β§ Β¬ π₯ β π΄)) β π§ β π΅) |
35 | | oveq2 7311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ = 0β β
(π¦ +β
π§) = (π¦ +β
0β)) |
36 | | ax-hvaddid 29407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ β β β (π¦ +β
0β) = π¦) |
37 | 24, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β π΄ β (π¦ +β 0β) =
π¦) |
38 | 35, 37 | sylan9eqr 2798 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β π΄ β§ π§ = 0β) β (π¦ +β π§) = π¦) |
39 | 38 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β π΄ β§ π§ = 0β) β (π₯ = (π¦ +β π§) β π₯ = π¦)) |
40 | | eleq1a 2832 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β π΄ β (π₯ = π¦ β π₯ β π΄)) |
41 | 40 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β π΄ β§ π§ = 0β) β (π₯ = π¦ β π₯ β π΄)) |
42 | 39, 41 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β π΄ β§ π§ = 0β) β (π₯ = (π¦ +β π§) β π₯ β π΄)) |
43 | 42 | impancom 453 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β π΄ β§ π₯ = (π¦ +β π§)) β (π§ = 0β β π₯ β π΄)) |
44 | 43 | necon3bd 2955 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β π΄ β§ π₯ = (π¦ +β π§)) β (Β¬ π₯ β π΄ β π§ β 0β)) |
45 | 44 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π¦ β π΄ β§ π₯ = (π¦ +β π§)) β§ Β¬ π₯ β π΄) β π§ β 0β) |
46 | | spansnss 29974 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΅ β
Sβ β§ π§ β π΅) β (spanβ{π§}) β π΅) |
47 | 17, 46 | mpan 688 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ β π΅ β (spanβ{π§}) β π΅) |
48 | | spansneleq 29973 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΆ β β β§ π§ β 0β)
β (π§ β
(spanβ{πΆ}) β
(spanβ{π§}) =
(spanβ{πΆ}))) |
49 | 7, 48 | mpan 688 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ β 0β
β (π§ β
(spanβ{πΆ}) β
(spanβ{π§}) =
(spanβ{πΆ}))) |
50 | 49 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π§ β 0β β§
π§ β (spanβ{πΆ})) β (spanβ{π§}) = (spanβ{πΆ})) |
51 | 50 | sseq1d 3957 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π§ β 0β β§
π§ β (spanβ{πΆ})) β ((spanβ{π§}) β π΅ β (spanβ{πΆ}) β π΅)) |
52 | 47, 51 | syl5ib 245 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π§ β 0β β§
π§ β (spanβ{πΆ})) β (π§ β π΅ β (spanβ{πΆ}) β π΅)) |
53 | 52 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π§ β (spanβ{πΆ}) β§ π§ β 0β) β (π§ β π΅ β (spanβ{πΆ}) β π΅)) |
54 | 45, 53 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π§ β (spanβ{πΆ}) β§ ((π¦ β π΄ β§ π₯ = (π¦ +β π§)) β§ Β¬ π₯ β π΄)) β (π§ β π΅ β (spanβ{πΆ}) β π΅)) |
55 | 54 | exp44 439 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β (spanβ{πΆ}) β (π¦ β π΄ β (π₯ = (π¦ +β π§) β (Β¬ π₯ β π΄ β (π§ β π΅ β (spanβ{πΆ}) β π΅))))) |
56 | 55 | com12 32 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β π΄ β (π§ β (spanβ{πΆ}) β (π₯ = (π¦ +β π§) β (Β¬ π₯ β π΄ β (π§ β π΅ β (spanβ{πΆ}) β π΅))))) |
57 | 56 | imp41 427 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β π΄ β§ π§ β (spanβ{πΆ})) β§ π₯ = (π¦ +β π§)) β§ Β¬ π₯ β π΄) β (π§ β π΅ β (spanβ{πΆ}) β π΅)) |
58 | 57 | adantrl 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ β π΄ β§ π§ β (spanβ{πΆ})) β§ π₯ = (π¦ +β π§)) β§ ((π΄ β π΅ β§ π₯ β π΅) β§ Β¬ π₯ β π΄)) β (π§ β π΅ β (spanβ{πΆ}) β π΅)) |
59 | 34, 58 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ β π΄ β§ π§ β (spanβ{πΆ})) β§ π₯ = (π¦ +β π§)) β§ ((π΄ β π΅ β§ π₯ β π΅) β§ Β¬ π₯ β π΄)) β (spanβ{πΆ}) β π΅) |
60 | 59 | exp43 438 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π΄ β§ π§ β (spanβ{πΆ})) β (π₯ = (π¦ +β π§) β ((π΄ β π΅ β§ π₯ β π΅) β (Β¬ π₯ β π΄ β (spanβ{πΆ}) β π΅)))) |
61 | 60 | rexlimivv 3193 |
. . . . . . . . . . . . 13
β’
(βπ¦ β
π΄ βπ§ β (spanβ{πΆ})π₯ = (π¦ +β π§) β ((π΄ β π΅ β§ π₯ β π΅) β (Β¬ π₯ β π΄ β (spanβ{πΆ}) β π΅))) |
62 | 12, 61 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄ β¨β (spanβ{πΆ})) β ((π΄ β π΅ β§ π₯ β π΅) β (Β¬ π₯ β π΄ β (spanβ{πΆ}) β π΅))) |
63 | 5, 62 | syl 17 |
. . . . . . . . . . 11
β’ ((π΅ β (π΄ β¨β (spanβ{πΆ})) β§ π₯ β π΅) β ((π΄ β π΅ β§ π₯ β π΅) β (Β¬ π₯ β π΄ β (spanβ{πΆ}) β π΅))) |
64 | 63 | imp 408 |
. . . . . . . . . 10
β’ (((π΅ β (π΄ β¨β (spanβ{πΆ})) β§ π₯ β π΅) β§ (π΄ β π΅ β§ π₯ β π΅)) β (Β¬ π₯ β π΄ β (spanβ{πΆ}) β π΅)) |
65 | 64 | anandirs 677 |
. . . . . . . . 9
β’ (((π΅ β (π΄ β¨β (spanβ{πΆ})) β§ π΄ β π΅) β§ π₯ β π΅) β (Β¬ π₯ β π΄ β (spanβ{πΆ}) β π΅)) |
66 | 65 | expimpd 455 |
. . . . . . . 8
β’ ((π΅ β (π΄ β¨β (spanβ{πΆ})) β§ π΄ β π΅) β ((π₯ β π΅ β§ Β¬ π₯ β π΄) β (spanβ{πΆ}) β π΅)) |
67 | 66 | exlimdv 1934 |
. . . . . . 7
β’ ((π΅ β (π΄ β¨β (spanβ{πΆ})) β§ π΄ β π΅) β (βπ₯(π₯ β π΅ β§ Β¬ π₯ β π΄) β (spanβ{πΆ}) β π΅)) |
68 | 4, 67 | syl5 34 |
. . . . . 6
β’ ((π΅ β (π΄ β¨β (spanβ{πΆ})) β§ π΄ β π΅) β (π΄ β π΅ β (spanβ{πΆ}) β π΅)) |
69 | 68 | ex 414 |
. . . . 5
β’ (π΅ β (π΄ β¨β (spanβ{πΆ})) β (π΄ β π΅ β (π΄ β π΅ β (spanβ{πΆ}) β π΅))) |
70 | 69 | pm2.43d 53 |
. . . 4
β’ (π΅ β (π΄ β¨β (spanβ{πΆ})) β (π΄ β π΅ β (spanβ{πΆ}) β π΅)) |
71 | 70 | impcom 409 |
. . 3
β’ ((π΄ β π΅ β§ π΅ β (π΄ β¨β (spanβ{πΆ}))) β (spanβ{πΆ}) β π΅) |
72 | 6, 10, 16 | chlubii 29875 |
. . 3
β’ ((π΄ β π΅ β§ (spanβ{πΆ}) β π΅) β (π΄ β¨β (spanβ{πΆ})) β π΅) |
73 | 3, 71, 72 | syl2anc 585 |
. 2
β’ ((π΄ β π΅ β§ π΅ β (π΄ β¨β (spanβ{πΆ}))) β (π΄ β¨β (spanβ{πΆ})) β π΅) |
74 | 1, 73 | eqssd 3943 |
1
β’ ((π΄ β π΅ β§ π΅ β (π΄ β¨β (spanβ{πΆ}))) β π΅ = (π΄ β¨β (spanβ{πΆ}))) |