Step | Hyp | Ref
| Expression |
1 | | dfpss3 4051 |
. . 3
β’ (π β π β (π β π β§ Β¬ π β π)) |
2 | 1 | simprbi 498 |
. 2
β’ (π β π β Β¬ π β π) |
3 | | ss2rab 4033 |
. . . . . 6
β’ ({π β π΄ β£ π β π} β {π β π΄ β£ π β π} β βπ β π΄ (π β π β π β π)) |
4 | | iman 403 |
. . . . . . 7
β’ ((π β π β π β π) β Β¬ (π β π β§ Β¬ π β π)) |
5 | 4 | ralbii 3097 |
. . . . . 6
β’
(βπ β
π΄ (π β π β π β π) β βπ β π΄ Β¬ (π β π β§ Β¬ π β π)) |
6 | 3, 5 | bitr2i 276 |
. . . . 5
β’
(βπ β
π΄ Β¬ (π β π β§ Β¬ π β π) β {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) |
7 | | simpl1 1192 |
. . . . . . . 8
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β π β LMod) |
8 | | lssat.s |
. . . . . . . . . . 11
β’ π = (LSubSpβπ) |
9 | | lssat.a |
. . . . . . . . . . 11
β’ π΄ = (LSAtomsβπ) |
10 | 8, 9 | lsatlss 37487 |
. . . . . . . . . 10
β’ (π β LMod β π΄ β π) |
11 | | rabss2 4040 |
. . . . . . . . . 10
β’ (π΄ β π β {π β π΄ β£ π β π} β {π β π β£ π β π}) |
12 | | uniss 4878 |
. . . . . . . . . 10
β’ ({π β π΄ β£ π β π} β {π β π β£ π β π} β βͺ {π β π΄ β£ π β π} β βͺ
{π β π β£ π β π}) |
13 | 7, 10, 11, 12 | 4syl 19 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β βͺ
{π β π΄ β£ π β π} β βͺ
{π β π β£ π β π}) |
14 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β π β π) |
15 | | unimax 4910 |
. . . . . . . . . . 11
β’ (π β π β βͺ {π β π β£ π β π} = π) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β βͺ
{π β π β£ π β π} = π) |
17 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
18 | 17, 8 | lssss 20413 |
. . . . . . . . . . 11
β’ (π β π β π β (Baseβπ)) |
19 | 14, 18 | syl 17 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β π β (Baseβπ)) |
20 | 16, 19 | eqsstrd 3987 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β βͺ
{π β π β£ π β π} β (Baseβπ)) |
21 | 13, 20 | sstrd 3959 |
. . . . . . . 8
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β βͺ
{π β π΄ β£ π β π} β (Baseβπ)) |
22 | | uniss 4878 |
. . . . . . . . 9
β’ ({π β π΄ β£ π β π} β {π β π΄ β£ π β π} β βͺ {π β π΄ β£ π β π} β βͺ
{π β π΄ β£ π β π}) |
23 | 22 | adantl 483 |
. . . . . . . 8
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β βͺ
{π β π΄ β£ π β π} β βͺ
{π β π΄ β£ π β π}) |
24 | | eqid 2737 |
. . . . . . . . 9
β’
(LSpanβπ) =
(LSpanβπ) |
25 | 17, 24 | lspss 20461 |
. . . . . . . 8
β’ ((π β LMod β§ βͺ {π
β π΄ β£ π β π} β (Baseβπ) β§ βͺ {π β π΄ β£ π β π} β βͺ
{π β π΄ β£ π β π}) β ((LSpanβπ)ββͺ {π β π΄ β£ π β π}) β ((LSpanβπ)ββͺ {π β π΄ β£ π β π})) |
26 | 7, 21, 23, 25 | syl3anc 1372 |
. . . . . . 7
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β ((LSpanβπ)ββͺ {π β π΄ β£ π β π}) β ((LSpanβπ)ββͺ {π β π΄ β£ π β π})) |
27 | | simpl3 1194 |
. . . . . . . 8
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β π β π) |
28 | 8, 24, 9 | lssats 37503 |
. . . . . . . 8
β’ ((π β LMod β§ π β π) β π = ((LSpanβπ)ββͺ {π β π΄ β£ π β π})) |
29 | 7, 27, 28 | syl2anc 585 |
. . . . . . 7
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β π = ((LSpanβπ)ββͺ {π β π΄ β£ π β π})) |
30 | 8, 24, 9 | lssats 37503 |
. . . . . . . 8
β’ ((π β LMod β§ π β π) β π = ((LSpanβπ)ββͺ {π β π΄ β£ π β π})) |
31 | 7, 14, 30 | syl2anc 585 |
. . . . . . 7
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β π = ((LSpanβπ)ββͺ {π β π΄ β£ π β π})) |
32 | 26, 29, 31 | 3sstr4d 3996 |
. . . . . 6
β’ (((π β LMod β§ π β π β§ π β π) β§ {π β π΄ β£ π β π} β {π β π΄ β£ π β π}) β π β π) |
33 | 32 | ex 414 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β ({π β π΄ β£ π β π} β {π β π΄ β£ π β π} β π β π)) |
34 | 6, 33 | biimtrid 241 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β (βπ β π΄ Β¬ (π β π β§ Β¬ π β π) β π β π)) |
35 | 34 | con3dimp 410 |
. . 3
β’ (((π β LMod β§ π β π β§ π β π) β§ Β¬ π β π) β Β¬ βπ β π΄ Β¬ (π β π β§ Β¬ π β π)) |
36 | | dfrex2 3077 |
. . 3
β’
(βπ β
π΄ (π β π β§ Β¬ π β π) β Β¬ βπ β π΄ Β¬ (π β π β§ Β¬ π β π)) |
37 | 35, 36 | sylibr 233 |
. 2
β’ (((π β LMod β§ π β π β§ π β π) β§ Β¬ π β π) β βπ β π΄ (π β π β§ Β¬ π β π)) |
38 | 2, 37 | sylan2 594 |
1
β’ (((π β LMod β§ π β π β§ π β π) β§ π β π) β βπ β π΄ (π β π β§ Β¬ π β π)) |