Step | Hyp | Ref
| Expression |
1 | | incom 4162 |
. . . . . 6
β’ (π β© π) = (π β© π) |
2 | 1 | oveq1i 7368 |
. . . . 5
β’ ((π β© π) + π) = ((π β© π) + π) |
3 | | hllat 37828 |
. . . . . . 7
β’ (πΎ β HL β πΎ β Lat) |
4 | 3 | 3ad2ant1 1134 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β πΎ β Lat) |
5 | | simp22 1208 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
6 | | ssinss1 4198 |
. . . . . . 7
β’ (π β π΄ β (π β© π) β π΄) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β (π β© π) β π΄) |
8 | | simp23 1209 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
9 | | pmod.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
10 | | pmod.p |
. . . . . . 7
β’ + =
(+πβπΎ) |
11 | 9, 10 | paddcom 38279 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β© π) β π΄ β§ π β π΄) β ((π β© π) + π) = (π + (π β© π))) |
12 | 4, 7, 8, 11 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β ((π β© π) + π) = (π + (π β© π))) |
13 | 2, 12 | eqtrid 2789 |
. . . 4
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β ((π β© π) + π) = (π + (π β© π))) |
14 | | simp21 1207 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β π β π) |
15 | 8, 5, 14 | 3jca 1129 |
. . . . 5
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β (π β π΄ β§ π β π΄ β§ π β π)) |
16 | | pmod.s |
. . . . . . 7
β’ π = (PSubSpβπΎ) |
17 | 9, 16, 10 | pmod1i 38314 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β (π β π β ((π + π) β© π) = (π + (π β© π)))) |
18 | 17 | 3impia 1118 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β ((π + π) β© π) = (π + (π β© π))) |
19 | 15, 18 | syld3an2 1412 |
. . . 4
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β ((π + π) β© π) = (π + (π β© π))) |
20 | 9, 10 | paddcom 38279 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΄ β§ π β π΄) β (π + π) = (π + π)) |
21 | 4, 8, 5, 20 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β (π + π) = (π + π)) |
22 | 21 | ineq1d 4172 |
. . . 4
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β ((π + π) β© π) = ((π + π) β© π)) |
23 | 13, 19, 22 | 3eqtr2d 2783 |
. . 3
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β ((π β© π) + π) = ((π + π) β© π)) |
24 | | incom 4162 |
. . 3
β’ ((π + π) β© π) = (π β© (π + π)) |
25 | 23, 24 | eqtrdi 2793 |
. 2
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄) β§ π β π) β ((π β© π) + π) = (π β© (π + π))) |
26 | 25 | 3expia 1122 |
1
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄)) β (π β π β ((π β© π) + π) = (π β© (π + π)))) |