Metamath Proof Explorer

Theorem dihjatc1

Description: Lemma for isomorphism H of a lattice meet. TODO: shorter proof if we change .\/ order of ( X ./\ Y ) .\/ Q here and down? (Contributed by NM, 6-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 dihjatc1.b 
 |-  B = ( Base ` K )
2 dihjatc1.l 
 |-  .<_ = ( le ` K )
3 dihjatc1.h 
 |-  H = ( LHyp ` K )
4 dihjatc1.j 
 |-  .\/ = ( join ` K )
5 dihjatc1.m 
 |-  ./\ = ( meet ` K )
6 dihjatc1.a 
 |-  A = ( Atoms ` K )
7 dihjatc1.u 
 |-  U = ( ( DVecH ` K ) ` W )
8 dihjatc1.s 
 |-  .(+) = ( LSSum ` U )
9 dihjatc1.i 
 |-  I = ( ( DIsoH ` K ) ` W )
10 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( K e. HL /\ W e. H ) )
11 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> K e. HL )
12 11 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> K e. Lat )
13 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> X e. B )
14 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> Y e. B )
15 1 5 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
16 12 13 14 15 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( X ./\ Y ) e. B )
17 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> Q e. A )
18 1 6 atbase 
 |-  ( Q e. A -> Q e. B )
19 17 18 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> Q e. B )
20 1 4 latjcl 
 |-  ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ Q e. B ) -> ( ( X ./\ Y ) .\/ Q ) e. B )
21 12 16 19 20 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( ( X ./\ Y ) .\/ Q ) e. B )
22 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( Q e. A /\ -. Q .<_ W ) )
23 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> Q .<_ X )
24 1 2 3 4 5 6 dihmeetlem6 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> -. ( X ./\ ( Y .\/ Q ) ) .<_ W )
25 10 13 14 22 23 24 syl32anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> -. ( X ./\ ( Y .\/ Q ) ) .<_ W )
26 1 2 4 5 6 dihmeetlem5 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> ( X ./\ ( Y .\/ Q ) ) = ( ( X ./\ Y ) .\/ Q ) )
27 11 13 14 17 23 26 syl32anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( X ./\ ( Y .\/ Q ) ) = ( ( X ./\ Y ) .\/ Q ) )
28 27 breq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( ( X ./\ ( Y .\/ Q ) ) .<_ W <-> ( ( X ./\ Y ) .\/ Q ) .<_ W ) )
29 25 28 mtbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> -. ( ( X ./\ Y ) .\/ Q ) .<_ W )
30 1 2 4 latlej2 
 |-  ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ Q e. B ) -> Q .<_ ( ( X ./\ Y ) .\/ Q ) )
31 12 16 19 30 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> Q .<_ ( ( X ./\ Y ) .\/ Q ) )
32 1 2 4 5 6 3 9 7 8 dihvalcq2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( X ./\ Y ) .\/ Q ) e. B /\ -. ( ( X ./\ Y ) .\/ Q ) .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ ( ( X ./\ Y ) .\/ Q ) ) ) -> ( I ` ( ( X ./\ Y ) .\/ Q ) ) = ( ( I ` Q ) .(+) ( I ` ( ( ( X ./\ Y ) .\/ Q ) ./\ W ) ) ) )
33 10 21 29 22 31 32 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` ( ( X ./\ Y ) .\/ Q ) ) = ( ( I ` Q ) .(+) ( I ` ( ( ( X ./\ Y ) .\/ Q ) ./\ W ) ) ) )
34 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
35 2 5 34 6 3 lhpmat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q ./\ W ) = ( 0. ` K ) )
36 10 22 35 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( Q ./\ W ) = ( 0. ` K ) )
37 36 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( ( X ./\ Y ) .\/ ( Q ./\ W ) ) = ( ( X ./\ Y ) .\/ ( 0. ` K ) ) )
38 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> W e. H )
39 1 3 lhpbase 
 |-  ( W e. H -> W e. B )
40 38 39 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> W e. B )
41 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( X ./\ Y ) .<_ W )
42 1 2 4 5 6 atmod1i2 
 |-  ( ( K e. HL /\ ( Q e. A /\ ( X ./\ Y ) e. B /\ W e. B ) /\ ( X ./\ Y ) .<_ W ) -> ( ( X ./\ Y ) .\/ ( Q ./\ W ) ) = ( ( ( X ./\ Y ) .\/ Q ) ./\ W ) )
43 11 17 16 40 41 42 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( ( X ./\ Y ) .\/ ( Q ./\ W ) ) = ( ( ( X ./\ Y ) .\/ Q ) ./\ W ) )
44 hlol 
 |-  ( K e. HL -> K e. OL )
45 11 44 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> K e. OL )
46 1 4 34 olj01 
 |-  ( ( K e. OL /\ ( X ./\ Y ) e. B ) -> ( ( X ./\ Y ) .\/ ( 0. ` K ) ) = ( X ./\ Y ) )
47 45 16 46 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( ( X ./\ Y ) .\/ ( 0. ` K ) ) = ( X ./\ Y ) )
48 37 43 47 3eqtr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( ( ( X ./\ Y ) .\/ Q ) ./\ W ) = ( X ./\ Y ) )
49 48 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` ( ( ( X ./\ Y ) .\/ Q ) ./\ W ) ) = ( I ` ( X ./\ Y ) ) )
50 49 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( ( I ` Q ) .(+) ( I ` ( ( ( X ./\ Y ) .\/ Q ) ./\ W ) ) ) = ( ( I ` Q ) .(+) ( I ` ( X ./\ Y ) ) ) )
51 33 50 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` ( ( X ./\ Y ) .\/ Q ) ) = ( ( I ` Q ) .(+) ( I ` ( X ./\ Y ) ) ) )