Metamath Proof Explorer


Theorem dihmeetlem12N

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

Ref Expression
Hypotheses dihmeetlem9.b B = Base K
dihmeetlem9.l ˙ = K
dihmeetlem9.h H = LHyp K
dihmeetlem9.j ˙ = join K
dihmeetlem9.m ˙ = meet K
dihmeetlem9.a A = Atoms K
dihmeetlem9.u U = DVecH K W
dihmeetlem9.s ˙ = LSSum U
dihmeetlem9.i I = DIsoH K W
Assertion dihmeetlem12N K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W I X ˙ Y ˙ I p I Y = I X I Y

Proof

Step Hyp Ref Expression
1 dihmeetlem9.b B = Base K
2 dihmeetlem9.l ˙ = K
3 dihmeetlem9.h H = LHyp K
4 dihmeetlem9.j ˙ = join K
5 dihmeetlem9.m ˙ = meet K
6 dihmeetlem9.a A = Atoms K
7 dihmeetlem9.u U = DVecH K W
8 dihmeetlem9.s ˙ = LSSum U
9 dihmeetlem9.i I = DIsoH K W
10 simpl1 K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W K HL W H
11 simpl2 K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W X B
12 simpl3 K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W Y B
13 simpr1 K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W p A ¬ p ˙ W
14 simpr2 K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W p ˙ X
15 simpr3 K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W X ˙ Y ˙ W
16 1 2 3 4 5 6 7 8 9 dihmeetlem8N K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W I X ˙ Y ˙ p = I p ˙ I X ˙ Y
17 10 11 12 13 14 15 16 syl312anc K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W I X ˙ Y ˙ p = I p ˙ I X ˙ Y
18 17 ineq1d K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W I X ˙ Y ˙ p I Y = I p ˙ I X ˙ Y I Y
19 1 2 3 4 5 6 7 8 9 dihmeetlem11N K HL W H X B Y B p A ¬ p ˙ W p ˙ X I X ˙ Y ˙ p I Y = I X I Y
20 19 3adantr3 K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W I X ˙ Y ˙ p I Y = I X I Y
21 simpr1l K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W p A
22 1 2 3 4 5 6 7 8 9 dihmeetlem9N K HL W H X B Y B p A I p ˙ I X ˙ Y I Y = I X ˙ Y ˙ I p I Y
23 10 11 12 21 22 syl121anc K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W I p ˙ I X ˙ Y I Y = I X ˙ Y ˙ I p I Y
24 18 20 23 3eqtr3rd K HL W H X B Y B p A ¬ p ˙ W p ˙ X X ˙ Y ˙ W I X ˙ Y ˙ I p I Y = I X I Y