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

Theorem dihlspsnssN 32144
 Description: A subspace included in a 1-dim subspace belongs to the range of isomorphism H. (Contributed by NM, 26-Apr-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dih1dor0.h
dih1dor0.u
dihldor0.v
dih1dor0.s
dih1dor0.n
dih1dor0.i
Assertion
Ref Expression
dihlspsnssN

Proof of Theorem dihlspsnssN
StepHypRef Expression
1 simpr 447 . . . . 5
2 dih1dor0.h . . . . . . . 8
3 dih1dor0.u . . . . . . . 8
4 dihldor0.v . . . . . . . 8
5 dih1dor0.n . . . . . . . 8
6 dih1dor0.i . . . . . . . 8
72, 3, 4, 5, 6dihlsprn 32143 . . . . . . 7
873adant3 975 . . . . . 6
98ad2antrr 706 . . . . 5
101, 9eqeltrd 2370 . . . 4
11 simpr 447 . . . . . 6
12 simpll1 994 . . . . . . 7
13 eqid 2296 . . . . . . . 8
14 eqid 2296 . . . . . . . 8
1513, 2, 6, 3, 14dih0 32092 . . . . . . 7
1612, 15syl 15 . . . . . 6
1711, 16eqtr4d 2331 . . . . 5
18 eqid 2296 . . . . . . . 8
1918, 2, 6dihfn 32080 . . . . . . 7
2012, 19syl 15 . . . . . 6
21 simp1l 979 . . . . . . . 8
2221ad2antrr 706 . . . . . . 7
23 hlop 30174 . . . . . . 7
2418, 13op0cl 29996 . . . . . . 7
2522, 23, 243syl 18 . . . . . 6
26 fnfvelrn 5678 . . . . . 6
2720, 25, 26syl2anc 642 . . . . 5
2817, 27eqeltrd 2370 . . . 4
29 simpl1 958 . . . . . 6
302, 3, 29dvhlvec 31921 . . . . 5
31 simpr 447 . . . . 5
32 simpl2 959 . . . . 5
33 simpl3 960 . . . . 5
34 dih1dor0.s . . . . . 6
354, 14, 34, 5lspsnat 15914 . . . . 5
3630, 31, 32, 33, 35syl31anc 1185 . . . 4
3710, 28, 36mpjaodan 761 . . 3
3837ex 423 . 2
392, 3, 6, 34dihsslss 32088 . . . 4