Step | Hyp | Ref
| Expression |
1 | | elin 3963 |
. . . 4
β’ (π¦ β ((π΅ +β (spanβ{πΆ})) β© π΄) β (π¦ β (π΅ +β (spanβ{πΆ})) β§ π¦ β π΄)) |
2 | | sumdmdi.2 |
. . . . . . . . 9
β’ π΅ β
Cβ |
3 | 2 | chshii 30747 |
. . . . . . . 8
β’ π΅ β
Sβ |
4 | | spansnsh 31081 |
. . . . . . . 8
β’ (πΆ β β β
(spanβ{πΆ}) β
Sβ ) |
5 | | shsel 30834 |
. . . . . . . 8
β’ ((π΅ β
Sβ β§ (spanβ{πΆ}) β Sβ
) β (π¦ β (π΅ +β
(spanβ{πΆ})) β
βπ§ β π΅ βπ€ β (spanβ{πΆ})π¦ = (π§ +β π€))) |
6 | 3, 4, 5 | sylancr 585 |
. . . . . . 7
β’ (πΆ β β β (π¦ β (π΅ +β (spanβ{πΆ})) β βπ§ β π΅ βπ€ β (spanβ{πΆ})π¦ = (π§ +β π€))) |
7 | | sumdmdi.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ π΄ β
Cβ |
8 | 7 | cheli 30752 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β π΄ β π¦ β β) |
9 | 2 | cheli 30752 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ β π΅ β π§ β β) |
10 | | elspansncl 31085 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΆ β β β§ π€ β (spanβ{πΆ})) β π€ β β) |
11 | | hvsubadd 30597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π¦ β β β§ π§ β β β§ π€ β β) β ((π¦ ββ
π§) = π€ β (π§ +β π€) = π¦)) |
12 | | eqcom 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π§ +β π€) = π¦ β π¦ = (π§ +β π€)) |
13 | 11, 12 | bitrdi 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β β β§ π§ β β β§ π€ β β) β ((π¦ ββ
π§) = π€ β π¦ = (π§ +β π€))) |
14 | 8, 9, 10, 13 | syl3an 1158 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β π΄ β§ π§ β π΅ β§ (πΆ β β β§ π€ β (spanβ{πΆ}))) β ((π¦ ββ π§) = π€ β π¦ = (π§ +β π€))) |
15 | 14 | 3expa 1116 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π¦ β π΄ β§ π§ β π΅) β§ (πΆ β β β§ π€ β (spanβ{πΆ}))) β ((π¦ ββ π§) = π€ β π¦ = (π§ +β π€))) |
16 | 7 | chshii 30747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ π΄ β
Sβ |
17 | 16, 3 | shsvsi 30887 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β π΄ β§ π§ β π΅) β (π¦ ββ π§) β (π΄ +β π΅)) |
18 | | eleq1 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ ββ
π§) = π€ β ((π¦ ββ π§) β (π΄ +β π΅) β π€ β (π΄ +β π΅))) |
19 | 17, 18 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β π΄ β§ π§ β π΅) β ((π¦ ββ π§) = π€ β π€ β (π΄ +β π΅))) |
20 | 19 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π¦ β π΄ β§ π§ β π΅) β§ (πΆ β β β§ π€ β (spanβ{πΆ}))) β ((π¦ ββ π§) = π€ β π€ β (π΄ +β π΅))) |
21 | 15, 20 | sylbird 259 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π¦ β π΄ β§ π§ β π΅) β§ (πΆ β β β§ π€ β (spanβ{πΆ}))) β (π¦ = (π§ +β π€) β π€ β (π΄ +β π΅))) |
22 | 21 | exp32 419 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β π΄ β§ π§ β π΅) β (πΆ β β β (π€ β (spanβ{πΆ}) β (π¦ = (π§ +β π€) β π€ β (π΄ +β π΅))))) |
23 | 22 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = (π§ +β π€) β ((π¦ β π΄ β§ π§ β π΅) β (πΆ β β β (π€ β (spanβ{πΆ}) β π€ β (π΄ +β π΅))))) |
24 | 23 | imp31 416 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ πΆ β β) β (π€ β (spanβ{πΆ}) β π€ β (π΄ +β π΅))) |
25 | 24 | adantrr 713 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ (πΆ β β β§ Β¬ πΆ β (π΄ +β π΅))) β (π€ β (spanβ{πΆ}) β π€ β (π΄ +β π΅))) |
26 | 16, 3 | shscli 30837 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ +β π΅) β
Sβ |
27 | | elspansn5 31094 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ +β π΅) β
Sβ β (((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β§ (π€ β (spanβ{πΆ}) β§ π€ β (π΄ +β π΅))) β π€ = 0β)) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β§ (π€ β (spanβ{πΆ}) β§ π€ β (π΄ +β π΅))) β π€ = 0β) |
29 | 28 | exp32 419 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β (π€ β (spanβ{πΆ}) β (π€ β (π΄ +β π΅) β π€ = 0β))) |
30 | 29 | adantl 480 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ (πΆ β β β§ Β¬ πΆ β (π΄ +β π΅))) β (π€ β (spanβ{πΆ}) β (π€ β (π΄ +β π΅) β π€ = 0β))) |
31 | 25, 30 | mpdd 43 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ (πΆ β β β§ Β¬ πΆ β (π΄ +β π΅))) β (π€ β (spanβ{πΆ}) β π€ = 0β)) |
32 | | oveq2 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ = 0β β
(π§ +β
π€) = (π§ +β
0β)) |
33 | | ax-hvaddid 30524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ β β β (π§ +β
0β) = π§) |
34 | 32, 33 | sylan9eqr 2792 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π§ β β β§ π€ = 0β) β
(π§ +β
π€) = π§) |
35 | 9, 34 | sylan 578 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π§ β π΅ β§ π€ = 0β) β (π§ +β π€) = π§) |
36 | 35 | eqeq2d 2741 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π§ β π΅ β§ π€ = 0β) β (π¦ = (π§ +β π€) β π¦ = π§)) |
37 | 36 | adantll 710 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π¦ β π΄ β§ π§ β π΅) β§ π€ = 0β) β (π¦ = (π§ +β π€) β π¦ = π§)) |
38 | 37 | biimpac 477 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ = (π§ +β π€) β§ ((π¦ β π΄ β§ π§ β π΅) β§ π€ = 0β)) β π¦ = π§) |
39 | | eleq1 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ = π§ β (π¦ β π΅ β π§ β π΅)) |
40 | 39 | biimparc 478 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π§ β π΅ β§ π¦ = π§) β π¦ β π΅) |
41 | | elin 3963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β (π΅ β© π΄) β (π¦ β π΅ β§ π¦ β π΄)) |
42 | 41 | biimpri 227 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β π΅ β§ π¦ β π΄) β π¦ β (π΅ β© π΄)) |
43 | 42 | ancoms 457 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β π΄ β§ π¦ β π΅) β π¦ β (π΅ β© π΄)) |
44 | 40, 43 | sylan2 591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β π΄ β§ (π§ β π΅ β§ π¦ = π§)) β π¦ β (π΅ β© π΄)) |
45 | 44 | expr 455 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β π΄ β§ π§ β π΅) β (π¦ = π§ β π¦ β (π΅ β© π΄))) |
46 | 45 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ = (π§ +β π€) β§ ((π¦ β π΄ β§ π§ β π΅) β§ π€ = 0β)) β (π¦ = π§ β π¦ β (π΅ β© π΄))) |
47 | 38, 46 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ = (π§ +β π€) β§ ((π¦ β π΄ β§ π§ β π΅) β§ π€ = 0β)) β π¦ β (π΅ β© π΄)) |
48 | 47 | expr 455 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β (π€ = 0β β π¦ β (π΅ β© π΄))) |
49 | 48 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β (π€ β (spanβ{πΆ}) β (π€ = 0β β π¦ β (π΅ β© π΄)))) |
50 | 49 | adantr 479 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ (πΆ β β β§ Β¬ πΆ β (π΄ +β π΅))) β (π€ β (spanβ{πΆ}) β (π€ = 0β β π¦ β (π΅ β© π΄)))) |
51 | 31, 50 | mpdd 43 |
. . . . . . . . . . . . . . . . 17
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ (πΆ β β β§ Β¬ πΆ β (π΄ +β π΅))) β (π€ β (spanβ{πΆ}) β π¦ β (π΅ β© π΄))) |
52 | 51 | ex 411 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β (π€ β (spanβ{πΆ}) β π¦ β (π΅ β© π΄)))) |
53 | 52 | com23 86 |
. . . . . . . . . . . . . . 15
β’ ((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β (π€ β (spanβ{πΆ}) β ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β π¦ β (π΅ β© π΄)))) |
54 | 53 | exp32 419 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π§ +β π€) β (π¦ β π΄ β (π§ β π΅ β (π€ β (spanβ{πΆ}) β ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β π¦ β (π΅ β© π΄)))))) |
55 | 54 | com4l 92 |
. . . . . . . . . . . . 13
β’ (π¦ β π΄ β (π§ β π΅ β (π€ β (spanβ{πΆ}) β (π¦ = (π§ +β π€) β ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β π¦ β (π΅ β© π΄)))))) |
56 | 55 | imp4c 422 |
. . . . . . . . . . . 12
β’ (π¦ β π΄ β (((π§ β π΅ β§ π€ β (spanβ{πΆ})) β§ π¦ = (π§ +β π€)) β ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β π¦ β (π΅ β© π΄)))) |
57 | 56 | exp4a 430 |
. . . . . . . . . . 11
β’ (π¦ β π΄ β (((π§ β π΅ β§ π€ β (spanβ{πΆ})) β§ π¦ = (π§ +β π€)) β (πΆ β β β (Β¬ πΆ β (π΄ +β π΅) β π¦ β (π΅ β© π΄))))) |
58 | 57 | com23 86 |
. . . . . . . . . 10
β’ (π¦ β π΄ β (πΆ β β β (((π§ β π΅ β§ π€ β (spanβ{πΆ})) β§ π¦ = (π§ +β π€)) β (Β¬ πΆ β (π΄ +β π΅) β π¦ β (π΅ β© π΄))))) |
59 | 58 | com4l 92 |
. . . . . . . . 9
β’ (πΆ β β β (((π§ β π΅ β§ π€ β (spanβ{πΆ})) β§ π¦ = (π§ +β π€)) β (Β¬ πΆ β (π΄ +β π΅) β (π¦ β π΄ β π¦ β (π΅ β© π΄))))) |
60 | 59 | expd 414 |
. . . . . . . 8
β’ (πΆ β β β ((π§ β π΅ β§ π€ β (spanβ{πΆ})) β (π¦ = (π§ +β π€) β (Β¬ πΆ β (π΄ +β π΅) β (π¦ β π΄ β π¦ β (π΅ β© π΄)))))) |
61 | 60 | rexlimdvv 3208 |
. . . . . . 7
β’ (πΆ β β β
(βπ§ β π΅ βπ€ β (spanβ{πΆ})π¦ = (π§ +β π€) β (Β¬ πΆ β (π΄ +β π΅) β (π¦ β π΄ β π¦ β (π΅ β© π΄))))) |
62 | 6, 61 | sylbid 239 |
. . . . . 6
β’ (πΆ β β β (π¦ β (π΅ +β (spanβ{πΆ})) β (Β¬ πΆ β (π΄ +β π΅) β (π¦ β π΄ β π¦ β (π΅ β© π΄))))) |
63 | 62 | com23 86 |
. . . . 5
β’ (πΆ β β β (Β¬
πΆ β (π΄ +β π΅) β (π¦ β (π΅ +β (spanβ{πΆ})) β (π¦ β π΄ β π¦ β (π΅ β© π΄))))) |
64 | 63 | imp4b 420 |
. . . 4
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β ((π¦ β (π΅ +β (spanβ{πΆ})) β§ π¦ β π΄) β π¦ β (π΅ β© π΄))) |
65 | 1, 64 | biimtrid 241 |
. . 3
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β (π¦ β ((π΅ +β (spanβ{πΆ})) β© π΄) β π¦ β (π΅ β© π΄))) |
66 | 65 | ssrdv 3987 |
. 2
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β ((π΅ +β (spanβ{πΆ})) β© π΄) β (π΅ β© π΄)) |
67 | | shsub1 30844 |
. . . . 5
β’ ((π΅ β
Sβ β§ (spanβ{πΆ}) β Sβ
) β π΅ β (π΅ +β
(spanβ{πΆ}))) |
68 | 3, 4, 67 | sylancr 585 |
. . . 4
β’ (πΆ β β β π΅ β (π΅ +β (spanβ{πΆ}))) |
69 | 68 | ssrind 4234 |
. . 3
β’ (πΆ β β β (π΅ β© π΄) β ((π΅ +β (spanβ{πΆ})) β© π΄)) |
70 | 69 | adantr 479 |
. 2
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β (π΅ β© π΄) β ((π΅ +β (spanβ{πΆ})) β© π΄)) |
71 | 66, 70 | eqssd 3998 |
1
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β ((π΅ +β (spanβ{πΆ})) β© π΄) = (π΅ β© π΄)) |