Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihlatat Structured version   Unicode version

Theorem dihlatat 32197
 Description: The reverse isomorphism H of a 1-dim subspace is an atom. (Contributed by NM, 28-Apr-2014.)
Hypotheses
Ref Expression
dihlatat.a
dihlatat.h
dihlatat.u
dihlatat.i
dihlatat.l LSAtoms
Assertion
Ref Expression
dihlatat

Proof of Theorem dihlatat
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dihlatat.h . . . . 5
2 dihlatat.u . . . . 5
3 id 21 . . . . 5
41, 2, 3dvhlvec 31969 . . . 4
5 eqid 2438 . . . . 5
6 eqid 2438 . . . . 5
7 eqid 2438 . . . . 5
8 dihlatat.l . . . . 5 LSAtoms
95, 6, 7, 8islsat 29851 . . . 4
104, 9syl 16 . . 3
1110biimpa 472 . 2
12 eldifsn 3929 . . . . . 6
13 dihlatat.a . . . . . . . 8
14 dihlatat.i . . . . . . . 8
1513, 1, 2, 5, 7, 6, 14dihlspsnat 32193 . . . . . . 7
16153expb 1155 . . . . . 6
1712, 16sylan2b 463 . . . . 5
18 fveq2 5730 . . . . . 6
1918eleq1d 2504 . . . . 5
2017, 19syl5ibrcom 215 . . . 4
2120rexlimdva 2832 . . 3