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

Metamath Proof Explorer

Theorem dihatlat

Description: The isomorphism H of an atom is a 1-dim subspace. (Contributed by NM, 28-Apr-2014)

Ref Expression
Hypotheses dihatlat.a 
|- A = ( Atoms ` K )
dihatlat.h 
|- H = ( LHyp ` K )
dihatlat.u 
|- U = ( ( DVecH ` K ) ` W )
dihatlat.i 
|- I = ( ( DIsoH ` K ) ` W )
dihatlat.l 
|- L = ( LSAtoms ` U )
Assertion dihatlat 
|- ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) -> ( I ` Q ) e. L )

Proof

Step Hyp Ref Expression
1 dihatlat.a 
 |-  A = ( Atoms ` K )
2 dihatlat.h 
 |-  H = ( LHyp ` K )
3 dihatlat.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dihatlat.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 dihatlat.l 
 |-  L = ( LSAtoms ` U )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 eqid 
 |-  ( le ` K ) = ( le ` K )
8 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
9 eqid 
 |-  ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) )
10 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
11 6 7 1 2 8 9 3 4 10 dih1dimb2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ Q ( le ` K ) W ) ) -> E. g e. ( ( LTrn ` K ) ` W ) ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) )
12 11 anassrs 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W ) -> E. g e. ( ( LTrn ` K ) ` W ) ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) )
13 simp3rr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) )
14 simp1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> ( K e. HL /\ W e. H ) )
15 2 3 14 dvhlmod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> U e. LMod )
16 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> g e. ( ( LTrn ` K ) ` W ) )
17 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
18 6 2 8 17 9 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) e. ( ( TEndo ` K ) ` W ) )
19 14 18 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) e. ( ( TEndo ` K ) ` W ) )
20 eqid 
 |-  ( Base ` U ) = ( Base ` U )
21 2 8 17 3 20 dvhelvbasei 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) e. ( ( TEndo ` K ) ` W ) ) ) -> <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. e. ( Base ` U ) )
22 14 16 19 21 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. e. ( Base ` U ) )
23 simp3rl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> g =/= ( _I |` ( Base ` K ) ) )
24 23 neneqd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> -. g = ( _I |` ( Base ` K ) ) )
25 24 intnanrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> -. ( g = ( _I |` ( Base ` K ) ) /\ ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) )
26 vex 
 |-  g e. _V
27 fvex 
 |-  ( ( LTrn ` K ) ` W ) e. _V
28 27 mptex 
 |-  ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) e. _V
29 26 28 opth 
 |-  ( <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. = <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. <-> ( g = ( _I |` ( Base ` K ) ) /\ ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) )
30 29 necon3abii 
 |-  ( <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. =/= <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. <-> -. ( g = ( _I |` ( Base ` K ) ) /\ ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) )
31 25 30 sylibr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. =/= <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. )
32 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
33 6 2 8 3 32 9 dvh0g 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` U ) = <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. )
34 14 33 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> ( 0g ` U ) = <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. )
35 31 34 neeqtrrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. =/= ( 0g ` U ) )
36 20 10 32 5 lsatlspsn2 
 |-  ( ( U e. LMod /\ <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. e. ( Base ` U ) /\ <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. =/= ( 0g ` U ) ) -> ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) e. L )
37 15 22 35 36 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) e. L )
38 13 37 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> ( I ` Q ) e. L )
39 38 3expa 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W ) /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( g =/= ( _I |` ( Base ` K ) ) /\ ( I ` Q ) = ( ( LSpan ` U ) ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } ) ) ) ) -> ( I ` Q ) e. L )
40 12 39 rexlimddv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ Q ( le ` K ) W ) -> ( I ` Q ) e. L )
41 eqid 
 |-  ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
42 eqid 
 |-  ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) = ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q )
43 7 1 2 41 8 4 3 10 42 dih1dimc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q ( le ` K ) W ) ) -> ( I ` Q ) = ( ( LSpan ` U ) ` { <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) )
44 43 anassrs 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( I ` Q ) = ( ( LSpan ` U ) ` { <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) )
45 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( K e. HL /\ W e. H ) )
46 2 3 45 dvhlmod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> U e. LMod )
47 eqid 
 |-  ( oc ` K ) = ( oc ` K )
48 7 47 1 2 lhpocnel 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) )
49 48 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) )
50 simplr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> Q e. A )
51 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> -. Q ( le ` K ) W )
52 7 1 2 8 42 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) /\ ( Q e. A /\ -. Q ( le ` K ) W ) ) -> ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) )
53 45 49 50 51 52 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) )
54 2 8 17 tendoidcl 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` ( ( LTrn ` K ) ` W ) ) e. ( ( TEndo ` K ) ` W ) )
55 54 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( _I |` ( ( LTrn ` K ) ` W ) ) e. ( ( TEndo ` K ) ` W ) )
56 2 8 17 3 20 dvhelvbasei 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) /\ ( _I |` ( ( LTrn ` K ) ` W ) ) e. ( ( TEndo ` K ) ` W ) ) ) -> <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. ( Base ` U ) )
57 45 53 55 56 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. ( Base ` U ) )
58 6 2 8 17 9 tendo1ne0 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` ( ( LTrn ` K ) ` W ) ) =/= ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) )
59 58 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( _I |` ( ( LTrn ` K ) ` W ) ) =/= ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) )
60 59 neneqd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> -. ( _I |` ( ( LTrn ` K ) ` W ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) )
61 60 intnand 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> -. ( ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) = ( _I |` ( Base ` K ) ) /\ ( _I |` ( ( LTrn ` K ) ` W ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) )
62 riotaex 
 |-  ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) e. _V
63 resiexg 
 |-  ( ( ( LTrn ` K ) ` W ) e. _V -> ( _I |` ( ( LTrn ` K ) ` W ) ) e. _V )
64 27 63 ax-mp 
 |-  ( _I |` ( ( LTrn ` K ) ` W ) ) e. _V
65 62 64 opth 
 |-  ( <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. = <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. <-> ( ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) = ( _I |` ( Base ` K ) ) /\ ( _I |` ( ( LTrn ` K ) ` W ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) )
66 65 necon3abii 
 |-  ( <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. =/= <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. <-> -. ( ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) = ( _I |` ( Base ` K ) ) /\ ( _I |` ( ( LTrn ` K ) ` W ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) )
67 61 66 sylibr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. =/= <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. )
68 33 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( 0g ` U ) = <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. )
69 67 68 neeqtrrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. =/= ( 0g ` U ) )
70 20 10 32 5 lsatlspsn2 
 |-  ( ( U e. LMod /\ <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. ( Base ` U ) /\ <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. =/= ( 0g ` U ) ) -> ( ( LSpan ` U ) ` { <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) e. L )
71 46 57 69 70 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( ( LSpan ` U ) ` { <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) e. L )
72 44 71 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( I ` Q ) e. L )
73 40 72 pm2.61dan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) -> ( I ` Q ) e. L )