Metamath Proof Explorer

Theorem dihlatat

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

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

Proof

Step Hyp Ref Expression
1 dihlatat.a 
 |-  A = ( Atoms ` K )
2 dihlatat.h 
 |-  H = ( LHyp ` K )
3 dihlatat.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dihlatat.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 dihlatat.l 
 |-  L = ( LSAtoms ` U )
6 id 
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
7 2 3 6 dvhlvec 
 |-  ( ( K e. HL /\ W e. H ) -> U e. LVec )
8 eqid 
 |-  ( Base ` U ) = ( Base ` U )
9 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
10 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
11 8 9 10 5 islsat 
 |-  ( U e. LVec -> ( Q e. L <-> E. v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) Q = ( ( LSpan ` U ) ` { v } ) ) )
12 7 11 syl 
 |-  ( ( K e. HL /\ W e. H ) -> ( Q e. L <-> E. v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) Q = ( ( LSpan ` U ) ` { v } ) ) )
13 12 biimpa 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. L ) -> E. v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) Q = ( ( LSpan ` U ) ` { v } ) )
14 eldifsn 
 |-  ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) <-> ( v e. ( Base ` U ) /\ v =/= ( 0g ` U ) ) )
15 1 2 3 8 10 9 4 dihlspsnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ v e. ( Base ` U ) /\ v =/= ( 0g ` U ) ) -> ( `' I ` ( ( LSpan ` U ) ` { v } ) ) e. A )
16 15 3expb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( v e. ( Base ` U ) /\ v =/= ( 0g ` U ) ) ) -> ( `' I ` ( ( LSpan ` U ) ` { v } ) ) e. A )
17 14 16 sylan2b 
 |-  ( ( ( K e. HL /\ W e. H ) /\ v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) ) -> ( `' I ` ( ( LSpan ` U ) ` { v } ) ) e. A )
18 fveq2 
 |-  ( Q = ( ( LSpan ` U ) ` { v } ) -> ( `' I ` Q ) = ( `' I ` ( ( LSpan ` U ) ` { v } ) ) )
19 18 eleq1d 
 |-  ( Q = ( ( LSpan ` U ) ` { v } ) -> ( ( `' I ` Q ) e. A <-> ( `' I ` ( ( LSpan ` U ) ` { v } ) ) e. A ) )
20 17 19 syl5ibrcom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) ) -> ( Q = ( ( LSpan ` U ) ` { v } ) -> ( `' I ` Q ) e. A ) )
21 20 rexlimdva 
 |-  ( ( K e. HL /\ W e. H ) -> ( E. v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) Q = ( ( LSpan ` U ) ` { v } ) -> ( `' I ` Q ) e. A ) )
22 21 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. L ) -> ( E. v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) Q = ( ( LSpan ` U ) ` { v } ) -> ( `' I ` Q ) e. A ) )
23 13 22 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. L ) -> ( `' I ` Q ) e. A )