Step | Hyp | Ref
| Expression |
1 | | pmapojoin.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | pmapojoin.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
3 | | pmapojoin.m |
. . . 4
β’ π = (pmapβπΎ) |
4 | | pmapojoin.p |
. . . 4
β’ + =
(+πβπΎ) |
5 | | eqid 2731 |
. . . 4
β’
(β₯πβπΎ) = (β₯πβπΎ) |
6 | 1, 2, 3, 4, 5 | pmapj2N 39104 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πβ(π β¨ π)) =
((β₯πβπΎ)β((β₯πβπΎ)β((πβπ) + (πβπ))))) |
7 | 6 | adantr 480 |
. 2
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β (πβ(π β¨ π)) =
((β₯πβπΎ)β((β₯πβπΎ)β((πβπ) + (πβπ))))) |
8 | | simpl1 1190 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β πΎ β HL) |
9 | | simpl2 1191 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β π β π΅) |
10 | | eqid 2731 |
. . . . . 6
β’
(PSubClβπΎ) =
(PSubClβπΎ) |
11 | 1, 3, 10 | pmapsubclN 39121 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅) β (πβπ) β (PSubClβπΎ)) |
12 | 8, 9, 11 | syl2anc 583 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β (πβπ) β (PSubClβπΎ)) |
13 | | simpl3 1192 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β π β π΅) |
14 | 1, 3, 10 | pmapsubclN 39121 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅) β (πβπ) β (PSubClβπΎ)) |
15 | 8, 13, 14 | syl2anc 583 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β (πβπ) β (PSubClβπΎ)) |
16 | | hlop 38536 |
. . . . . . . . 9
β’ (πΎ β HL β πΎ β OP) |
17 | 16 | 3ad2ant1 1132 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β πΎ β OP) |
18 | | simp3 1137 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β π β π΅) |
19 | | pmapojoin.o |
. . . . . . . . 9
β’ β₯ =
(ocβπΎ) |
20 | 1, 19 | opoccl 38368 |
. . . . . . . 8
β’ ((πΎ β OP β§ π β π΅) β ( β₯ βπ) β π΅) |
21 | 17, 18, 20 | syl2anc 583 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ( β₯ βπ) β π΅) |
22 | | pmapojoin.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
23 | 1, 22, 3 | pmaple 38936 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΅ β§ ( β₯ βπ) β π΅) β (π β€ ( β₯ βπ) β (πβπ) β (πβ( β₯ βπ)))) |
24 | 21, 23 | syld3an3 1408 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ ( β₯ βπ) β (πβπ) β (πβ( β₯ βπ)))) |
25 | 24 | biimpa 476 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β (πβπ) β (πβ( β₯ βπ))) |
26 | 1, 19, 3, 5 | polpmapN 39087 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅) β
((β₯πβπΎ)β(πβπ)) = (πβ( β₯ βπ))) |
27 | 8, 13, 26 | syl2anc 583 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β
((β₯πβπΎ)β(πβπ)) = (πβ( β₯ βπ))) |
28 | 25, 27 | sseqtrrd 4024 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β (πβπ) β
((β₯πβπΎ)β(πβπ))) |
29 | 4, 5, 10 | osumclN 39142 |
. . . 4
β’ (((πΎ β HL β§ (πβπ) β (PSubClβπΎ) β§ (πβπ) β (PSubClβπΎ)) β§ (πβπ) β
((β₯πβπΎ)β(πβπ))) β ((πβπ) + (πβπ)) β (PSubClβπΎ)) |
30 | 8, 12, 15, 28, 29 | syl31anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β ((πβπ) + (πβπ)) β (PSubClβπΎ)) |
31 | 5, 10 | psubcli2N 39114 |
. . 3
β’ ((πΎ β HL β§ ((πβπ) + (πβπ)) β (PSubClβπΎ)) β
((β₯πβπΎ)β((β₯πβπΎ)β((πβπ) + (πβπ)))) = ((πβπ) + (πβπ))) |
32 | 8, 30, 31 | syl2anc 583 |
. 2
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β
((β₯πβπΎ)β((β₯πβπΎ)β((πβπ) + (πβπ)))) = ((πβπ) + (πβπ))) |
33 | 7, 32 | eqtrd 2771 |
1
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β (πβ(π β¨ π)) = ((πβπ) + (πβπ))) |