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 ` 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 e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( J ` Q ) )

Proof

Step Hyp Ref Expression
1 dihvalcqat.l 
 |-  .<_ = ( le ` 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 e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( K e. HL /\ W e. H ) )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 7 2 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
9 8 ad2antrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> Q e. ( Base ` K ) )
10 simprr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> -. Q .<_ W )
11 simpr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q e. A /\ -. Q .<_ W ) )
12 eqid 
 |-  ( meet ` K ) = ( meet ` K )
13 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
14 1 12 13 2 3 lhpmat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q ( meet ` K ) W ) = ( 0. ` K ) )
15 14 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q ( join ` K ) ( Q ( meet ` K ) W ) ) = ( Q ( join ` K ) ( 0. ` K ) ) )
16 hlol 
 |-  ( K e. HL -> K e. OL )
17 16 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> K e. OL )
18 eqid 
 |-  ( join ` K ) = ( join ` K )
19 7 18 13 olj01 
 |-  ( ( K e. OL /\ Q e. ( Base ` K ) ) -> ( Q ( join ` K ) ( 0. ` K ) ) = Q )
20 17 9 19 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q ( join ` K ) ( 0. ` K ) ) = Q )
21 15 20 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. 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 e. HL /\ W e. H ) /\ ( Q e. ( Base ` K ) /\ -. Q .<_ W ) /\ ( ( Q e. 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 e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) ) )
27 14 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( 0. ` K ) ) )
28 eqid 
 |-  ( 0g ` ( ( DVecH ` K ) ` W ) ) = ( 0g ` ( ( DVecH ` K ) ` W ) )
29 13 3 22 23 28 dib0 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( DIsoB ` K ) ` W ) ` ( 0. ` K ) ) = { ( 0g ` ( ( DVecH ` K ) ` W ) ) } )
30 29 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( 0. ` K ) ) = { ( 0g ` ( ( DVecH ` K ) ` W ) ) } )
31 27 30 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) = { ( 0g ` ( ( DVecH ` K ) ` W ) ) } )
32 31 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) ) = ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) { ( 0g ` ( ( DVecH ` K ) ` W ) ) } ) )
33 3 23 6 dvhlmod 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( DVecH ` K ) ` W ) e. LMod )
34 eqid 
 |-  ( LSubSp ` ( ( DVecH ` K ) ` W ) ) = ( LSubSp ` ( ( DVecH ` K ) ` W ) )
35 1 2 3 23 4 34 diclss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( J ` Q ) e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) )
36 34 lsssubg 
 |-  ( ( ( ( DVecH ` K ) ` W ) e. LMod /\ ( J ` Q ) e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) ) -> ( J ` Q ) e. ( SubGrp ` ( ( DVecH ` K ) ` W ) ) )
37 33 35 36 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( J ` Q ) e. ( SubGrp ` ( ( DVecH ` K ) ` W ) ) )
38 28 24 lsm01 
 |-  ( ( J ` Q ) e. ( SubGrp ` ( ( DVecH ` K ) ` W ) ) -> ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) { ( 0g ` ( ( DVecH ` K ) ` W ) ) } ) = ( J ` Q ) )
39 37 38 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) { ( 0g ` ( ( DVecH ` K ) ` W ) ) } ) = ( J ` Q ) )
40 32 39 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) ) = ( J ` Q ) )
41 26 40 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( J ` Q ) )