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 ) |