Theorem hdmapip0com

Description: Commutation property of Baer's sigma map (Holland's A map). Line 20 of Holland95 p. 14. Also part of Lemma 1 of Baer p. 110 line 7. (Contributed by NM, 9-Jun-2015)

	Ref	Expression
Hypotheses	hdmapip0com.h	|- H = ( LHyp ` K )
	hdmapip0com.u	|- U = ( ( DVecH ` K ) ` W )
	hdmapip0com.v	|- V = ( Base ` U )
	hdmapip0com.r	|- R = ( Scalar ` U )
	hdmapip0com.z	|- .0. = ( 0g ` R )
	hdmapip0com.s	|- S = ( ( HDMap ` K ) ` W )
	hdmapip0com.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmapip0com.x	|- ( ph -> X e. V )
	hdmapip0com.y	|- ( ph -> Y e. V )
Assertion	hdmapip0com	|- ( ph -> ( ( ( S ` X ) ` Y ) = .0. <-> ( ( S ` Y ) ` X ) = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapip0com.h	|- H = ( LHyp ` K )
2		hdmapip0com.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmapip0com.v	|- V = ( Base ` U )
4		hdmapip0com.r	|- R = ( Scalar ` U )
5		hdmapip0com.z	|- .0. = ( 0g ` R )
6		hdmapip0com.s	|- S = ( ( HDMap ` K ) ` W )
7		hdmapip0com.k	|- ( ph -> ( K e. HL /\ W e. H ) )
8		hdmapip0com.x	|- ( ph -> X e. V )
9		hdmapip0com.y	|- ( ph -> Y e. V )
10		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
11	1 10 2 3 7 9 8	dochsncom	|- ( ph -> ( Y e. ( ( ( ocH ` K ) ` W ) ` { X } ) <-> X e. ( ( ( ocH ` K ) ` W ) ` { Y } ) ) )
12	1 10 2 3 4 5 6 7 8 9	hdmapellkr	|- ( ph -> ( ( ( S ` X ) ` Y ) = .0. <-> Y e. ( ( ( ocH ` K ) ` W ) ` { X } ) ) )
13	1 10 2 3 4 5 6 7 9 8	hdmapellkr	|- ( ph -> ( ( ( S ` Y ) ` X ) = .0. <-> X e. ( ( ( ocH ` K ) ` W ) ` { Y } ) ) )
14	11 12 13	3bitr4d	|- ( ph -> ( ( ( S ` X ) ` Y ) = .0. <-> ( ( S ` Y ) ` X ) = .0. ) )