Metamath Proof Explorer

Theorem dihvalcqpre

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

Ref Expression
Hypotheses dihval.b 
|- B = ( Base ` K )
dihval.l 
|- .<_ = ( le ` K )
dihval.j 
|- .\/ = ( join ` K )
dihval.m 
|- ./\ = ( meet ` K )
dihval.a 
|- A = ( Atoms ` K )
dihval.h 
|- H = ( LHyp ` K )
dihval.i 
|- I = ( ( DIsoH ` K ) ` W )
dihval.d 
|- D = ( ( DIsoB ` K ) ` W )
dihval.c 
|- C = ( ( DIsoC ` K ) ` W )
dihval.u 
|- U = ( ( DVecH ` K ) ` W )
dihval.s 
|- S = ( LSubSp ` U )
dihval.p 
|- .(+) = ( LSSum ` U )
Assertion dihvalcqpre 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( I ` X ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) )

Proof

Step Hyp Ref Expression
1 dihval.b 
 |-  B = ( Base ` K )
2 dihval.l 
 |-  .<_ = ( le ` K )
3 dihval.j 
 |-  .\/ = ( join ` K )
4 dihval.m 
 |-  ./\ = ( meet ` K )
5 dihval.a 
 |-  A = ( Atoms ` K )
6 dihval.h 
 |-  H = ( LHyp ` K )
7 dihval.i 
 |-  I = ( ( DIsoH ` K ) ` W )
8 dihval.d 
 |-  D = ( ( DIsoB ` K ) ` W )
9 dihval.c 
 |-  C = ( ( DIsoC ` K ) ` W )
10 dihval.u 
 |-  U = ( ( DVecH ` K ) ` W )
11 dihval.s 
 |-  S = ( LSubSp ` U )
12 dihval.p 
 |-  .(+) = ( LSSum ` U )
13 11 fvexi 
 |-  S e. _V
14 nfv 
 |-  F/ q ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) )
15 nfvd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> F/ q ( I ` X ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) )
16 1 2 3 4 5 6 7 8 9 10 11 12 dihvalc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( I ` X ) = ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
17 16 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( I ` X ) = ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
18 eqeq1 
 |-  ( ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( I ` X ) -> ( ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) <-> ( I ` X ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) ) )
19 18 adantl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( I ` X ) ) -> ( ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) <-> ( I ` X ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) ) )
20 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( K e. HL /\ W e. H ) )
21 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> q e. A )
22 simprrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> -. q .<_ W )
23 21 22 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( q e. A /\ -. q .<_ W ) )
24 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
25 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> X e. B )
26 simprrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( q .\/ ( X ./\ W ) ) = X )
27 simpl3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( Q .\/ ( X ./\ W ) ) = X )
28 26 27 eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( q .\/ ( X ./\ W ) ) = ( Q .\/ ( X ./\ W ) ) )
29 1 2 3 4 5 6 8 9 10 12 dihjust 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ X e. B ) /\ ( q .\/ ( X ./\ W ) ) = ( Q .\/ ( X ./\ W ) ) ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) )
30 20 23 24 25 28 29 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) )
31 30 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) -> ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) ) )
32 1 2 3 4 5 6 7 8 9 10 11 12 dihlsscpre 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( I ` X ) e. S )
33 32 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( I ` X ) e. S )
34 1 2 3 4 5 6 lhpmcvr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> E. q e. A ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) )
35 34 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> E. q e. A ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) )
36 14 15 17 19 31 33 35 riotasv3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) /\ S e. _V ) -> ( I ` X ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) )
37 13 36 mpan2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( I ` X ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) )