This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihmeetlem4preN

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

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

Proof

Step Hyp Ref Expression
1 dihmeetlem4.b 
 |-  B = ( Base ` K )
2 dihmeetlem4.l 
 |-  .<_ = ( le ` K )
3 dihmeetlem4.m 
 |-  ./\ = ( meet ` K )
4 dihmeetlem4.a 
 |-  A = ( Atoms ` K )
5 dihmeetlem4.h 
 |-  H = ( LHyp ` K )
6 dihmeetlem4.i 
 |-  I = ( ( DIsoH ` K ) ` W )
7 dihmeetlem4.u 
 |-  U = ( ( DVecH ` K ) ` W )
8 dihmeetlem4.z 
 |-  .0. = ( 0g ` U )
9 dihmeetlem4.g 
 |-  G = ( iota_ g e. T ( g ` P ) = Q )
10 dihmeetlem4.p 
 |-  P = ( ( oc ` K ) ` W )
11 dihmeetlem4.t 
 |-  T = ( ( LTrn ` K ) ` W )
12 dihmeetlem4.r 
 |-  R = ( ( trL ` K ) ` W )
13 dihmeetlem4.e 
 |-  E = ( ( TEndo ` K ) ` W )
14 dihmeetlem4.o 
 |-  O = ( h e. T |-> ( _I |` B ) )
15 5 6 dihvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` Q ) )
16 relin1 
 |-  ( Rel ( I ` Q ) -> Rel ( ( I ` Q ) i^i ( I ` ( X ./\ W ) ) ) )
17 15 16 syl 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( ( I ` Q ) i^i ( I ` ( X ./\ W ) ) ) )
18 17 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> Rel ( ( I ` Q ) i^i ( I ` ( X ./\ W ) ) ) )
19 5 6 dihvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` ( 0. ` K ) ) )
20 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
21 20 5 6 7 8 dih0 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` ( 0. ` K ) ) = { .0. } )
22 21 releqd 
 |-  ( ( K e. HL /\ W e. H ) -> ( Rel ( I ` ( 0. ` K ) ) <-> Rel { .0. } ) )
23 19 22 mpbid 
 |-  ( ( K e. HL /\ W e. H ) -> Rel { .0. } )
24 23 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> Rel { .0. } )
25 id 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) )
26 elin 
 |-  ( <. f , s >. e. ( ( I ` Q ) i^i ( I ` ( X ./\ W ) ) ) <-> ( <. f , s >. e. ( I ` Q ) /\ <. f , s >. e. ( I ` ( X ./\ W ) ) ) )
27 vex 
 |-  f e. _V
28 vex 
 |-  s e. _V
29 2 4 5 10 11 13 6 9 27 28 dihopelvalcqat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. f , s >. e. ( I ` Q ) <-> ( f = ( s ` G ) /\ s e. E ) ) )
30 29 3adant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. f , s >. e. ( I ` Q ) <-> ( f = ( s ` G ) /\ s e. E ) ) )
31 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( K e. HL /\ W e. H ) )
32 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> K e. HL )
33 32 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> K e. Lat )
34 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> X e. B )
35 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> W e. H )
36 1 5 lhpbase 
 |-  ( W e. H -> W e. B )
