# 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 ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( 𝐼𝑄 ) = ( 𝐽𝑄 ) )