Description: The projective map of the join of a lattice element and a lattice line (expressed as the join Q .\/ R of two atoms). (Contributed by NM, 16-Sep-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pmapjat.b | |
|
pmapjat.j | |
||
pmapjat.a | |
||
pmapjat.m | |
||
pmapjat.p | |
||
Assertion | pmapjlln1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pmapjat.b | |
|
2 | pmapjat.j | |
|
3 | pmapjat.a | |
|
4 | pmapjat.m | |
|
5 | pmapjat.p | |
|
6 | simpl | |
|
7 | 1 3 4 | pmapssat | |
8 | 7 | 3ad2antr1 | |
9 | simpr2 | |
|
10 | 1 3 | atbase | |
11 | 9 10 | syl | |
12 | 1 3 4 | pmapssat | |
13 | 11 12 | syldan | |
14 | simpr3 | |
|
15 | 1 3 | atbase | |
16 | 14 15 | syl | |
17 | 1 3 4 | pmapssat | |
18 | 16 17 | syldan | |
19 | 3 5 | paddass | |
20 | 6 8 13 18 19 | syl13anc | |
21 | hllat | |
|
22 | 21 | adantr | |
23 | simpr1 | |
|
24 | 1 2 | latjcl | |
25 | 22 23 11 24 | syl3anc | |
26 | 1 2 3 4 5 | pmapjat1 | |
27 | 6 25 14 26 | syl3anc | |
28 | 1 2 | latjass | |
29 | 22 23 11 16 28 | syl13anc | |
30 | 29 | fveq2d | |
31 | 1 2 3 4 5 | pmapjat1 | |
32 | 31 | 3adant3r3 | |
33 | 32 | oveq1d | |
34 | 27 30 33 | 3eqtr3d | |
35 | 1 2 3 4 5 | pmapjat1 | |
36 | 6 11 14 35 | syl3anc | |
37 | 36 | oveq2d | |
38 | 20 34 37 | 3eqtr4d | |