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