Theorem signswbase

Description: The base of W is the unordered triple reprensenting the possible signs. (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypotheses	signsw.p	|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
	signsw.w	|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
Assertion	signswbase	|- { -u 1 , 0 , 1 } = ( Base ` W )

Proof

Step	Hyp	Ref	Expression
1		signsw.p	|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
2		signsw.w	|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
3		tpex	|- { -u 1 , 0 , 1 } e. _V
4	2	grpbase	|- ( { -u 1 , 0 , 1 } e. _V -> { -u 1 , 0 , 1 } = ( Base ` W ) )
5	3 4	ax-mp	|- { -u 1 , 0 , 1 } = ( Base ` W )