Theorem signsw0g

Description: The neutral element of W . (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	signsw0g	|- 0 = ( 0g ` 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		c0ex	|- 0 e. _V
4	3	tpid2	|- 0 e. { -u 1 , 0 , 1 }
5	1	signsw0glem	|- A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u )
6	4 5	pm3.2i	|- ( 0 e. { -u 1 , 0 , 1 } /\ A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u ) )
7	1 2	signswbase	|- { -u 1 , 0 , 1 } = ( Base ` W )
8		eqid	|- ( 0g ` W ) = ( 0g ` W )
9	1 2	signswplusg	|- .+^ = ( +g ` W )
10		oveq1	|- ( e = 0 -> ( e .+^ u ) = ( 0 .+^ u ) )
11	10	eqeq1d	|- ( e = 0 -> ( ( e .+^ u ) = u <-> ( 0 .+^ u ) = u ) )
12	11	ovanraleqv	|- ( e = 0 -> ( A. u e. { -u 1 , 0 , 1 } ( ( e .+^ u ) = u /\ ( u .+^ e ) = u ) <-> A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u ) ) )
13	12	rspcev	|- ( ( 0 e. { -u 1 , 0 , 1 } /\ A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u ) ) -> E. e e. { -u 1 , 0 , 1 } A. u e. { -u 1 , 0 , 1 } ( ( e .+^ u ) = u /\ ( u .+^ e ) = u ) )
14	4 5 13	mp2an	|- E. e e. { -u 1 , 0 , 1 } A. u e. { -u 1 , 0 , 1 } ( ( e .+^ u ) = u /\ ( u .+^ e ) = u )
15	14	a1i	|- ( T. -> E. e e. { -u 1 , 0 , 1 } A. u e. { -u 1 , 0 , 1 } ( ( e .+^ u ) = u /\ ( u .+^ e ) = u ) )
16	7 8 9 15	ismgmid	|- ( T. -> ( ( 0 e. { -u 1 , 0 , 1 } /\ A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u ) ) <-> ( 0g ` W ) = 0 ) )
17	16	mptru	|- ( ( 0 e. { -u 1 , 0 , 1 } /\ A. u e. { -u 1 , 0 , 1 } ( ( 0 .+^ u ) = u /\ ( u .+^ 0 ) = u ) ) <-> ( 0g ` W ) = 0 )
18	6 17	mpbi	|- ( 0g ` W ) = 0
19	18	eqcomi	|- 0 = ( 0g ` W )