Step | Hyp | Ref
| Expression |
1 | | elin 3964 |
. . . 4
β’ (π¦ β ((π΅ +β (spanβ{πΆ})) β© π΄) β (π¦ β (π΅ +β (spanβ{πΆ})) β§ π¦ β π΄)) |
2 | | sumdmdi.2 |
. . . . . . . . 9
β’ π΅ β
Cβ |
3 | 2 | chshii 30468 |
. . . . . . . 8
β’ π΅ β
Sβ |
4 | | spansnsh 30802 |
. . . . . . . 8
β’ (πΆ β β β
(spanβ{πΆ}) β
Sβ ) |
5 | | shsel 30555 |
. . . . . . . 8
β’ ((π΅ β
Sβ β§ (spanβ{πΆ}) β Sβ
) β (π¦ β (π΅ +β
(spanβ{πΆ})) β
βπ§ β π΅ βπ€ β (spanβ{πΆ})π¦ = (π§ +β π€))) |
6 | 3, 4, 5 | sylancr 588 |
. . . . . . 7
β’ (πΆ β β β (π¦ β (π΅ +β (spanβ{πΆ})) β βπ§ β π΅ βπ€ β (spanβ{πΆ})π¦ = (π§ +β π€))) |
7 | | sumdmdi.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ π΄ β
Cβ |
8 | 7 | cheli 30473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β π΄ β π¦ β β) |
9 | 2 | cheli 30473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ β π΅ β π§ β β) |
10 | | elspansncl 30806 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΆ β β β§ π€ β (spanβ{πΆ})) β π€ β β) |
11 | | hvsubadd 30318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π¦ β β β§ π§ β β β§ π€ β β) β ((π¦ ββ
π§) = π€ β (π§ +β π€) = π¦)) |
12 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π§ +β π€) = π¦ β π¦ = (π§ +β π€)) |
13 | 11, 12 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β β β§ π§ β β β§ π€ β β) β ((π¦ ββ
π§) = π€ β π¦ = (π§ +β π€))) |
14 | 8, 9, 10, 13 | syl3an 1161 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β π΄ β§ π§ β π΅ β§ (πΆ β β β§ π€ β (spanβ{πΆ}))) β ((π¦ ββ π§) = π€ β π¦ = (π§ +β π€))) |
15 | 14 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π¦ β π΄ β§ π§ β π΅) β§ (πΆ β β β§ π€ β (spanβ{πΆ}))) β ((π¦ ββ π§) = π€ β π¦ = (π§ +β π€))) |
16 | 7 | chshii 30468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ π΄ β
Sβ |
17 | 16, 3 | shsvsi 30608 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β π΄ β§ π§ β π΅) β (π¦ ββ π§) β (π΄ +β π΅)) |
18 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ ββ
π§) = π€ β ((π¦ ββ π§) β (π΄ +β π΅) β π€ β (π΄ +β π΅))) |
19 | 17, 18 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β π΄ β§ π§ β π΅) β ((π¦ ββ π§) = π€ β π€ β (π΄ +β π΅))) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π¦ β π΄ β§ π§ β π΅) β§ (πΆ β β β§ π€ β (spanβ{πΆ}))) β ((π¦ ββ π§) = π€ β π€ β (π΄ +β π΅))) |
21 | 15, 20 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π¦ β π΄ β§ π§ β π΅) β§ (πΆ β β β§ π€ β (spanβ{πΆ}))) β (π¦ = (π§ +β π€) β π€ β (π΄ +β π΅))) |
22 | 21 | exp32 422 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β π΄ β§ π§ β π΅) β (πΆ β β β (π€ β (spanβ{πΆ}) β (π¦ = (π§ +β π€) β π€ β (π΄ +β π΅))))) |
23 | 22 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = (π§ +β π€) β ((π¦ β π΄ β§ π§ β π΅) β (πΆ β β β (π€ β (spanβ{πΆ}) β π€ β (π΄ +β π΅))))) |
24 | 23 | imp31 419 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ πΆ β β) β (π€ β (spanβ{πΆ}) β π€ β (π΄ +β π΅))) |
25 | 24 | adantrr 716 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ (πΆ β β β§ Β¬ πΆ β (π΄ +β π΅))) β (π€ β (spanβ{πΆ}) β π€ β (π΄ +β π΅))) |
26 | 16, 3 | shscli 30558 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ +β π΅) β
Sβ |
27 | | elspansn5 30815 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ +β π΅) β
Sβ β (((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β§ (π€ β (spanβ{πΆ}) β§ π€ β (π΄ +β π΅))) β π€ = 0β)) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β§ (π€ β (spanβ{πΆ}) β§ π€ β (π΄ +β π΅))) β π€ = 0β) |
29 | 28 | exp32 422 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β (π€ β (spanβ{πΆ}) β (π€ β (π΄ +β π΅) β π€ = 0β))) |
30 | 29 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ (πΆ β β β§ Β¬ πΆ β (π΄ +β π΅))) β (π€ β (spanβ{πΆ}) β (π€ β (π΄ +β π΅) β π€ = 0β))) |
31 | 25, 30 | mpdd 43 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ (πΆ β β β§ Β¬ πΆ β (π΄ +β π΅))) β (π€ β (spanβ{πΆ}) β π€ = 0β)) |
32 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ = 0β β
(π§ +β
π€) = (π§ +β
0β)) |
33 | | ax-hvaddid 30245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ β β β (π§ +β
0β) = π§) |
34 | 32, 33 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π§ β β β§ π€ = 0β) β
(π§ +β
π€) = π§) |
35 | 9, 34 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π§ β π΅ β§ π€ = 0β) β (π§ +β π€) = π§) |
36 | 35 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π§ β π΅ β§ π€ = 0β) β (π¦ = (π§ +β π€) β π¦ = π§)) |
37 | 36 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π¦ β π΄ β§ π§ β π΅) β§ π€ = 0β) β (π¦ = (π§ +β π€) β π¦ = π§)) |
38 | 37 | biimpac 480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ = (π§ +β π€) β§ ((π¦ β π΄ β§ π§ β π΅) β§ π€ = 0β)) β π¦ = π§) |
39 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ = π§ β (π¦ β π΅ β π§ β π΅)) |
40 | 39 | biimparc 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π§ β π΅ β§ π¦ = π§) β π¦ β π΅) |
41 | | elin 3964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β (π΅ β© π΄) β (π¦ β π΅ β§ π¦ β π΄)) |
42 | 41 | biimpri 227 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β π΅ β§ π¦ β π΄) β π¦ β (π΅ β© π΄)) |
43 | 42 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β π΄ β§ π¦ β π΅) β π¦ β (π΅ β© π΄)) |
44 | 40, 43 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β π΄ β§ (π§ β π΅ β§ π¦ = π§)) β π¦ β (π΅ β© π΄)) |
45 | 44 | expr 458 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β π΄ β§ π§ β π΅) β (π¦ = π§ β π¦ β (π΅ β© π΄))) |
46 | 45 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ = (π§ +β π€) β§ ((π¦ β π΄ β§ π§ β π΅) β§ π€ = 0β)) β (π¦ = π§ β π¦ β (π΅ β© π΄))) |
47 | 38, 46 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ = (π§ +β π€) β§ ((π¦ β π΄ β§ π§ β π΅) β§ π€ = 0β)) β π¦ β (π΅ β© π΄)) |
48 | 47 | expr 458 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β (π€ = 0β β π¦ β (π΅ β© π΄))) |
49 | 48 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β (π€ β (spanβ{πΆ}) β (π€ = 0β β π¦ β (π΅ β© π΄)))) |
50 | 49 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ (πΆ β β β§ Β¬ πΆ β (π΄ +β π΅))) β (π€ β (spanβ{πΆ}) β (π€ = 0β β π¦ β (π΅ β© π΄)))) |
51 | 31, 50 | mpdd 43 |
. . . . . . . . . . . . . . . . 17
β’ (((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β§ (πΆ β β β§ Β¬ πΆ β (π΄ +β π΅))) β (π€ β (spanβ{πΆ}) β π¦ β (π΅ β© π΄))) |
52 | 51 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β (π€ β (spanβ{πΆ}) β π¦ β (π΅ β© π΄)))) |
53 | 52 | com23 86 |
. . . . . . . . . . . . . . 15
β’ ((π¦ = (π§ +β π€) β§ (π¦ β π΄ β§ π§ β π΅)) β (π€ β (spanβ{πΆ}) β ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β π¦ β (π΅ β© π΄)))) |
54 | 53 | exp32 422 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π§ +β π€) β (π¦ β π΄ β (π§ β π΅ β (π€ β (spanβ{πΆ}) β ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β π¦ β (π΅ β© π΄)))))) |
55 | 54 | com4l 92 |
. . . . . . . . . . . . 13
β’ (π¦ β π΄ β (π§ β π΅ β (π€ β (spanβ{πΆ}) β (π¦ = (π§ +β π€) β ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β π¦ β (π΅ β© π΄)))))) |
56 | 55 | imp4c 425 |
. . . . . . . . . . . 12
β’ (π¦ β π΄ β (((π§ β π΅ β§ π€ β (spanβ{πΆ})) β§ π¦ = (π§ +β π€)) β ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β π¦ β (π΅ β© π΄)))) |
57 | 56 | exp4a 433 |
. . . . . . . . . . 11
β’ (π¦ β π΄ β (((π§ β π΅ β§ π€ β (spanβ{πΆ})) β§ π¦ = (π§ +β π€)) β (πΆ β β β (Β¬ πΆ β (π΄ +β π΅) β π¦ β (π΅ β© π΄))))) |
58 | 57 | com23 86 |
. . . . . . . . . 10
β’ (π¦ β π΄ β (πΆ β β β (((π§ β π΅ β§ π€ β (spanβ{πΆ})) β§ π¦ = (π§ +β π€)) β (Β¬ πΆ β (π΄ +β π΅) β π¦ β (π΅ β© π΄))))) |
59 | 58 | com4l 92 |
. . . . . . . . 9
β’ (πΆ β β β (((π§ β π΅ β§ π€ β (spanβ{πΆ})) β§ π¦ = (π§ +β π€)) β (Β¬ πΆ β (π΄ +β π΅) β (π¦ β π΄ β π¦ β (π΅ β© π΄))))) |
60 | 59 | expd 417 |
. . . . . . . 8
β’ (πΆ β β β ((π§ β π΅ β§ π€ β (spanβ{πΆ})) β (π¦ = (π§ +β π€) β (Β¬ πΆ β (π΄ +β π΅) β (π¦ β π΄ β π¦ β (π΅ β© π΄)))))) |
61 | 60 | rexlimdvv 3211 |
. . . . . . 7
β’ (πΆ β β β
(βπ§ β π΅ βπ€ β (spanβ{πΆ})π¦ = (π§ +β π€) β (Β¬ πΆ β (π΄ +β π΅) β (π¦ β π΄ β π¦ β (π΅ β© π΄))))) |
62 | 6, 61 | sylbid 239 |
. . . . . 6
β’ (πΆ β β β (π¦ β (π΅ +β (spanβ{πΆ})) β (Β¬ πΆ β (π΄ +β π΅) β (π¦ β π΄ β π¦ β (π΅ β© π΄))))) |
63 | 62 | com23 86 |
. . . . 5
β’ (πΆ β β β (Β¬
πΆ β (π΄ +β π΅) β (π¦ β (π΅ +β (spanβ{πΆ})) β (π¦ β π΄ β π¦ β (π΅ β© π΄))))) |
64 | 63 | imp4b 423 |
. . . 4
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β ((π¦ β (π΅ +β (spanβ{πΆ})) β§ π¦ β π΄) β π¦ β (π΅ β© π΄))) |
65 | 1, 64 | biimtrid 241 |
. . 3
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β (π¦ β ((π΅ +β (spanβ{πΆ})) β© π΄) β π¦ β (π΅ β© π΄))) |
66 | 65 | ssrdv 3988 |
. 2
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β ((π΅ +β (spanβ{πΆ})) β© π΄) β (π΅ β© π΄)) |
67 | | shsub1 30565 |
. . . . 5
β’ ((π΅ β
Sβ β§ (spanβ{πΆ}) β Sβ
) β π΅ β (π΅ +β
(spanβ{πΆ}))) |
68 | 3, 4, 67 | sylancr 588 |
. . . 4
β’ (πΆ β β β π΅ β (π΅ +β (spanβ{πΆ}))) |
69 | 68 | ssrind 4235 |
. . 3
β’ (πΆ β β β (π΅ β© π΄) β ((π΅ +β (spanβ{πΆ})) β© π΄)) |
70 | 69 | adantr 482 |
. 2
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β (π΅ β© π΄) β ((π΅ +β (spanβ{πΆ})) β© π΄)) |
71 | 66, 70 | eqssd 3999 |
1
β’ ((πΆ β β β§ Β¬
πΆ β (π΄ +β π΅)) β ((π΅ +β (spanβ{πΆ})) β© π΄) = (π΅ β© π΄)) |