Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
2 | | eqid 2737 |
. . . . 5
β’
(joinβπΎ) =
(joinβπΎ) |
3 | | pmod.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
4 | | pmod.s |
. . . . 5
β’ π = (PSubSpβπΎ) |
5 | | pmod.p |
. . . . 5
β’ + =
(+πβπΎ) |
6 | 1, 2, 3, 4, 5 | pmodlem2 38313 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β ((π + π) β© π) β (π + (π β© π))) |
7 | 6 | 3expa 1119 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β ((π + π) β© π) β (π + (π β© π))) |
8 | | inss1 4189 |
. . . . 5
β’ (π β© π) β π |
9 | | simpll 766 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β πΎ β HL) |
10 | | simplr2 1217 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β π β π΄) |
11 | | simplr1 1216 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β π β π΄) |
12 | 3, 5 | paddss2 38284 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ((π β© π) β π β (π + (π β© π)) β (π + π))) |
13 | 9, 10, 11, 12 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β ((π β© π) β π β (π + (π β© π)) β (π + π))) |
14 | 8, 13 | mpi 20 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β (π + (π β© π)) β (π + π)) |
15 | | simpl 484 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β πΎ β HL) |
16 | 3, 4 | psubssat 38220 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π) β π β π΄) |
17 | 16 | 3ad2antr3 1191 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β π β π΄) |
18 | | simpr2 1196 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β π β π΄) |
19 | | ssinss1 4198 |
. . . . . . . 8
β’ (π β π΄ β (π β© π) β π΄) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β (π β© π) β π΄) |
21 | 3, 5 | paddss1 38283 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ (π β© π) β π΄) β (π β π β (π + (π β© π)) β (π + (π β© π)))) |
22 | 15, 17, 20, 21 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β (π β π β (π + (π β© π)) β (π + (π β© π)))) |
23 | 22 | imp 408 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β (π + (π β© π)) β (π + (π β© π))) |
24 | | simplr3 1218 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β π β π) |
25 | 9, 24, 16 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β π β π΄) |
26 | | inss2 4190 |
. . . . . . . 8
β’ (π β© π) β π |
27 | 3, 5 | paddss2 38284 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ((π β© π) β π β (π + (π β© π)) β (π + π))) |
28 | 26, 27 | mpi 20 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π + (π β© π)) β (π + π)) |
29 | 9, 25, 25, 28 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β (π + (π β© π)) β (π + π)) |
30 | 4, 5 | paddidm 38307 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π) β (π + π) = π) |
31 | 9, 24, 30 | syl2anc 585 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β (π + π) = π) |
32 | 29, 31 | sseqtrd 3985 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β (π + (π β© π)) β π) |
33 | 23, 32 | sstrd 3955 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β (π + (π β© π)) β π) |
34 | 14, 33 | ssind 4193 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β (π + (π β© π)) β ((π + π) β© π)) |
35 | 7, 34 | eqssd 3962 |
. 2
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ π β π) β ((π + π) β© π) = (π + (π β© π))) |
36 | 35 | ex 414 |
1
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β (π β π β ((π + π) β© π) = (π + (π β© π)))) |