Step | Hyp | Ref
| Expression |
1 | | simp11l 1284 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β πΎ β HL) |
2 | | simp12l 1286 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β π β π΄) |
3 | | simp11 1203 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΎ β HL β§ π β π»)) |
4 | | simp2r 1200 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β πΊ β π) |
5 | | cdlemg12.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
6 | | cdlemg12.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
7 | | cdlemg12.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
8 | | cdlemg12.t |
. . . . . . 7
β’ π = ((LTrnβπΎ)βπ) |
9 | 5, 6, 7, 8 | ltrnat 38709 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ π β π΄) β (πΊβπ) β π΄) |
10 | 3, 4, 2, 9 | syl3anc 1371 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΊβπ) β π΄) |
11 | | cdlemg12.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
12 | 5, 11, 6 | hlatlej1 37943 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ (πΊβπ) β π΄) β π β€ (π β¨ (πΊβπ))) |
13 | 1, 2, 10, 12 | syl3anc 1371 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β π β€ (π β¨ (πΊβπ))) |
14 | | simp32 1210 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π
βπΉ) = (π
βπΊ)) |
15 | | simp2l 1199 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β πΉ β π) |
16 | | simp12 1204 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
17 | 5, 6, 7, 8 | ltrnel 38708 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) |
18 | 3, 4, 16, 17 | syl3anc 1371 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) |
19 | | cdlemg12.m |
. . . . . . . . 9
β’ β§ =
(meetβπΎ) |
20 | | cdlemg12b.r |
. . . . . . . . 9
β’ π
= ((trLβπΎ)βπ) |
21 | 5, 11, 19, 6, 7, 8,
20 | trlval2 38732 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) β (π
βπΉ) = (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π)) |
22 | 3, 15, 18, 21 | syl3anc 1371 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π
βπΉ) = (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π)) |
23 | 5, 11, 19, 6, 7, 8,
20 | trlval2 38732 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΊ) = ((π β¨ (πΊβπ)) β§ π)) |
24 | 3, 4, 16, 23 | syl3anc 1371 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π
βπΊ) = ((π β¨ (πΊβπ)) β§ π)) |
25 | 14, 22, 24 | 3eqtr3d 2779 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΊβπ)) β§ π)) |
26 | 25 | oveq2d 7393 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((πΊβπ) β¨ (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π)) = ((πΊβπ) β¨ ((π β¨ (πΊβπ)) β§ π))) |
27 | 5, 6, 7, 8 | ltrncoat 38713 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β (πΉβ(πΊβπ)) β π΄) |
28 | 3, 15, 4, 2, 27 | syl121anc 1375 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉβ(πΊβπ)) β π΄) |
29 | | eqid 2731 |
. . . . . . 7
β’ (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π) = (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π) |
30 | 5, 11, 19, 6, 7, 29 | cdleme0cp 38783 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π) β§ (πΉβ(πΊβπ)) β π΄)) β ((πΊβπ) β¨ (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π)) = ((πΊβπ) β¨ (πΉβ(πΊβπ)))) |
31 | 3, 18, 28, 30 | syl12anc 835 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((πΊβπ) β¨ (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π)) = ((πΊβπ) β¨ (πΉβ(πΊβπ)))) |
32 | | eqid 2731 |
. . . . . . 7
β’ ((π β¨ (πΊβπ)) β§ π) = ((π β¨ (πΊβπ)) β§ π) |
33 | 5, 11, 19, 6, 7, 32 | cdleme0cq 38784 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π))) β ((πΊβπ) β¨ ((π β¨ (πΊβπ)) β§ π)) = (π β¨ (πΊβπ))) |
34 | 3, 2, 18, 33 | syl12anc 835 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((πΊβπ) β¨ ((π β¨ (πΊβπ)) β§ π)) = (π β¨ (πΊβπ))) |
35 | 26, 31, 34 | 3eqtr3rd 2780 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β¨ (πΊβπ)) = ((πΊβπ) β¨ (πΉβ(πΊβπ)))) |
36 | 13, 35 | breqtrd 5151 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β π β€ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) |
37 | 5, 11, 6 | hlatlej2 37944 |
. . . 4
β’ ((πΎ β HL β§ (πΊβπ) β π΄ β§ (πΉβ(πΊβπ)) β π΄) β (πΉβ(πΊβπ)) β€ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) |
38 | 1, 10, 28, 37 | syl3anc 1371 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉβ(πΊβπ)) β€ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) |
39 | 1 | hllatd 37932 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β πΎ β Lat) |
40 | | eqid 2731 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
41 | 40, 6 | atbase 37857 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
42 | 2, 41 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β π β (BaseβπΎ)) |
43 | 40, 6 | atbase 37857 |
. . . . 5
β’ ((πΉβ(πΊβπ)) β π΄ β (πΉβ(πΊβπ)) β (BaseβπΎ)) |
44 | 28, 43 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉβ(πΊβπ)) β (BaseβπΎ)) |
45 | 40, 11, 6 | hlatjcl 37935 |
. . . . 5
β’ ((πΎ β HL β§ (πΊβπ) β π΄ β§ (πΉβ(πΊβπ)) β π΄) β ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
46 | 1, 10, 28, 45 | syl3anc 1371 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
47 | 40, 5, 11 | latjle12 18368 |
. . . 4
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (πΉβ(πΊβπ)) β (BaseβπΎ) β§ ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ))) β ((π β€ ((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ (πΉβ(πΊβπ)) β€ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) β (π β¨ (πΉβ(πΊβπ))) β€ ((πΊβπ) β¨ (πΉβ(πΊβπ))))) |
48 | 39, 42, 44, 46, 47 | syl13anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β€ ((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ (πΉβ(πΊβπ)) β€ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) β (π β¨ (πΉβ(πΊβπ))) β€ ((πΊβπ) β¨ (πΉβ(πΊβπ))))) |
49 | 36, 38, 48 | mpbi2and 710 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β¨ (πΉβ(πΊβπ))) β€ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) |
50 | | simp13 1205 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
51 | | simp33 1211 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π)) |
52 | 5, 11, 19, 6, 7, 8 | cdlemg11a 39206 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉβ(πΊβπ)) β π) |
53 | 3, 16, 50, 15, 4, 51, 52 | syl123anc 1387 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉβ(πΊβπ)) β π) |
54 | 53 | necomd 2995 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β π β (πΉβ(πΊβπ))) |
55 | 5, 11, 6 | ps-1 38046 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ (πΉβ(πΊβπ)) β π΄ β§ π β (πΉβ(πΊβπ))) β§ ((πΊβπ) β π΄ β§ (πΉβ(πΊβπ)) β π΄)) β ((π β¨ (πΉβ(πΊβπ))) β€ ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (π β¨ (πΉβ(πΊβπ))) = ((πΊβπ) β¨ (πΉβ(πΊβπ))))) |
56 | 1, 2, 28, 54, 10, 28, 55 | syl132anc 1388 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β€ ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (π β¨ (πΉβ(πΊβπ))) = ((πΊβπ) β¨ (πΉβ(πΊβπ))))) |
57 | 49, 56 | mpbid 231 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π
βπΉ) = (π
βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β¨ (πΉβ(πΊβπ))) = ((πΊβπ) β¨ (πΉβ(πΊβπ)))) |