Metamath Proof Explorer

Theorem dihvalcqat

Description: Value of isomorphism H for a lattice K at an atom not under W . (Contributed by NM, 27-Mar-2014)

Ref Expression
Hypotheses dihvalcqat.l ⊢ ≤ ˙ = ≤ K
dihvalcqat.a ⊢ A = Atoms ⁡ K
dihvalcqat.h ⊢ H = LHyp ⁡ K
dihvalcqat.j ⊢ J = DIsoC ⁡ K ⁡ W
dihvalcqat.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihvalcqat ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q = J ⁡ Q

Proof

Step Hyp Ref Expression
1 dihvalcqat.l ⊢ ≤ ˙ = ≤ K
2 dihvalcqat.a ⊢ A = Atoms ⁡ K
3 dihvalcqat.h ⊢ H = LHyp ⁡ K
4 dihvalcqat.j ⊢ J = DIsoC ⁡ K ⁡ W
5 dihvalcqat.i ⊢ I = DIsoH ⁡ K ⁡ W
6 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → K ∈ HL ∧ W ∈ H
7 eqid ⊢ Base K = Base K
8 7 2 atbase ⊢ Q ∈ A → Q ∈ Base K
9 8 ad2antrl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∈ Base K
10 simprr ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → ¬ Q ≤ ˙ W
11 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∈ A ∧ ¬ Q ≤ ˙ W
12 eqid ⊢ meet ⁡ K = meet ⁡ K
13 eqid ⊢ 0. ⁡ K = 0. ⁡ K
14 1 12 13 2 3 lhpmat ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q meet ⁡ K W = 0. ⁡ K
15 14 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q join ⁡ K Q meet ⁡ K W = Q join ⁡ K 0. ⁡ K
16 hlol ⊢ K ∈ HL → K ∈ OL
17 16 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → K ∈ OL
18 eqid ⊢ join ⁡ K = join ⁡ K
19 7 18 13 olj01 ⊢ K ∈ OL ∧ Q ∈ Base K → Q join ⁡ K 0. ⁡ K = Q
20 17 9 19 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q join ⁡ K 0. ⁡ K = Q
21 15 20 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q join ⁡ K Q meet ⁡ K W = Q
22 eqid ⊢ DIsoB ⁡ K ⁡ W = DIsoB ⁡ K ⁡ W
23 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
24 eqid ⊢ LSSum ⁡ DVecH ⁡ K ⁡ W = LSSum ⁡ DVecH ⁡ K ⁡ W
25 7 1 18 12 2 3 5 22 4 23 24 dihvalcq ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ Base K ∧ ¬ Q ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ Q join ⁡ K Q meet ⁡ K W = Q → I ⁡ Q = J ⁡ Q LSSum ⁡ DVecH ⁡ K ⁡ W DIsoB ⁡ K ⁡ W ⁡ Q meet ⁡ K W
26 6 9 10 11 21 25 syl122anc ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q = J ⁡ Q LSSum ⁡ DVecH ⁡ K ⁡ W DIsoB ⁡ K ⁡ W ⁡ Q meet ⁡ K W
27 14 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → DIsoB ⁡ K ⁡ W ⁡ Q meet ⁡ K W = DIsoB ⁡ K ⁡ W ⁡ 0. ⁡ K
28 eqid ⊢ 0 DVecH ⁡ K ⁡ W = 0 DVecH ⁡ K ⁡ W
29 13 3 22 23 28 dib0 ⊢ K ∈ HL ∧ W ∈ H → DIsoB ⁡ K ⁡ W ⁡ 0. ⁡ K = 0 DVecH ⁡ K ⁡ W
30 29 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → DIsoB ⁡ K ⁡ W ⁡ 0. ⁡ K = 0 DVecH ⁡ K ⁡ W
31 27 30 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → DIsoB ⁡ K ⁡ W ⁡ Q meet ⁡ K W = 0 DVecH ⁡ K ⁡ W
32 31 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → J ⁡ Q LSSum ⁡ DVecH ⁡ K ⁡ W DIsoB ⁡ K ⁡ W ⁡ Q meet ⁡ K W = J ⁡ Q LSSum ⁡ DVecH ⁡ K ⁡ W 0 DVecH ⁡ K ⁡ W
33 3 23 6 dvhlmod ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → DVecH ⁡ K ⁡ W ∈ LMod
34 eqid ⊢ LSubSp ⁡ DVecH ⁡ K ⁡ W = LSubSp ⁡ DVecH ⁡ K ⁡ W
35 1 2 3 23 4 34 diclss ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → J ⁡ Q ∈ LSubSp ⁡ DVecH ⁡ K ⁡ W
36 34 lsssubg ⊢ DVecH ⁡ K ⁡ W ∈ LMod ∧ J ⁡ Q ∈ LSubSp ⁡ DVecH ⁡ K ⁡ W → J ⁡ Q ∈ SubGrp ⁡ DVecH ⁡ K ⁡ W
37 33 35 36 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → J ⁡ Q ∈ SubGrp ⁡ DVecH ⁡ K ⁡ W
38 28 24 lsm01 ⊢ J ⁡ Q ∈ SubGrp ⁡ DVecH ⁡ K ⁡ W → J ⁡ Q LSSum ⁡ DVecH ⁡ K ⁡ W 0 DVecH ⁡ K ⁡ W = J ⁡ Q
39 37 38 syl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → J ⁡ Q LSSum ⁡ DVecH ⁡ K ⁡ W 0 DVecH ⁡ K ⁡ W = J ⁡ Q
40 32 39 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → J ⁡ Q LSSum ⁡ DVecH ⁡ K ⁡ W DIsoB ⁡ K ⁡ W ⁡ Q meet ⁡ K W = J ⁡ Q
41 26 40 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q = J ⁡ Q