Metamath Proof Explorer


Theorem dihmeetlem19N

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

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

Proof

Step Hyp Ref Expression
1 dihmeetlem14.b B = Base K
2 dihmeetlem14.l ˙ = K
3 dihmeetlem14.h H = LHyp K
4 dihmeetlem14.j ˙ = join K
5 dihmeetlem14.m ˙ = meet K
6 dihmeetlem14.a A = Atoms K
7 dihmeetlem14.u U = DVecH K W
8 dihmeetlem14.s ˙ = LSSum U
9 dihmeetlem14.i I = DIsoH K W
10 incom I p I Y = I Y I p
11 eqid 0 U = 0 U
12 1 2 3 4 5 6 7 8 9 11 dihmeetlem18N K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W I Y I p = 0 U
13 10 12 syl5eq K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W I p I Y = 0 U
14 13 oveq2d K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W I X ˙ Y ˙ I p I Y = I X ˙ Y ˙ 0 U
15 simpl1 K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W K HL W H
16 simpl2l K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W X B
17 simpl3 K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W Y B
18 simpr1 K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W p A ¬ p ˙ W
19 simpr31 K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W p ˙ X
20 simpr33 K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W X ˙ Y ˙ W
21 1 2 3 4 5 6 7 8 9 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
22 15 16 17 18 19 20 21 syl33anc K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W I X ˙ Y ˙ I p I Y = I X I Y
23 3 7 15 dvhlmod K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W U LMod
24 simpl1l K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W K HL
25 24 hllatd K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W K Lat
26 1 5 latmcl K Lat X B Y B X ˙ Y B
27 25 16 17 26 syl3anc K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W X ˙ Y B
28 eqid LSubSp U = LSubSp U
29 1 3 9 7 28 dihlss K HL W H X ˙ Y B I X ˙ Y LSubSp U
30 15 27 29 syl2anc K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W I X ˙ Y LSubSp U
31 28 lsssubg U LMod I X ˙ Y LSubSp U I X ˙ Y SubGrp U
32 23 30 31 syl2anc K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W I X ˙ Y SubGrp U
33 11 8 lsm01 I X ˙ Y SubGrp U I X ˙ Y ˙ 0 U = I X ˙ Y
34 32 33 syl K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W I X ˙ Y ˙ 0 U = I X ˙ Y
35 14 22 34 3eqtr3rd K HL W H X B ¬ X ˙ W Y B p A ¬ p ˙ W r A ¬ r ˙ W p ˙ X r ˙ Y X ˙ Y ˙ W I X ˙ Y = I X I Y