Metamath Proof Explorer

Theorem dihvalcq2

Description: Value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . (Contributed by NM, 26-Sep-2014)

Ref Expression
Hypotheses dihvalcq2.b 
|- B = ( Base ` K )
dihvalcq2.l 
|- .<_ = ( le ` K )
dihvalcq2.j 
|- .\/ = ( join ` K )
dihvalcq2.m 
|- ./\ = ( meet ` K )
dihvalcq2.a 
|- A = ( Atoms ` K )
dihvalcq2.h 
|- H = ( LHyp ` K )
dihvalcq2.i 
|- I = ( ( DIsoH ` K ) ` W )
dihvalcq2.u 
|- U = ( ( DVecH ` K ) ` W )
dihvalcq2.p 
|- .(+) = ( LSSum ` U )
Assertion dihvalcq2 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( I ` X ) = ( ( I ` Q ) .(+) ( I ` ( X ./\ W ) ) ) )

Proof

Step Hyp Ref Expression
1 dihvalcq2.b 
 |-  B = ( Base ` K )
2 dihvalcq2.l 
 |-  .<_ = ( le ` K )
3 dihvalcq2.j 
 |-  .\/ = ( join ` K )
4 dihvalcq2.m 
 |-  ./\ = ( meet ` K )
5 dihvalcq2.a 
 |-  A = ( Atoms ` K )
6 dihvalcq2.h 
 |-  H = ( LHyp ` K )
7 dihvalcq2.i 
 |-  I = ( ( DIsoH ` K ) ` W )
8 dihvalcq2.u 
 |-  U = ( ( DVecH ` K ) ` W )
9 dihvalcq2.p 
 |-  .(+) = ( LSSum ` U )
10 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( K e. HL /\ W e. H ) )
11 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( X e. B /\ -. X .<_ W ) )
12 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( Q e. A /\ -. Q .<_ W ) )
13 simp3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> Q .<_ X )
14 1 2 3 4 5 6 lhpmcvr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q .<_ X <-> ( Q .\/ ( X ./\ W ) ) = X ) )
15 10 11 12 14 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( Q .<_ X <-> ( Q .\/ ( X ./\ W ) ) = X ) )
16 13 15 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( Q .\/ ( X ./\ W ) ) = X )
17 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
18 eqid 
 |-  ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )
19 1 2 3 4 5 6 7 17 18 8 9 dihvalcq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( I ` X ) = ( ( ( ( DIsoC ` K ) ` W ) ` Q ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ W ) ) ) )
20 10 11 12 16 19 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( I ` X ) = ( ( ( ( DIsoC ` K ) ` W ) ` Q ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ W ) ) ) )
21 2 5 6 18 7 dihvalcqat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( ( ( DIsoC ` K ) ` W ) ` Q ) )
22 10 12 21 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( I ` Q ) = ( ( ( DIsoC ` K ) ` W ) ` Q ) )
23 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> K e. HL )
24 23 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> K e. Lat )
25 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> X e. B )
26 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> W e. H )
27 1 6 lhpbase 
 |-  ( W e. H -> W e. B )
28 26 27 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> W e. B )
29 1 4 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
30 24 25 28 29 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( X ./\ W ) e. B )
31 1 2 4 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ W )
32 24 25 28 31 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( X ./\ W ) .<_ W )
33 1 2 6 7 17 dihvalb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X ./\ W ) e. B /\ ( X ./\ W ) .<_ W ) ) -> ( I ` ( X ./\ W ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ W ) ) )
34 10 30 32 33 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( I ` ( X ./\ W ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ W ) ) )
35 22 34 oveq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( ( I ` Q ) .(+) ( I ` ( X ./\ W ) ) ) = ( ( ( ( DIsoC ` K ) ` W ) ` Q ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ W ) ) ) )
36 20 35 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( I ` X ) = ( ( I ` Q ) .(+) ( I ` ( X ./\ W ) ) ) )