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 ⊢ ≤ = ( le ‘ 𝐾 )
dihvalcqat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihvalcqat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihvalcqat.j ⊢ 𝐽 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
dihvalcqat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihvalcqat ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( 𝐽 ‘ 𝑄 ) )

Proof

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