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 ˙ = join K
atexchcvr.a A = Atoms K
atexchcvr.c C = K
Assertion atexchcvrN K HL P A Q A R A P R P C Q ˙ R Q C P ˙ R

Proof

Step Hyp Ref Expression
1 atexchcvr.j ˙ = join K
2 atexchcvr.a A = Atoms K
3 atexchcvr.c C = K
4 simpl1 K HL P A Q A R A P R P C Q ˙ R K HL
5 simpl21 K HL P A Q A R A P R P C Q ˙ R P A
6 eqid Base K = Base K
7 6 2 atbase P A P Base K
8 5 7 syl K HL P A Q A R A P R P C Q ˙ R P Base K
9 4 hllatd K HL P A Q A R A P R P C Q ˙ R K Lat
10 simpl22 K HL P A Q A R A P R P C Q ˙ R Q A
11 6 2 atbase Q A Q Base K
12 10 11 syl K HL P A Q A R A P R P C Q ˙ R Q Base K
13 simpl23 K HL P A Q A R A P R P C Q ˙ R R A
14 6 2 atbase R A R Base K
15 13 14 syl K HL P A Q A R A P R P C Q ˙ R R Base K
16 6 1 latjcl K Lat Q Base K R Base K Q ˙ R Base K
17 9 12 15 16 syl3anc K HL P A Q A R A P R P C Q ˙ R Q ˙ R Base K
18 4 8 17 3jca K HL P A Q A R A P R P C Q ˙ R K HL P Base K Q ˙ R Base K
19 eqid K = K
20 6 19 3 cvrle K HL P Base K Q ˙ R Base K P C Q ˙ R P K Q ˙ R
21 18 20 sylancom K HL P A Q A R A P R P C Q ˙ R P K Q ˙ R
22 21 ex K HL P A Q A R A P R P C Q ˙ R P K Q ˙ R
23 19 1 2 hlatexch2 K HL P A Q A R A P R P K Q ˙ R Q K P ˙ R
24 simpl1 K HL P A Q A R A P R Q K P ˙ R K HL
25 simpl22 K HL P A Q A R A P R Q K P ˙ R Q A
26 simpl21 K HL P A Q A R A P R Q K P ˙ R P A
27 simpl23 K HL P A Q A R A P R Q K P ˙ R R A
28 simpl3 K HL P A Q A R A P R Q K P ˙ R P R
29 simpr K HL P A Q A R A P R Q K P ˙ R Q K P ˙ R
30 19 1 3 2 atcvrj2 K HL Q A P A R A P R Q K P ˙ R Q C P ˙ R
31 24 25 26 27 28 29 30 syl132anc K HL P A Q A R A P R Q K P ˙ R Q C P ˙ R
32 31 ex K HL P A Q A R A P R Q K P ˙ R Q C P ˙ R
33 22 23 32 3syld K HL P A Q A R A P R P C Q ˙ R Q C P ˙ R