Step | Hyp | Ref
| Expression |
1 | | nonbool.1 |
. . . . . . . . . . . . 13
β’ π΄ β β |
2 | | nonbool.2 |
. . . . . . . . . . . . 13
β’ π΅ β β |
3 | 1, 2 | hvaddcli 29960 |
. . . . . . . . . . . 12
β’ (π΄ +β π΅) β
β |
4 | | spansnid 30505 |
. . . . . . . . . . . 12
β’ ((π΄ +β π΅) β β β (π΄ +β π΅) β (spanβ{(π΄ +β π΅)})) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π΄ +β π΅) β (spanβ{(π΄ +β π΅)}) |
6 | | nonbool.5 |
. . . . . . . . . . 11
β’ π» = (spanβ{(π΄ +β π΅)}) |
7 | 5, 6 | eleqtrri 2836 |
. . . . . . . . . 10
β’ (π΄ +β π΅) β π» |
8 | | nonbool.3 |
. . . . . . . . . . . . 13
β’ πΉ = (spanβ{π΄}) |
9 | 1 | spansnchi 30504 |
. . . . . . . . . . . . . 14
β’
(spanβ{π΄})
β Cβ |
10 | 9 | chshii 30169 |
. . . . . . . . . . . . 13
β’
(spanβ{π΄})
β Sβ |
11 | 8, 10 | eqeltri 2833 |
. . . . . . . . . . . 12
β’ πΉ β
Sβ |
12 | | nonbool.4 |
. . . . . . . . . . . . 13
β’ πΊ = (spanβ{π΅}) |
13 | 2 | spansnchi 30504 |
. . . . . . . . . . . . . 14
β’
(spanβ{π΅})
β Cβ |
14 | 13 | chshii 30169 |
. . . . . . . . . . . . 13
β’
(spanβ{π΅})
β Sβ |
15 | 12, 14 | eqeltri 2833 |
. . . . . . . . . . . 12
β’ πΊ β
Sβ |
16 | 11, 15 | shsleji 30312 |
. . . . . . . . . . 11
β’ (πΉ +β πΊ) β (πΉ β¨β πΊ) |
17 | | spansnid 30505 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β π΄ β (spanβ{π΄})) |
18 | 1, 17 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ π΄ β (spanβ{π΄}) |
19 | 18, 8 | eleqtrri 2836 |
. . . . . . . . . . . 12
β’ π΄ β πΉ |
20 | | spansnid 30505 |
. . . . . . . . . . . . . 14
β’ (π΅ β β β π΅ β (spanβ{π΅})) |
21 | 2, 20 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ π΅ β (spanβ{π΅}) |
22 | 21, 12 | eleqtrri 2836 |
. . . . . . . . . . . 12
β’ π΅ β πΊ |
23 | 11, 15 | shsvai 30306 |
. . . . . . . . . . . 12
β’ ((π΄ β πΉ β§ π΅ β πΊ) β (π΄ +β π΅) β (πΉ +β πΊ)) |
24 | 19, 22, 23 | mp2an 690 |
. . . . . . . . . . 11
β’ (π΄ +β π΅) β (πΉ +β πΊ) |
25 | 16, 24 | sselii 3941 |
. . . . . . . . . 10
β’ (π΄ +β π΅) β (πΉ β¨β πΊ) |
26 | | elin 3926 |
. . . . . . . . . 10
β’ ((π΄ +β π΅) β (π» β© (πΉ β¨β πΊ)) β ((π΄ +β π΅) β π» β§ (π΄ +β π΅) β (πΉ β¨β πΊ))) |
27 | 7, 25, 26 | mpbir2an 709 |
. . . . . . . . 9
β’ (π΄ +β π΅) β (π» β© (πΉ β¨β πΊ)) |
28 | | eleq2 2826 |
. . . . . . . . 9
β’ ((π» β© (πΉ β¨β πΊ)) = 0β β ((π΄ +β π΅) β (π» β© (πΉ β¨β πΊ)) β (π΄ +β π΅) β
0β)) |
29 | 27, 28 | mpbii 232 |
. . . . . . . 8
β’ ((π» β© (πΉ β¨β πΊ)) = 0β β (π΄ +β π΅) β
0β) |
30 | | elch0 30196 |
. . . . . . . 8
β’ ((π΄ +β π΅) β 0β
β (π΄
+β π΅) =
0β) |
31 | 29, 30 | sylib 217 |
. . . . . . 7
β’ ((π» β© (πΉ β¨β πΊ)) = 0β β (π΄ +β π΅) =
0β) |
32 | | ch0 30170 |
. . . . . . . 8
β’
((spanβ{π΄})
β Cβ β 0β β
(spanβ{π΄})) |
33 | 9, 32 | ax-mp 5 |
. . . . . . 7
β’
0β β (spanβ{π΄}) |
34 | 31, 33 | eqeltrdi 2845 |
. . . . . 6
β’ ((π» β© (πΉ β¨β πΊ)) = 0β β (π΄ +β π΅) β (spanβ{π΄})) |
35 | 8 | eleq2i 2829 |
. . . . . . 7
β’ (π΅ β πΉ β π΅ β (spanβ{π΄})) |
36 | | sumspansn 30591 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β) β ((π΄ +β π΅) β (spanβ{π΄}) β π΅ β (spanβ{π΄}))) |
37 | 1, 2, 36 | mp2an 690 |
. . . . . . 7
β’ ((π΄ +β π΅) β (spanβ{π΄}) β π΅ β (spanβ{π΄})) |
38 | 35, 37 | bitr4i 277 |
. . . . . 6
β’ (π΅ β πΉ β (π΄ +β π΅) β (spanβ{π΄})) |
39 | 34, 38 | sylibr 233 |
. . . . 5
β’ ((π» β© (πΉ β¨β πΊ)) = 0β β π΅ β πΉ) |
40 | 39 | con3i 154 |
. . . 4
β’ (Β¬
π΅ β πΉ β Β¬ (π» β© (πΉ β¨β πΊ)) = 0β) |
41 | 40 | adantl 482 |
. . 3
β’ ((Β¬
π΄ β πΊ β§ Β¬ π΅ β πΉ) β Β¬ (π» β© (πΉ β¨β πΊ)) = 0β) |
42 | 6, 8 | ineq12i 4170 |
. . . . . 6
β’ (π» β© πΉ) = ((spanβ{(π΄ +β π΅)}) β© (spanβ{π΄})) |
43 | 3, 1 | spansnm0i 30592 |
. . . . . . 7
β’ (Β¬
(π΄ +β
π΅) β
(spanβ{π΄}) β
((spanβ{(π΄
+β π΅)})
β© (spanβ{π΄})) =
0β) |
44 | 38, 43 | sylnbi 329 |
. . . . . 6
β’ (Β¬
π΅ β πΉ β ((spanβ{(π΄ +β π΅)}) β© (spanβ{π΄})) = 0β) |
45 | 42, 44 | eqtrid 2788 |
. . . . 5
β’ (Β¬
π΅ β πΉ β (π» β© πΉ) = 0β) |
46 | 6, 12 | ineq12i 4170 |
. . . . . 6
β’ (π» β© πΊ) = ((spanβ{(π΄ +β π΅)}) β© (spanβ{π΅})) |
47 | | sumspansn 30591 |
. . . . . . . . 9
β’ ((π΅ β β β§ π΄ β β) β ((π΅ +β π΄) β (spanβ{π΅}) β π΄ β (spanβ{π΅}))) |
48 | 2, 1, 47 | mp2an 690 |
. . . . . . . 8
β’ ((π΅ +β π΄) β (spanβ{π΅}) β π΄ β (spanβ{π΅})) |
49 | 1, 2 | hvcomi 29961 |
. . . . . . . . 9
β’ (π΄ +β π΅) = (π΅ +β π΄) |
50 | 49 | eleq1i 2828 |
. . . . . . . 8
β’ ((π΄ +β π΅) β (spanβ{π΅}) β (π΅ +β π΄) β (spanβ{π΅})) |
51 | 12 | eleq2i 2829 |
. . . . . . . 8
β’ (π΄ β πΊ β π΄ β (spanβ{π΅})) |
52 | 48, 50, 51 | 3bitr4ri 303 |
. . . . . . 7
β’ (π΄ β πΊ β (π΄ +β π΅) β (spanβ{π΅})) |
53 | 3, 2 | spansnm0i 30592 |
. . . . . . 7
β’ (Β¬
(π΄ +β
π΅) β
(spanβ{π΅}) β
((spanβ{(π΄
+β π΅)})
β© (spanβ{π΅})) =
0β) |
54 | 52, 53 | sylnbi 329 |
. . . . . 6
β’ (Β¬
π΄ β πΊ β ((spanβ{(π΄ +β π΅)}) β© (spanβ{π΅})) = 0β) |
55 | 46, 54 | eqtrid 2788 |
. . . . 5
β’ (Β¬
π΄ β πΊ β (π» β© πΊ) = 0β) |
56 | 45, 55 | oveqan12rd 7377 |
. . . 4
β’ ((Β¬
π΄ β πΊ β§ Β¬ π΅ β πΉ) β ((π» β© πΉ) β¨β (π» β© πΊ)) = (0β
β¨β 0β)) |
57 | | h0elch 30197 |
. . . . 5
β’
0β β
Cβ |
58 | 57 | chj0i 30397 |
. . . 4
β’
(0β β¨β 0β) =
0β |
59 | 56, 58 | eqtrdi 2792 |
. . 3
β’ ((Β¬
π΄ β πΊ β§ Β¬ π΅ β πΉ) β ((π» β© πΉ) β¨β (π» β© πΊ)) = 0β) |
60 | | eqeq2 2748 |
. . . . 5
β’ (((π» β© πΉ) β¨β (π» β© πΊ)) = 0β β ((π» β© (πΉ β¨β πΊ)) = ((π» β© πΉ) β¨β (π» β© πΊ)) β (π» β© (πΉ β¨β πΊ)) = 0β)) |
61 | 60 | notbid 317 |
. . . 4
β’ (((π» β© πΉ) β¨β (π» β© πΊ)) = 0β β (Β¬
(π» β© (πΉ β¨β πΊ)) = ((π» β© πΉ) β¨β (π» β© πΊ)) β Β¬ (π» β© (πΉ β¨β πΊ)) = 0β)) |
62 | 61 | biimparc 480 |
. . 3
β’ ((Β¬
(π» β© (πΉ β¨β πΊ)) = 0β β§ ((π» β© πΉ) β¨β (π» β© πΊ)) = 0β) β Β¬
(π» β© (πΉ β¨β πΊ)) = ((π» β© πΉ) β¨β (π» β© πΊ))) |
63 | 41, 59, 62 | syl2anc 584 |
. 2
β’ ((Β¬
π΄ β πΊ β§ Β¬ π΅ β πΉ) β Β¬ (π» β© (πΉ β¨β πΊ)) = ((π» β© πΉ) β¨β (π» β© πΊ))) |
64 | | ioran 982 |
. 2
β’ (Β¬
(π΄ β πΊ β¨ π΅ β πΉ) β (Β¬ π΄ β πΊ β§ Β¬ π΅ β πΉ)) |
65 | | df-ne 2944 |
. 2
β’ ((π» β© (πΉ β¨β πΊ)) β ((π» β© πΉ) β¨β (π» β© πΊ)) β Β¬ (π» β© (πΉ β¨β πΊ)) = ((π» β© πΉ) β¨β (π» β© πΊ))) |
66 | 63, 64, 65 | 3imtr4i 291 |
1
β’ (Β¬
(π΄ β πΊ β¨ π΅ β πΉ) β (π» β© (πΉ β¨β πΊ)) β ((π» β© πΉ) β¨β (π» β© πΊ))) |