Theorem riotaocN

Description: The orthocomplement of the unique poset element such that ps . ( riotaneg analog.) (Contributed by NM, 16-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	riotaoc.b	|- B = ( Base ` K )
	riotaoc.o	|- ._|_ = ( oc ` K )
	riotaoc.a	|- ( x = ( ._|_ ` y ) -> ( ph <-> ps ) )
Assertion	riotaocN	|- ( ( K e. OP /\ E! x e. B ph ) -> ( iota_ x e. B ph ) = ( ._|_ ` ( iota_ y e. B ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		riotaoc.b	|- B = ( Base ` K )
2		riotaoc.o	|- ._|_ = ( oc ` K )
3		riotaoc.a	|- ( x = ( ._|_ ` y ) -> ( ph <-> ps ) )
4		nfcv	|- F/_ y ._|_
5		nfriota1	|- F/_ y ( iota_ y e. B ps )
6	4 5	nffv	|- F/_ y ( ._|_ ` ( iota_ y e. B ps ) )
7	1 2	opoccl	|- ( ( K e. OP /\ y e. B ) -> ( ._|_ ` y ) e. B )
8	1 2	opoccl	|- ( ( K e. OP /\ ( iota_ y e. B ps ) e. B ) -> ( ._|_ ` ( iota_ y e. B ps ) ) e. B )
9		fveq2	|- ( y = ( iota_ y e. B ps ) -> ( ._|_ ` y ) = ( ._|_ ` ( iota_ y e. B ps ) ) )
10	1 2	opoccl	|- ( ( K e. OP /\ x e. B ) -> ( ._|_ ` x ) e. B )
11	1 2	opcon2b	|- ( ( K e. OP /\ x e. B /\ y e. B ) -> ( x = ( ._|_ ` y ) <-> y = ( ._|_ ` x ) ) )
12	10 11	reuhypd	|- ( ( K e. OP /\ x e. B ) -> E! y e. B x = ( ._|_ ` y ) )
13	6 7 8 3 9 12	riotaxfrd	|- ( ( K e. OP /\ E! x e. B ph ) -> ( iota_ x e. B ph ) = ( ._|_ ` ( iota_ y e. B ps ) ) )