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

Theorem omlspjN 35087
 Description: Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
omlspj.b
omlspj.l
omlspj.j
omlspj.m
omlspj.o
Assertion
Ref Expression
omlspjN

Proof of Theorem omlspjN
StepHypRef Expression
1 omllat 35068 . . . . . 6
213ad2ant1 1017 . . . . 5
3 omlop 35067 . . . . . . 7
433ad2ant1 1017 . . . . . 6
5 simp2r 1023 . . . . . 6
6 omlspj.b . . . . . . 7
7 omlspj.o . . . . . . 7
86, 7opoccl 35020 . . . . . 6
94, 5, 8syl2anc 661 . . . . 5
10 omlspj.m . . . . . 6
116, 10latmcom 15831 . . . . 5
122, 9, 5, 11syl3anc 1228 . . . 4
13 eqid 2457 . . . . . 6
146, 7, 10, 13opnoncon 35034 . . . . 5
154, 5, 14syl2anc 661 . . . 4
1612, 15eqtrd 2498 . . 3
1716oveq2d 6312 . 2
18 simp1 996 . . 3
19 simp2l 1022 . . 3
20 simp3 998 . . 3
21 eqid 2457 . . . . . 6
226, 21cmtidN 35083 . . . . 5
2318, 5, 22syl2anc 661 . . . 4
246, 7, 21cmt3N 35077 . . . . 5
2518, 5, 5, 24syl3anc 1228 . . . 4
2623, 25mpbid 210 . . 3
27 omlspj.l . . . 4
28 omlspj.j . . . 4
296, 27, 28, 10, 21omlmod1i2N 35086 . . 3
3018, 19, 9, 5, 20, 26, 29syl132anc 1246 . 2
31 omlol 35066 . . . 4