Theorem signsw0g

Description: The neutral element of W . (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypotheses	signsw.p	$$⊢\underset{\dot{}}{⨣}=\left(a\in \left\{-1,0,1\right\},b\in \left\{-1,0,1\right\}⟼if\left(b=0,a,b\right)\right)$$
	signsw.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{-1,0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
Assertion	signsw0g	$$⊢0=0_W$$

Proof

Step	Hyp	Ref	Expression
1		signsw.p	$$⊢\underset{\dot{}}{⨣}=\left(a\in \left\{-1,0,1\right\},b\in \left\{-1,0,1\right\}⟼if\left(b=0,a,b\right)\right)$$
2		signsw.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{-1,0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
3		c0ex	$$⊢0\in \mathrm{V}$$
4	3	tpid2	$$⊢0\in \left\{-1,0,1\right\}$$
5	1	signsw0glem	$$⊢\forall u\in \left\{-1,0,1\right\}\left(0\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}0=u\right)$$
6	4 5	pm3.2i	$$⊢\left(0\in \left\{-1,0,1\right\}\wedge \forall u\in \left\{-1,0,1\right\}\left(0\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}0=u\right)\right)$$
7	1 2	signswbase	$$⊢\left\{-1,0,1\right\}={\mathrm{Base}}_W$$
8		eqid	$$⊢0_W=0_W$$
9	1 2	signswplusg	$$⊢\underset{\dot{}}{⨣}={+}_W$$
10		oveq1	$$⊢e=0\to e\underset{\dot{}}{⨣}u=0\underset{\dot{}}{⨣}u$$
11	10	eqeq1d	$$⊢e=0\to \left(e\underset{\dot{}}{⨣}u=u\leftrightarrow 0\underset{\dot{}}{⨣}u=u\right)$$
12	11	ovanraleqv	$$⊢e=0\to \left(\forall u\in \left\{-1,0,1\right\}\left(e\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}e=u\right)\leftrightarrow \forall u\in \left\{-1,0,1\right\}\left(0\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}0=u\right)\right)$$
13	12	rspcev	$$⊢\left(0\in \left\{-1,0,1\right\}\wedge \forall u\in \left\{-1,0,1\right\}\left(0\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}0=u\right)\right)\to \exists e\in \left\{-1,0,1\right\}\forall u\in \left\{-1,0,1\right\}\left(e\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}e=u\right)$$
14	4 5 13	mp2an	$$⊢\exists e\in \left\{-1,0,1\right\}\forall u\in \left\{-1,0,1\right\}\left(e\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}e=u\right)$$
15	14	a1i	$$⊢\top \to \exists e\in \left\{-1,0,1\right\}\forall u\in \left\{-1,0,1\right\}\left(e\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}e=u\right)$$
16	7 8 9 15	ismgmid	$$⊢\top \to \left(\left(0\in \left\{-1,0,1\right\}\wedge \forall u\in \left\{-1,0,1\right\}\left(0\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}0=u\right)\right)\leftrightarrow 0_W=0\right)$$
17	16	mptru	$$⊢\left(0\in \left\{-1,0,1\right\}\wedge \forall u\in \left\{-1,0,1\right\}\left(0\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}0=u\right)\right)\leftrightarrow 0_W=0$$
18	6 17	mpbi	$$⊢0_W=0$$
19	18	eqcomi	$$⊢0=0_W$$