Metamath Proof Explorer


Theorem dihmeetlem9N

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 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

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 simp1 K HL W H X B Y B p A K HL W H
11 3 7 10 dvhlmod K HL W H X B Y B p A U LMod
12 eqid LSubSp U = LSubSp U
13 12 lsssssubg U LMod LSubSp U SubGrp U
14 11 13 syl K HL W H X B Y B p A LSubSp U SubGrp U
15 simp1l K HL W H X B Y B p A K HL
16 15 hllatd K HL W H X B Y B p A K Lat
17 simp2l K HL W H X B Y B p A X B
18 simp2r K HL W H X B Y B p A Y B
19 1 5 latmcl K Lat X B Y B X ˙ Y B
20 16 17 18 19 syl3anc K HL W H X B Y B p A X ˙ Y B
21 1 3 9 7 12 dihlss K HL W H X ˙ Y B I X ˙ Y LSubSp U
22 10 20 21 syl2anc K HL W H X B Y B p A I X ˙ Y LSubSp U
23 14 22 sseldd K HL W H X B Y B p A I X ˙ Y SubGrp U
24 1 6 atbase p A p B
25 24 3ad2ant3 K HL W H X B Y B p A p B
26 1 3 9 7 12 dihlss K HL W H p B I p LSubSp U
27 10 25 26 syl2anc K HL W H X B Y B p A I p LSubSp U
28 14 27 sseldd K HL W H X B Y B p A I p SubGrp U
29 1 3 9 7 12 dihlss K HL W H Y B I Y LSubSp U
30 10 18 29 syl2anc K HL W H X B Y B p A I Y LSubSp U
31 14 30 sseldd K HL W H X B Y B p A I Y SubGrp U
32 1 2 5 latmle2 K Lat X B Y B X ˙ Y ˙ Y
33 16 17 18 32 syl3anc K HL W H X B Y B p A X ˙ Y ˙ Y
34 1 2 3 9 dihord K HL W H X ˙ Y B Y B I X ˙ Y I Y X ˙ Y ˙ Y
35 10 20 18 34 syl3anc K HL W H X B Y B p A I X ˙ Y I Y X ˙ Y ˙ Y
36 33 35 mpbird K HL W H X B Y B p A I X ˙ Y I Y
37 8 lsmmod I X ˙ Y SubGrp U I p SubGrp U I Y SubGrp U I X ˙ Y I Y I X ˙ Y ˙ I p I Y = I X ˙ Y ˙ I p I Y
38 23 28 31 36 37 syl31anc K HL W H X B Y B p A I X ˙ Y ˙ I p I Y = I X ˙ Y ˙ I p I Y
39 lmodabl U LMod U Abel
40 11 39 syl K HL W H X B Y B p A U Abel
41 8 lsmcom U Abel I X ˙ Y SubGrp U I p SubGrp U I X ˙ Y ˙ I p = I p ˙ I X ˙ Y
42 40 23 28 41 syl3anc K HL W H X B Y B p A I X ˙ Y ˙ I p = I p ˙ I X ˙ Y
43 42 ineq1d K HL W H X B Y B p A I X ˙ Y ˙ I p I Y = I p ˙ I X ˙ Y I Y
44 38 43 eqtr2d K HL W H X B Y B p A I p ˙ I X ˙ Y I Y = I X ˙ Y ˙ I p I Y