Metamath Proof Explorer


Theorem dihmeetlem5

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 6-Apr-2014)

Ref Expression
Hypotheses dihmeetlem5.b B = Base K
dihmeetlem5.l ˙ = K
dihmeetlem5.j ˙ = join K
dihmeetlem5.m ˙ = meet K
dihmeetlem5.a A = Atoms K
Assertion dihmeetlem5 K HL X B Y B Q A Q ˙ X X ˙ Y ˙ Q = X ˙ Y ˙ Q

Proof

Step Hyp Ref Expression
1 dihmeetlem5.b B = Base K
2 dihmeetlem5.l ˙ = K
3 dihmeetlem5.j ˙ = join K
4 dihmeetlem5.m ˙ = meet K
5 dihmeetlem5.a A = Atoms K
6 simpl1 K HL X B Y B Q A Q ˙ X K HL
7 simprl K HL X B Y B Q A Q ˙ X Q A
8 simpl2 K HL X B Y B Q A Q ˙ X X B
9 simpl3 K HL X B Y B Q A Q ˙ X Y B
10 simprr K HL X B Y B Q A Q ˙ X Q ˙ X
11 1 2 3 4 5 atmod2i1 K HL Q A X B Y B Q ˙ X X ˙ Y ˙ Q = X ˙ Y ˙ Q
12 6 7 8 9 10 11 syl131anc K HL X B Y B Q A Q ˙ X X ˙ Y ˙ Q = X ˙ Y ˙ Q
13 12 eqcomd K HL X B Y B Q A Q ˙ X X ˙ Y ˙ Q = X ˙ Y ˙ Q