Metamath Proof Explorer


Theorem llnexch2N

Description: Line exchange property (compare cvlatexch2 for atoms). (Contributed by NM, 18-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses llnexch.l ˙ = K
llnexch.j ˙ = join K
llnexch.m ˙ = meet K
llnexch.a A = Atoms K
llnexch.n N = LLines K
Assertion llnexch2N K HL X N Y N Z N X ˙ Y A X Z X ˙ Y ˙ Z X ˙ Z ˙ Y

Proof

Step Hyp Ref Expression
1 llnexch.l ˙ = K
2 llnexch.j ˙ = join K
3 llnexch.m ˙ = meet K
4 llnexch.a A = Atoms K
5 llnexch.n N = LLines K
6 1 2 3 4 5 llnexchb2 K HL X N Y N Z N X ˙ Y A X Z X ˙ Y ˙ Z X ˙ Y = X ˙ Z
7 hllat K HL K Lat
8 7 3ad2ant1 K HL X N Y N Z N X ˙ Y A X Z K Lat
9 simp21 K HL X N Y N Z N X ˙ Y A X Z X N
10 eqid Base K = Base K
11 10 5 llnbase X N X Base K
12 9 11 syl K HL X N Y N Z N X ˙ Y A X Z X Base K
13 simp22 K HL X N Y N Z N X ˙ Y A X Z Y N
14 10 5 llnbase Y N Y Base K
15 13 14 syl K HL X N Y N Z N X ˙ Y A X Z Y Base K
16 10 1 3 latmle2 K Lat X Base K Y Base K X ˙ Y ˙ Y
17 8 12 15 16 syl3anc K HL X N Y N Z N X ˙ Y A X Z X ˙ Y ˙ Y
18 breq1 X ˙ Y = X ˙ Z X ˙ Y ˙ Y X ˙ Z ˙ Y
19 17 18 syl5ibcom K HL X N Y N Z N X ˙ Y A X Z X ˙ Y = X ˙ Z X ˙ Z ˙ Y
20 6 19 sylbid K HL X N Y N Z N X ˙ Y A X Z X ˙ Y ˙ Z X ˙ Z ˙ Y