Metamath Proof Explorer


Theorem dihmeetlem7N

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem7.b B = Base K
dihmeetlem7.l ˙ = K
dihmeetlem7.j ˙ = join K
dihmeetlem7.m ˙ = meet K
dihmeetlem7.a A = Atoms K
Assertion dihmeetlem7N K HL X B Y B p A ¬ p ˙ Y X ˙ Y ˙ p ˙ Y = X ˙ Y

Proof

Step Hyp Ref Expression
1 dihmeetlem7.b B = Base K
2 dihmeetlem7.l ˙ = K
3 dihmeetlem7.j ˙ = join K
4 dihmeetlem7.m ˙ = meet K
5 dihmeetlem7.a A = Atoms K
6 simprr K HL X B Y B p A ¬ p ˙ Y ¬ p ˙ Y
7 simpl1 K HL X B Y B p A ¬ p ˙ Y K HL
8 hlatl K HL K AtLat
9 7 8 syl K HL X B Y B p A ¬ p ˙ Y K AtLat
10 simprl K HL X B Y B p A ¬ p ˙ Y p A
11 simpl3 K HL X B Y B p A ¬ p ˙ Y Y B
12 eqid 0. K = 0. K
13 1 2 4 12 5 atnle K AtLat p A Y B ¬ p ˙ Y p ˙ Y = 0. K
14 9 10 11 13 syl3anc K HL X B Y B p A ¬ p ˙ Y ¬ p ˙ Y p ˙ Y = 0. K
15 6 14 mpbid K HL X B Y B p A ¬ p ˙ Y p ˙ Y = 0. K
16 15 oveq2d K HL X B Y B p A ¬ p ˙ Y X ˙ Y ˙ p ˙ Y = X ˙ Y ˙ 0. K
17 7 hllatd K HL X B Y B p A ¬ p ˙ Y K Lat
18 simpl2 K HL X B Y B p A ¬ p ˙ Y X B
19 1 4 latmcl K Lat X B Y B X ˙ Y B
20 17 18 11 19 syl3anc K HL X B Y B p A ¬ p ˙ Y X ˙ Y B
21 1 2 4 latmle2 K Lat X B Y B X ˙ Y ˙ Y
22 17 18 11 21 syl3anc K HL X B Y B p A ¬ p ˙ Y X ˙ Y ˙ Y
23 1 2 3 4 5 atmod1i2 K HL p A X ˙ Y B Y B X ˙ Y ˙ Y X ˙ Y ˙ p ˙ Y = X ˙ Y ˙ p ˙ Y
24 7 10 20 11 22 23 syl131anc K HL X B Y B p A ¬ p ˙ Y X ˙ Y ˙ p ˙ Y = X ˙ Y ˙ p ˙ Y
25 hlol K HL K OL
26 7 25 syl K HL X B Y B p A ¬ p ˙ Y K OL
27 1 3 12 olj01 K OL X ˙ Y B X ˙ Y ˙ 0. K = X ˙ Y
28 26 20 27 syl2anc K HL X B Y B p A ¬ p ˙ Y X ˙ Y ˙ 0. K = X ˙ Y
29 16 24 28 3eqtr3d K HL X B Y B p A ¬ p ˙ Y X ˙ Y ˙ p ˙ Y = X ˙ Y