Metamath Proof Explorer

Theorem dihmeetlem13N

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem13.b 
|- B = ( Base ` K )
dihmeetlem13.l 
|- .<_ = ( le ` K )
dihmeetlem13.j 
|- .\/ = ( join ` K )
dihmeetlem13.a 
|- A = ( Atoms ` K )
dihmeetlem13.h 
|- H = ( LHyp ` K )
dihmeetlem13.p 
|- P = ( ( oc ` K ) ` W )
dihmeetlem13.t 
|- T = ( ( LTrn ` K ) ` W )
dihmeetlem13.e 
|- E = ( ( TEndo ` K ) ` W )
dihmeetlem13.o 
|- O = ( h e. T |-> ( _I |` B ) )
dihmeetlem13.i 
|- I = ( ( DIsoH ` K ) ` W )
dihmeetlem13.u 
|- U = ( ( DVecH ` K ) ` W )
dihmeetlem13.z 
|- .0. = ( 0g ` U )
dihmeetlem13.f 
|- F = ( iota_ h e. T ( h ` P ) = Q )
dihmeetlem13.g 
|- G = ( iota_ h e. T ( h ` P ) = R )
Assertion dihmeetlem13N 
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( ( I ` Q ) i^i ( I ` R ) ) = { .0. } )

Proof

Step Hyp Ref Expression
1 dihmeetlem13.b 
 |-  B = ( Base ` K )
2 dihmeetlem13.l 
 |-  .<_ = ( le ` K )
3 dihmeetlem13.j 
 |-  .\/ = ( join ` K )
4 dihmeetlem13.a 
 |-  A = ( Atoms ` K )
5 dihmeetlem13.h 
 |-  H = ( LHyp ` K )
6 dihmeetlem13.p 
 |-  P = ( ( oc ` K ) ` W )
7 dihmeetlem13.t 
 |-  T = ( ( LTrn ` K ) ` W )
8 dihmeetlem13.e 
 |-  E = ( ( TEndo ` K ) ` W )
9 dihmeetlem13.o 
 |-  O = ( h e. T |-> ( _I |` B ) )
10 dihmeetlem13.i 
 |-  I = ( ( DIsoH ` K ) ` W )
11 dihmeetlem13.u 
 |-  U = ( ( DVecH ` K ) ` W )
12 dihmeetlem13.z 
 |-  .0. = ( 0g ` U )
13 dihmeetlem13.f 
 |-  F = ( iota_ h e. T ( h ` P ) = Q )
14 dihmeetlem13.g 
 |-  G = ( iota_ h e. T ( h ` P ) = R )
15 5 10 dihvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` Q ) )
16 15 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> Rel ( I ` Q ) )
17 relin1 
 |-  ( Rel ( I ` Q ) -> Rel ( ( I ` Q ) i^i ( I ` R ) ) )
18 16 17 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> Rel ( ( I ` Q ) i^i ( I ` R ) ) )
19 elin 
 |-  ( <. f , s >. e. ( ( I ` Q ) i^i ( I ` R ) ) <-> ( <. f , s >. e. ( I ` Q ) /\ <. f , s >. e. ( I ` R ) ) )
20 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( K e. HL /\ W e. H ) )
21 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( Q e. A /\ -. Q .<_ W ) )
22 vex 
 |-  f e. _V
23 vex 
 |-  s e. _V
24 2 4 5 6 7 8 10 13 22 23 dihopelvalcqat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. f , s >. e. ( I ` Q ) <-> ( f = ( s ` F ) /\ s e. E ) ) )
25 20 21 24 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( <. f , s >. e. ( I ` Q ) <-> ( f = ( s ` F ) /\ s e. E ) ) )
26 simp2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( R e. A /\ -. R .<_ W ) )
27 2 4 5 6 7 8 10 14 22 23 dihopelvalcqat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( <. f , s >. e. ( I ` R ) <-> ( f = ( s ` G ) /\ s e. E ) ) )
28 20 26 27 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( <. f , s >. e. ( I ` R ) <-> ( f = ( s ` G ) /\ s e. E ) ) )
29 25 28 anbi12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( ( <. f , s >. e. ( I ` Q ) /\ <. f , s >. e. ( I ` R ) ) <-> ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) )
30 19 29 bitrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( <. f , s >. e. ( ( I ` Q ) i^i ( I ` R ) ) <-> ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) )
31 simprll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> f = ( s ` F ) )
32 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> Q =/= R )
33 fveq1 
 |-  ( F = G -> ( F ` P ) = ( G ` P ) )
34 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( K e. HL /\ W e. H ) )
35 2 4 5 6 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
36 34 35 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( P e. A /\ -. P .<_ W ) )
37 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
38 2 4 5 7 13 ltrniotaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( F ` P ) = Q )
39 34 36 37 38 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( F ` P ) = Q )
40 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( R e. A /\ -. R .<_ W ) )
41 2 4 5 7 14 ltrniotaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( G ` P ) = R )
42 34 36 40 41 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( G ` P ) = R )
43 39 42 eqeq12d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( ( F ` P ) = ( G ` P ) <-> Q = R ) )
44 33 43 imbitrid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( F = G -> Q = R ) )
45 44 necon3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( Q =/= R -> F =/= G ) )
46 32 45 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> F =/= G )
47 simp2ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> f = ( s ` F ) )
48 simp2rl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> f = ( s ` G ) )
49 47 48 eqtr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> ( s ` F ) = ( s ` G ) )
50 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> ( K e. HL /\ W e. H ) )
51 simp2rr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> s e. E )
52 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> s =/= O )
53 50 35 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> ( P e. A /\ -. P .<_ W ) )
54 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> ( Q e. A /\ -. Q .<_ W ) )
55 2 4 5 7 13 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> F e. T )
56 50 53 54 55 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> F e. T )
57 simp12r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> ( R e. A /\ -. R .<_ W ) )
58 2 4 5 7 14 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> G e. T )
59 50 53 57 58 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> G e. T )
60 1 5 7 8 9 tendospcanN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ s =/= O ) /\ ( F e. T /\ G e. T ) ) -> ( ( s ` F ) = ( s ` G ) <-> F = G ) )
61 50 51 52 56 59 60 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> ( ( s ` F ) = ( s ` G ) <-> F = G ) )
62 49 61 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) /\ s =/= O ) -> F = G )
63 62 3expia 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( s =/= O -> F = G ) )
64 63 necon1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( F =/= G -> s = O ) )
65 46 64 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> s = O )
66 65 fveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( s ` F ) = ( O ` F ) )
67 34 36 37 55 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> F e. T )
68 9 1 tendo02 
 |-  ( F e. T -> ( O ` F ) = ( _I |` B ) )
