Metamath Proof Explorer


Theorem pmapjlln1

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 B=BaseK
pmapjat.j ˙=joinK
pmapjat.a A=AtomsK
pmapjat.m M=pmapK
pmapjat.p +˙=+𝑃K
Assertion pmapjlln1 KHLXBQARAMX˙Q˙R=MX+˙MQ˙R

Proof

Step Hyp Ref Expression
1 pmapjat.b B=BaseK
2 pmapjat.j ˙=joinK
3 pmapjat.a A=AtomsK
4 pmapjat.m M=pmapK
5 pmapjat.p +˙=+𝑃K
6 simpl KHLXBQARAKHL
7 1 3 4 pmapssat KHLXBMXA
8 7 3ad2antr1 KHLXBQARAMXA
9 simpr2 KHLXBQARAQA
10 1 3 atbase QAQB
11 9 10 syl KHLXBQARAQB
12 1 3 4 pmapssat KHLQBMQA
13 11 12 syldan KHLXBQARAMQA
14 simpr3 KHLXBQARARA
15 1 3 atbase RARB
16 14 15 syl KHLXBQARARB
17 1 3 4 pmapssat KHLRBMRA
18 16 17 syldan KHLXBQARAMRA
19 3 5 paddass KHLMXAMQAMRAMX+˙MQ+˙MR=MX+˙MQ+˙MR
20 6 8 13 18 19 syl13anc KHLXBQARAMX+˙MQ+˙MR=MX+˙MQ+˙MR
21 hllat KHLKLat
22 21 adantr KHLXBQARAKLat
23 simpr1 KHLXBQARAXB
24 1 2 latjcl KLatXBQBX˙QB
25 22 23 11 24 syl3anc KHLXBQARAX˙QB
26 1 2 3 4 5 pmapjat1 KHLX˙QBRAMX˙Q˙R=MX˙Q+˙MR
27 6 25 14 26 syl3anc KHLXBQARAMX˙Q˙R=MX˙Q+˙MR
28 1 2 latjass KLatXBQBRBX˙Q˙R=X˙Q˙R
29 22 23 11 16 28 syl13anc KHLXBQARAX˙Q˙R=X˙Q˙R
30 29 fveq2d KHLXBQARAMX˙Q˙R=MX˙Q˙R
31 1 2 3 4 5 pmapjat1 KHLXBQAMX˙Q=MX+˙MQ
32 31 3adant3r3 KHLXBQARAMX˙Q=MX+˙MQ
33 32 oveq1d KHLXBQARAMX˙Q+˙MR=MX+˙MQ+˙MR
34 27 30 33 3eqtr3d KHLXBQARAMX˙Q˙R=MX+˙MQ+˙MR
35 1 2 3 4 5 pmapjat1 KHLQBRAMQ˙R=MQ+˙MR
36 6 11 14 35 syl3anc KHLXBQARAMQ˙R=MQ+˙MR
37 36 oveq2d KHLXBQARAMX+˙MQ˙R=MX+˙MQ+˙MR
38 20 34 37 3eqtr4d KHLXBQARAMX˙Q˙R=MX+˙MQ˙R