Metamath Proof Explorer


Theorem atexchcvrN

Description: Atom exchange property. Version of hlatexch2 with covers relation. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses atexchcvr.j ˙=joinK
atexchcvr.a A=AtomsK
atexchcvr.c C=K
Assertion atexchcvrN KHLPAQARAPRPCQ˙RQCP˙R

Proof

Step Hyp Ref Expression
1 atexchcvr.j ˙=joinK
2 atexchcvr.a A=AtomsK
3 atexchcvr.c C=K
4 simpl1 KHLPAQARAPRPCQ˙RKHL
5 simpl21 KHLPAQARAPRPCQ˙RPA
6 eqid BaseK=BaseK
7 6 2 atbase PAPBaseK
8 5 7 syl KHLPAQARAPRPCQ˙RPBaseK
9 4 hllatd KHLPAQARAPRPCQ˙RKLat
10 simpl22 KHLPAQARAPRPCQ˙RQA
11 6 2 atbase QAQBaseK
12 10 11 syl KHLPAQARAPRPCQ˙RQBaseK
13 simpl23 KHLPAQARAPRPCQ˙RRA
14 6 2 atbase RARBaseK
15 13 14 syl KHLPAQARAPRPCQ˙RRBaseK
16 6 1 latjcl KLatQBaseKRBaseKQ˙RBaseK
17 9 12 15 16 syl3anc KHLPAQARAPRPCQ˙RQ˙RBaseK
18 4 8 17 3jca KHLPAQARAPRPCQ˙RKHLPBaseKQ˙RBaseK
19 eqid K=K
20 6 19 3 cvrle KHLPBaseKQ˙RBaseKPCQ˙RPKQ˙R
21 18 20 sylancom KHLPAQARAPRPCQ˙RPKQ˙R
22 21 ex KHLPAQARAPRPCQ˙RPKQ˙R
23 19 1 2 hlatexch2 KHLPAQARAPRPKQ˙RQKP˙R
24 simpl1 KHLPAQARAPRQKP˙RKHL
25 simpl22 KHLPAQARAPRQKP˙RQA
26 simpl21 KHLPAQARAPRQKP˙RPA
27 simpl23 KHLPAQARAPRQKP˙RRA
28 simpl3 KHLPAQARAPRQKP˙RPR
29 simpr KHLPAQARAPRQKP˙RQKP˙R
30 19 1 3 2 atcvrj2 KHLQAPARAPRQKP˙RQCP˙R
31 24 25 26 27 28 29 30 syl132anc KHLPAQARAPRQKP˙RQCP˙R
32 31 ex KHLPAQARAPRQKP˙RQCP˙R
33 22 23 32 3syld KHLPAQARAPRPCQ˙RQCP˙R