Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ ((πΎ β AtLat β§ π β π΄) β πΎ β AtLat) |
2 | | elin 3927 |
. . . . . . . 8
β’ (π¦ β (Fin β© π«
π) β (π¦ β Fin β§ π¦ β π« π)) |
3 | | elpwi 4568 |
. . . . . . . . 9
β’ (π¦ β π« π β π¦ β π) |
4 | 3 | adantl 483 |
. . . . . . . 8
β’ ((π¦ β Fin β§ π¦ β π« π) β π¦ β π) |
5 | 2, 4 | sylbi 216 |
. . . . . . 7
β’ (π¦ β (Fin β© π«
π) β π¦ β π) |
6 | | simpll 766 |
. . . . . . . . 9
β’ (((πΎ β AtLat β§ π β π΄) β§ π¦ β π) β πΎ β AtLat) |
7 | | sstr 3953 |
. . . . . . . . . . . 12
β’ ((π¦ β π β§ π β π΄) β π¦ β π΄) |
8 | 7 | ancoms 460 |
. . . . . . . . . . 11
β’ ((π β π΄ β§ π¦ β π) β π¦ β π΄) |
9 | 8 | adantll 713 |
. . . . . . . . . 10
β’ (((πΎ β AtLat β§ π β π΄) β§ π¦ β π) β π¦ β π΄) |
10 | | pclfin.a |
. . . . . . . . . . 11
β’ π΄ = (AtomsβπΎ) |
11 | | eqid 2737 |
. . . . . . . . . . 11
β’
(PSubSpβπΎ) =
(PSubSpβπΎ) |
12 | | pclfin.c |
. . . . . . . . . . 11
β’ π = (PClβπΎ) |
13 | 10, 11, 12 | pclclN 38357 |
. . . . . . . . . 10
β’ ((πΎ β AtLat β§ π¦ β π΄) β (πβπ¦) β (PSubSpβπΎ)) |
14 | 6, 9, 13 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΎ β AtLat β§ π β π΄) β§ π¦ β π) β (πβπ¦) β (PSubSpβπΎ)) |
15 | 10, 11 | psubssat 38220 |
. . . . . . . . 9
β’ ((πΎ β AtLat β§ (πβπ¦) β (PSubSpβπΎ)) β (πβπ¦) β π΄) |
16 | 6, 14, 15 | syl2anc 585 |
. . . . . . . 8
β’ (((πΎ β AtLat β§ π β π΄) β§ π¦ β π) β (πβπ¦) β π΄) |
17 | 16 | ex 414 |
. . . . . . 7
β’ ((πΎ β AtLat β§ π β π΄) β (π¦ β π β (πβπ¦) β π΄)) |
18 | 5, 17 | syl5 34 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΄) β (π¦ β (Fin β© π« π) β (πβπ¦) β π΄)) |
19 | 18 | ralrimiv 3143 |
. . . . 5
β’ ((πΎ β AtLat β§ π β π΄) β βπ¦ β (Fin β© π« π)(πβπ¦) β π΄) |
20 | | iunss 5006 |
. . . . 5
β’ (βͺ π¦ β (Fin β© π« π)(πβπ¦) β π΄ β βπ¦ β (Fin β© π« π)(πβπ¦) β π΄) |
21 | 19, 20 | sylibr 233 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΄) β βͺ
π¦ β (Fin β©
π« π)(πβπ¦) β π΄) |
22 | | eliun 4959 |
. . . . . . . . 9
β’ (π β βͺ π¦ β (Fin β© π« π)(πβπ¦) β βπ¦ β (Fin β© π« π)π β (πβπ¦)) |
23 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π¦ = π€ β (πβπ¦) = (πβπ€)) |
24 | 23 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π¦ = π€ β (π β (πβπ¦) β π β (πβπ€))) |
25 | 24 | cbvrexvw 3227 |
. . . . . . . . 9
β’
(βπ¦ β
(Fin β© π« π)π β (πβπ¦) β βπ€ β (Fin β© π« π)π β (πβπ€)) |
26 | 22, 25 | bitri 275 |
. . . . . . . 8
β’ (π β βͺ π¦ β (Fin β© π« π)(πβπ¦) β βπ€ β (Fin β© π« π)π β (πβπ€)) |
27 | | eliun 4959 |
. . . . . . . . 9
β’ (π β βͺ π¦ β (Fin β© π« π)(πβπ¦) β βπ¦ β (Fin β© π« π)π β (πβπ¦)) |
28 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π¦ = π£ β (πβπ¦) = (πβπ£)) |
29 | 28 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π¦ = π£ β (π β (πβπ¦) β π β (πβπ£))) |
30 | 29 | cbvrexvw 3227 |
. . . . . . . . 9
β’
(βπ¦ β
(Fin β© π« π)π β (πβπ¦) β βπ£ β (Fin β© π« π)π β (πβπ£)) |
31 | 27, 30 | bitri 275 |
. . . . . . . 8
β’ (π β βͺ π¦ β (Fin β© π« π)(πβπ¦) β βπ£ β (Fin β© π« π)π β (πβπ£)) |
32 | 26, 31 | anbi12i 628 |
. . . . . . 7
β’ ((π β βͺ π¦ β (Fin β© π« π)(πβπ¦) β§ π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)) β (βπ€ β (Fin β© π« π)π β (πβπ€) β§ βπ£ β (Fin β© π« π)π β (πβπ£))) |
33 | | elin 3927 |
. . . . . . . . . . 11
β’ (π€ β (Fin β© π«
π) β (π€ β Fin β§ π€ β π« π)) |
34 | | elpwi 4568 |
. . . . . . . . . . . 12
β’ (π€ β π« π β π€ β π) |
35 | 34 | anim2i 618 |
. . . . . . . . . . 11
β’ ((π€ β Fin β§ π€ β π« π) β (π€ β Fin β§ π€ β π)) |
36 | 33, 35 | sylbi 216 |
. . . . . . . . . 10
β’ (π€ β (Fin β© π«
π) β (π€ β Fin β§ π€ β π)) |
37 | | elin 3927 |
. . . . . . . . . . . . . 14
β’ (π£ β (Fin β© π«
π) β (π£ β Fin β§ π£ β π« π)) |
38 | | elpwi 4568 |
. . . . . . . . . . . . . . 15
β’ (π£ β π« π β π£ β π) |
39 | 38 | anim2i 618 |
. . . . . . . . . . . . . 14
β’ ((π£ β Fin β§ π£ β π« π) β (π£ β Fin β§ π£ β π)) |
40 | 37, 39 | sylbi 216 |
. . . . . . . . . . . . 13
β’ (π£ β (Fin β© π«
π) β (π£ β Fin β§ π£ β π)) |
41 | | simp2rl 1243 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π€ β Fin) |
42 | | simp12l 1287 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π£ β Fin) |
43 | | unfi 9117 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π€ β Fin β§ π£ β Fin) β (π€ βͺ π£) β Fin) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β (π€ βͺ π£) β Fin) |
45 | | simp2rr 1244 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π€ β π) |
46 | | simp12r 1288 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π£ β π) |
47 | 45, 46 | unssd 4147 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β (π€ βͺ π£) β π) |
48 | | vex 3450 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π€ β V |
49 | | vex 3450 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π£ β V |
50 | 48, 49 | unex 7681 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ βͺ π£) β V |
51 | 50 | elpw 4565 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π€ βͺ π£) β π« π β (π€ βͺ π£) β π) |
52 | 47, 51 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β (π€ βͺ π£) β π« π) |
53 | 44, 52 | elind 4155 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β (π€ βͺ π£) β (Fin β© π« π)) |
54 | | simp11l 1285 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β πΎ β AtLat) |
55 | | simp11r 1286 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π β π΄) |
56 | 45, 55 | sstrd 3955 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π€ β π΄) |
57 | 46, 55 | sstrd 3955 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π£ β π΄) |
58 | 56, 57 | unssd 4147 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β (π€ βͺ π£) β π΄) |
59 | 10, 11, 12 | pclclN 38357 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΎ β AtLat β§ (π€ βͺ π£) β π΄) β (πβ(π€ βͺ π£)) β (PSubSpβπΎ)) |
60 | 54, 58, 59 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β (πβ(π€ βͺ π£)) β (PSubSpβπΎ)) |
61 | | simp3l 1202 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π β π΄) |
62 | | ssun1 4133 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π€ β (π€ βͺ π£) |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π€ β (π€ βͺ π£)) |
64 | 10, 12 | pclssN 38360 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΎ β AtLat β§ π€ β (π€ βͺ π£) β§ (π€ βͺ π£) β π΄) β (πβπ€) β (πβ(π€ βͺ π£))) |
65 | 54, 63, 58, 64 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β (πβπ€) β (πβ(π€ βͺ π£))) |
66 | | simp2l 1200 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π β (πβπ€)) |
67 | 65, 66 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π β (πβ(π€ βͺ π£))) |
68 | | ssun2 4134 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π£ β (π€ βͺ π£) |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π£ β (π€ βͺ π£)) |
70 | 10, 12 | pclssN 38360 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΎ β AtLat β§ π£ β (π€ βͺ π£) β§ (π€ βͺ π£) β π΄) β (πβπ£) β (πβ(π€ βͺ π£))) |
71 | 54, 69, 58, 70 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β (πβπ£) β (πβ(π€ βͺ π£))) |
72 | | simp13 1206 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π β (πβπ£)) |
73 | 71, 72 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π β (πβ(π€ βͺ π£))) |
74 | | simp3r 1203 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π(leβπΎ)(π(joinβπΎ)π)) |
75 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’
(leβπΎ) =
(leβπΎ) |
76 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’
(joinβπΎ) =
(joinβπΎ) |
77 | 75, 76, 10, 11 | psubspi2N 38214 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΎ β AtLat β§ (πβ(π€ βͺ π£)) β (PSubSpβπΎ) β§ π β π΄) β§ (π β (πβ(π€ βͺ π£)) β§ π β (πβ(π€ βͺ π£)) β§ π(leβπΎ)(π(joinβπΎ)π))) β π β (πβ(π€ βͺ π£))) |
78 | 54, 60, 61, 67, 73, 74, 77 | syl33anc 1386 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π β (πβ(π€ βͺ π£))) |
79 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = (π€ βͺ π£) β (πβπ¦) = (πβ(π€ βͺ π£))) |
80 | 79 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = (π€ βͺ π£) β (π β (πβπ¦) β π β (πβ(π€ βͺ π£)))) |
81 | 80 | rspcev 3582 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ βͺ π£) β (Fin β© π« π) β§ π β (πβ(π€ βͺ π£))) β βπ¦ β (Fin β© π« π)π β (πβπ¦)) |
82 | 53, 78, 81 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β βπ¦ β (Fin β© π« π)π β (πβπ¦)) |
83 | | eliun 4959 |
. . . . . . . . . . . . . . . . 17
β’ (π β βͺ π¦ β (Fin β© π« π)(πβπ¦) β βπ¦ β (Fin β© π« π)π β (πβπ¦)) |
84 | 82, 83 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β§ (π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β§ (π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π))) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)) |
85 | 84 | 3exp 1120 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β ((π β (πβπ€) β§ (π€ β Fin β§ π€ β π)) β ((π β π΄ β§ π(leβπΎ)(π(joinβπΎ)π)) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)))) |
86 | 85 | exp5c 446 |
. . . . . . . . . . . . . 14
β’ (((πΎ β AtLat β§ π β π΄) β§ (π£ β Fin β§ π£ β π) β§ π β (πβπ£)) β (π β (πβπ€) β ((π€ β Fin β§ π€ β π) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)))))) |
87 | 86 | 3exp 1120 |
. . . . . . . . . . . . 13
β’ ((πΎ β AtLat β§ π β π΄) β ((π£ β Fin β§ π£ β π) β (π β (πβπ£) β (π β (πβπ€) β ((π€ β Fin β§ π€ β π) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)))))))) |
88 | 40, 87 | syl5 34 |
. . . . . . . . . . . 12
β’ ((πΎ β AtLat β§ π β π΄) β (π£ β (Fin β© π« π) β (π β (πβπ£) β (π β (πβπ€) β ((π€ β Fin β§ π€ β π) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)))))))) |
89 | 88 | rexlimdv 3151 |
. . . . . . . . . . 11
β’ ((πΎ β AtLat β§ π β π΄) β (βπ£ β (Fin β© π« π)π β (πβπ£) β (π β (πβπ€) β ((π€ β Fin β§ π€ β π) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦))))))) |
90 | 89 | com24 95 |
. . . . . . . . . 10
β’ ((πΎ β AtLat β§ π β π΄) β ((π€ β Fin β§ π€ β π) β (π β (πβπ€) β (βπ£ β (Fin β© π« π)π β (πβπ£) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦))))))) |
91 | 36, 90 | syl5 34 |
. . . . . . . . 9
β’ ((πΎ β AtLat β§ π β π΄) β (π€ β (Fin β© π« π) β (π β (πβπ€) β (βπ£ β (Fin β© π« π)π β (πβπ£) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦))))))) |
92 | 91 | rexlimdv 3151 |
. . . . . . . 8
β’ ((πΎ β AtLat β§ π β π΄) β (βπ€ β (Fin β© π« π)π β (πβπ€) β (βπ£ β (Fin β© π« π)π β (πβπ£) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)))))) |
93 | 92 | impd 412 |
. . . . . . 7
β’ ((πΎ β AtLat β§ π β π΄) β ((βπ€ β (Fin β© π« π)π β (πβπ€) β§ βπ£ β (Fin β© π« π)π β (πβπ£)) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦))))) |
94 | 32, 93 | biimtrid 241 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΄) β ((π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦) β§ π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦))))) |
95 | 94 | ralrimdv 3150 |
. . . . 5
β’ ((πΎ β AtLat β§ π β π΄) β ((π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦) β§ π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)) β βπ β π΄ (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)))) |
96 | 95 | ralrimivv 3196 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΄) β βπ β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)βπ β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)βπ β π΄ (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦))) |
97 | 75, 76, 10, 11 | ispsubsp 38211 |
. . . . 5
β’ (πΎ β AtLat β (βͺ π¦ β (Fin β© π« π)(πβπ¦) β (PSubSpβπΎ) β (βͺ π¦ β (Fin β© π« π)(πβπ¦) β π΄ β§ βπ β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)βπ β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)βπ β π΄ (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦))))) |
98 | 97 | adantr 482 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΄) β (βͺ π¦ β (Fin β© π« π)(πβπ¦) β (PSubSpβπΎ) β (βͺ π¦ β (Fin β© π« π)(πβπ¦) β π΄ β§ βπ β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)βπ β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)βπ β π΄ (π(leβπΎ)(π(joinβπΎ)π) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦))))) |
99 | 21, 96, 98 | mpbir2and 712 |
. . 3
β’ ((πΎ β AtLat β§ π β π΄) β βͺ
π¦ β (Fin β©
π« π)(πβπ¦) β (PSubSpβπΎ)) |
100 | | snfi 8989 |
. . . . . . . . 9
β’ {π€} β Fin |
101 | 100 | a1i 11 |
. . . . . . . 8
β’ (((πΎ β AtLat β§ π β π΄) β§ π€ β π) β {π€} β Fin) |
102 | | snelpwi 5401 |
. . . . . . . . 9
β’ (π€ β π β {π€} β π« π) |
103 | 102 | adantl 483 |
. . . . . . . 8
β’ (((πΎ β AtLat β§ π β π΄) β§ π€ β π) β {π€} β π« π) |
104 | 101, 103 | elind 4155 |
. . . . . . 7
β’ (((πΎ β AtLat β§ π β π΄) β§ π€ β π) β {π€} β (Fin β© π« π)) |
105 | | vsnid 4624 |
. . . . . . . 8
β’ π€ β {π€} |
106 | | simpll 766 |
. . . . . . . . 9
β’ (((πΎ β AtLat β§ π β π΄) β§ π€ β π) β πΎ β AtLat) |
107 | | ssel2 3940 |
. . . . . . . . . . 11
β’ ((π β π΄ β§ π€ β π) β π€ β π΄) |
108 | 107 | adantll 713 |
. . . . . . . . . 10
β’ (((πΎ β AtLat β§ π β π΄) β§ π€ β π) β π€ β π΄) |
109 | 10, 11 | snatpsubN 38216 |
. . . . . . . . . 10
β’ ((πΎ β AtLat β§ π€ β π΄) β {π€} β (PSubSpβπΎ)) |
110 | 106, 108,
109 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΎ β AtLat β§ π β π΄) β§ π€ β π) β {π€} β (PSubSpβπΎ)) |
111 | 11, 12 | pclidN 38362 |
. . . . . . . . 9
β’ ((πΎ β AtLat β§ {π€} β (PSubSpβπΎ)) β (πβ{π€}) = {π€}) |
112 | 106, 110,
111 | syl2anc 585 |
. . . . . . . 8
β’ (((πΎ β AtLat β§ π β π΄) β§ π€ β π) β (πβ{π€}) = {π€}) |
113 | 105, 112 | eleqtrrid 2845 |
. . . . . . 7
β’ (((πΎ β AtLat β§ π β π΄) β§ π€ β π) β π€ β (πβ{π€})) |
114 | | fveq2 6843 |
. . . . . . . . 9
β’ (π¦ = {π€} β (πβπ¦) = (πβ{π€})) |
115 | 114 | eleq2d 2824 |
. . . . . . . 8
β’ (π¦ = {π€} β (π€ β (πβπ¦) β π€ β (πβ{π€}))) |
116 | 115 | rspcev 3582 |
. . . . . . 7
β’ (({π€} β (Fin β© π«
π) β§ π€ β (πβ{π€})) β βπ¦ β (Fin β© π« π)π€ β (πβπ¦)) |
117 | 104, 113,
116 | syl2anc 585 |
. . . . . 6
β’ (((πΎ β AtLat β§ π β π΄) β§ π€ β π) β βπ¦ β (Fin β© π« π)π€ β (πβπ¦)) |
118 | 117 | ex 414 |
. . . . 5
β’ ((πΎ β AtLat β§ π β π΄) β (π€ β π β βπ¦ β (Fin β© π« π)π€ β (πβπ¦))) |
119 | | eliun 4959 |
. . . . 5
β’ (π€ β βͺ π¦ β (Fin β© π« π)(πβπ¦) β βπ¦ β (Fin β© π« π)π€ β (πβπ¦)) |
120 | 118, 119 | syl6ibr 252 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΄) β (π€ β π β π€ β βͺ
π¦ β (Fin β©
π« π)(πβπ¦))) |
121 | 120 | ssrdv 3951 |
. . 3
β’ ((πΎ β AtLat β§ π β π΄) β π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦)) |
122 | | simpr 486 |
. . . . . . . . . 10
β’ (((πΎ β AtLat β§ π β π΄) β§ π¦ β π) β π¦ β π) |
123 | | simplr 768 |
. . . . . . . . . 10
β’ (((πΎ β AtLat β§ π β π΄) β§ π¦ β π) β π β π΄) |
124 | 10, 12 | pclssN 38360 |
. . . . . . . . . 10
β’ ((πΎ β AtLat β§ π¦ β π β§ π β π΄) β (πβπ¦) β (πβπ)) |
125 | 6, 122, 123, 124 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β AtLat β§ π β π΄) β§ π¦ β π) β (πβπ¦) β (πβπ)) |
126 | 125 | sseld 3944 |
. . . . . . . 8
β’ (((πΎ β AtLat β§ π β π΄) β§ π¦ β π) β (π€ β (πβπ¦) β π€ β (πβπ))) |
127 | 126 | ex 414 |
. . . . . . 7
β’ ((πΎ β AtLat β§ π β π΄) β (π¦ β π β (π€ β (πβπ¦) β π€ β (πβπ)))) |
128 | 5, 127 | syl5 34 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΄) β (π¦ β (Fin β© π« π) β (π€ β (πβπ¦) β π€ β (πβπ)))) |
129 | 128 | rexlimdv 3151 |
. . . . 5
β’ ((πΎ β AtLat β§ π β π΄) β (βπ¦ β (Fin β© π« π)π€ β (πβπ¦) β π€ β (πβπ))) |
130 | 119, 129 | biimtrid 241 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΄) β (π€ β βͺ
π¦ β (Fin β©
π« π)(πβπ¦) β π€ β (πβπ))) |
131 | 130 | ssrdv 3951 |
. . 3
β’ ((πΎ β AtLat β§ π β π΄) β βͺ
π¦ β (Fin β©
π« π)(πβπ¦) β (πβπ)) |
132 | 11, 12 | pclbtwnN 38363 |
. . 3
β’ (((πΎ β AtLat β§ βͺ π¦ β (Fin β© π« π)(πβπ¦) β (PSubSpβπΎ)) β§ (π β βͺ
π¦ β (Fin β©
π« π)(πβπ¦) β§ βͺ
π¦ β (Fin β©
π« π)(πβπ¦) β (πβπ))) β βͺ π¦ β (Fin β© π« π)(πβπ¦) = (πβπ)) |
133 | 1, 99, 121, 131, 132 | syl22anc 838 |
. 2
β’ ((πΎ β AtLat β§ π β π΄) β βͺ
π¦ β (Fin β©
π« π)(πβπ¦) = (πβπ)) |
134 | 133 | eqcomd 2743 |
1
β’ ((πΎ β AtLat β§ π β π΄) β (πβπ) = βͺ
π¦ β (Fin β©
π« π)(πβπ¦)) |