69 67 68 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( O ` F ) = ( _I |` B ) )
70 31 66 69 3eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> f = ( _I |` B ) )
71 70 65 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) /\ ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) ) -> ( f = ( _I |` B ) /\ s = O ) )
72 71 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( ( ( f = ( s ` F ) /\ s e. E ) /\ ( f = ( s ` G ) /\ s e. E ) ) -> ( f = ( _I |` B ) /\ s = O ) ) )
73 30 72 sylbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( <. f , s >. e. ( ( I ` Q ) i^i ( I ` R ) ) -> ( f = ( _I |` B ) /\ s = O ) ) )
74 opex 
 |-  <. f , s >. e. _V
75 74 elsn 
 |-  ( <. f , s >. e. { <. ( _I |` B ) , O >. } <-> <. f , s >. = <. ( _I |` B ) , O >. )
76 22 23 opth 
 |-  ( <. f , s >. = <. ( _I |` B ) , O >. <-> ( f = ( _I |` B ) /\ s = O ) )
77 75 76 bitr2i 
 |-  ( ( f = ( _I |` B ) /\ s = O ) <-> <. f , s >. e. { <. ( _I |` B ) , O >. } )
78 1 5 7 11 12 9 dvh0g 
 |-  ( ( K e. HL /\ W e. H ) -> .0. = <. ( _I |` B ) , O >. )
79 78 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> .0. = <. ( _I |` B ) , O >. )
80 79 sneqd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> { .0. } = { <. ( _I |` B ) , O >. } )
81 80 eleq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( <. f , s >. e. { .0. } <-> <. f , s >. e. { <. ( _I |` B ) , O >. } ) )
82 77 81 bitr4id 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( ( f = ( _I |` B ) /\ s = O ) <-> <. f , s >. e. { .0. } ) )
83 73 82 sylibd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( <. f , s >. e. ( ( I ` Q ) i^i ( I ` R ) ) -> <. f , s >. e. { .0. } ) )
84 18 83 relssdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( ( I ` Q ) i^i ( I ` R ) ) C_ { .0. } )
85 5 11 20 dvhlmod 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> U e. LMod )
86 simp2ll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> Q e. A )
87 1 4 atbase 
 |-  ( Q e. A -> Q e. B )
88 86 87 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> Q e. B )
89 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
90 1 5 10 11 89 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. B ) -> ( I ` Q ) e. ( LSubSp ` U ) )
91 20 88 90 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( I ` Q ) e. ( LSubSp ` U ) )
92 simp2rl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> R e. A )
93 1 4 atbase 
 |-  ( R e. A -> R e. B )
94 92 93 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> R e. B )
95 1 5 10 11 89 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. B ) -> ( I ` R ) e. ( LSubSp ` U ) )
96 20 94 95 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( I ` R ) e. ( LSubSp ` U ) )
97 89 lssincl 
 |-  ( ( U e. LMod /\ ( I ` Q ) e. ( LSubSp ` U ) /\ ( I ` R ) e. ( LSubSp ` U ) ) -> ( ( I ` Q ) i^i ( I ` R ) ) e. ( LSubSp ` U ) )
98 85 91 96 97 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( ( I ` Q ) i^i ( I ` R ) ) e. ( LSubSp ` U ) )
99 12 89 lss0ss 
 |-  ( ( U e. LMod /\ ( ( I ` Q ) i^i ( I ` R ) ) e. ( LSubSp ` U ) ) -> { .0. } C_ ( ( I ` Q ) i^i ( I ` R ) ) )
100 85 98 99 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> { .0. } C_ ( ( I ` Q ) i^i ( I ` R ) ) )
101 84 100 eqssd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ Q =/= R ) -> ( ( I ` Q ) i^i ( I ` R ) ) = { .0. } )