hdmapg

Description: Apply the scalar sigma function (involution) G to an inner product reverses the arguments. The inner product of X and Y is represented by ( ( SY )X ) . Line 15 in Baer p. 111, f(x,y) alpha = f(y,x). (Contributed by NM, 14-Jun-2015)

	Ref	Expression
Hypotheses	hdmapg.h	\|- H = ( LHyp ` K )
	hdmapg.u	\|- U = ( ( DVecH ` K ) ` W )
	hdmapg.v	\|- V = ( Base ` U )
	hdmapg.s	\|- S = ( ( HDMap ` K ) ` W )
	hdmapg.g	\|- G = ( ( HGMap ` K ) ` W )
	hdmapg.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmapg.x	\|- ( ph -> X e. V )
	hdmapg.y	\|- ( ph -> Y e. V )
Assertion	hdmapg	\|- ( ph -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapg.h	\|- H = ( LHyp ` K )
2		hdmapg.u	\|- U = ( ( DVecH ` K ) ` W )
3		hdmapg.v	\|- V = ( Base ` U )
4		hdmapg.s	\|- S = ( ( HDMap ` K ) ` W )
5		hdmapg.g	\|- G = ( ( HGMap ` K ) ` W )
6		hdmapg.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
7		hdmapg.x	\|- ( ph -> X e. V )
8		hdmapg.y	\|- ( ph -> Y e. V )
9		eqid	\|- <. ( _I \|` ( Base ` K ) ) , ( _I \|` ( ( LTrn ` K ) ` W ) ) >. = <. ( _I \|` ( Base ` K ) ) , ( _I \|` ( ( LTrn ` K ) ` W ) ) >.
10		eqid	\|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
11		eqid	\|- ( +g ` U ) = ( +g ` U )
12		eqid	\|- ( .s ` U ) = ( .s ` U )
13		eqid	\|- ( Scalar ` U ) = ( Scalar ` U )
14		eqid	\|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
15		eqid	\|- ( LSSum ` U ) = ( LSSum ` U )
16		eqid	\|- ( LSpan ` U ) = ( LSpan ` U )
17		eqid	\|- ( .r ` ( Scalar ` U ) ) = ( .r ` ( Scalar ` U ) )
18		eqid	\|- ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )
19		eqid	\|- ( +g ` ( Scalar ` U ) ) = ( +g ` ( Scalar ` U ) )
20	1 9 10 2 3 11 12 13 14 15 16 6 7 17 18 19 4 5 8	hdmapglem7	\|- ( ph -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) )

Metamath Proof Explorer

Theorem hdmapg

Proof