37 35 36 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> W e. B )
38 1 3 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
39 33 34 37 38 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( X ./\ W ) e. B )
40 1 2 3 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ W )
41 33 34 37 40 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( X ./\ W ) .<_ W )
42 1 2 5 11 12 14 6 dihopelvalbN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X ./\ W ) e. B /\ ( X ./\ W ) .<_ W ) ) -> ( <. f , s >. e. ( I ` ( X ./\ W ) ) <-> ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) )
43 31 39 41 42 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. f , s >. e. ( I ` ( X ./\ W ) ) <-> ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) )
44 30 43 anbi12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( <. f , s >. e. ( I ` Q ) /\ <. f , s >. e. ( I ` ( X ./\ W ) ) ) <-> ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) )
45 simprll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) -> f = ( s ` G ) )
46 simprrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) -> s = O )
47 46 fveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) -> ( s ` G ) = ( O ` G ) )
48 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) -> ( K e. HL /\ W e. H ) )
49 2 4 5 10 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
50 48 49 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) -> ( P e. A /\ -. P .<_ W ) )
51 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
52 2 4 5 11 9 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> G e. T )
53 48 50 51 52 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) -> G e. T )
54 14 1 tendo02 
 |-  ( G e. T -> ( O ` G ) = ( _I |` B ) )
55 53 54 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) -> ( O ` G ) = ( _I |` B ) )
56 45 47 55 3eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) -> f = ( _I |` B ) )
57 56 46 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) ) -> ( f = ( _I |` B ) /\ s = O ) )
58 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( K e. HL /\ W e. H ) )
59 58 49 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( P e. A /\ -. P .<_ W ) )
60 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( Q e. A /\ -. Q .<_ W ) )
61 58 59 60 52 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> G e. T )
62 61 54 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( O ` G ) = ( _I |` B ) )
63 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> s = O )
64 63 fveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( s ` G ) = ( O ` G ) )
65 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> f = ( _I |` B ) )
66 62 64 65 3eqtr4rd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> f = ( s ` G ) )
67 1 5 11 13 14 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> O e. E )
68 58 67 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> O e. E )
69 63 68 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> s e. E )
70 1 5 11 idltrn 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. T )
71 58 70 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( _I |` B ) e. T )
72 65 71 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> f e. T )
73 65 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( R ` f ) = ( R ` ( _I |` B ) ) )
74 1 20 5 12 trlid0 
 |-  ( ( K e. HL /\ W e. H ) -> ( R ` ( _I |` B ) ) = ( 0. ` K ) )
75 58 74 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( R ` ( _I |` B ) ) = ( 0. ` K ) )
76 73 75 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( R ` f ) = ( 0. ` K ) )
77 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> K e. HL )
78 hlatl 
 |-  ( K e. HL -> K e. AtLat )
79 77 78 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> K e. AtLat )
80 39 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( X ./\ W ) e. B )
81 1 2 20 atl0le 
 |-  ( ( K e. AtLat /\ ( X ./\ W ) e. B ) -> ( 0. ` K ) .<_ ( X ./\ W ) )
82 79 80 81 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( 0. ` K ) .<_ ( X ./\ W ) )
83 76 82 eqbrtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( R ` f ) .<_ ( X ./\ W ) )
84 72 83 63 jca31 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) )
85 66 69 84 jca31 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( _I |` B ) /\ s = O ) ) -> ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) )
86 57 85 impbida 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( f = ( s ` G ) /\ s e. E ) /\ ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = O ) ) <-> ( f = ( _I |` B ) /\ s = O ) ) )
87 44 86 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( <. f , s >. e. ( I ` Q ) /\ <. f , s >. e. ( I ` ( X ./\ W ) ) ) <-> ( f = ( _I |` B ) /\ s = O ) ) )
88 opex 
 |-  <. f , s >. e. _V
89 88 elsn 
 |-  ( <. f , s >. e. { <. ( _I |` B ) , O >. } <-> <. f , s >. = <. ( _I |` B ) , O >. )
90 27 28 opth 
 |-  ( <. f , s >. = <. ( _I |` B ) , O >. <-> ( f = ( _I |` B ) /\ s = O ) )
91 89 90 bitr2i 
 |-  ( ( f = ( _I |` B ) /\ s = O ) <-> <. f , s >. e. { <. ( _I |` B ) , O >. } )
92 87 91 bitrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( <. f , s >. e. ( I ` Q ) /\ <. f , s >. e. ( I ` ( X ./\ W ) ) ) <-> <. f , s >. e. { <. ( _I |` B ) , O >. } ) )
93 1 5 11 7 8 14 dvh0g 
 |-  ( ( K e. HL /\ W e. H ) -> .0. = <. ( _I |` B ) , O >. )
94 93 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> .0. = <. ( _I |` B ) , O >. )
95 94 sneqd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> { .0. } = { <. ( _I |` B ) , O >. } )
96 95 eleq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. f , s >. e. { .0. } <-> <. f , s >. e. { <. ( _I |` B ) , O >. } ) )
97 92 96 bitr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( <. f , s >. e. ( I ` Q ) /\ <. f , s >. e. ( I ` ( X ./\ W ) ) ) <-> <. f , s >. e. { .0. } ) )
98 26 97 bitrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. f , s >. e. ( ( I ` Q ) i^i ( I ` ( X ./\ W ) ) ) <-> <. f , s >. e. { .0. } ) )
99 98 eqrelrdv2 
 |-  ( ( ( Rel ( ( I ` Q ) i^i ( I ` ( X ./\ W ) ) ) /\ Rel { .0. } ) /\ ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) ) -> ( ( I ` Q ) i^i ( I ` ( X ./\ W ) ) ) = { .0. } )
100 18 24 25 99 syl21anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( I ` Q ) i^i ( I ` ( X ./\ W ) ) ) = { .0. } )