Theorem signsw0glem

Description: Neutral element property of .+^ . (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypothesis	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)$$
Assertion	signsw0glem	$$⊢\forall u\in \left\{-1,0,1\right\}\left(0\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}0=u\right)$$

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		c0ex	$$⊢0\in \mathrm{V}$$
3	2	tpid2	$$⊢0\in \left\{-1,0,1\right\}$$
4	1	signspval	$$⊢\left(0\in \left\{-1,0,1\right\}\wedge u\in \left\{-1,0,1\right\}\right)\to 0\underset{\dot{}}{⨣}u=if\left(u=0,0,u\right)$$
5	3 4	mpan	$$⊢u\in \left\{-1,0,1\right\}\to 0\underset{\dot{}}{⨣}u=if\left(u=0,0,u\right)$$
6		iftrue	$$⊢u=0\to if\left(u=0,0,u\right)=0$$
7		id	$$⊢u=0\to u=0$$
8	6 7	eqtr4d	$$⊢u=0\to if\left(u=0,0,u\right)=u$$
9		iffalse	$$⊢\neg u=0\to if\left(u=0,0,u\right)=u$$
10	8 9	pm2.61i	$$⊢if\left(u=0,0,u\right)=u$$
11	5 10	eqtrdi	$$⊢u\in \left\{-1,0,1\right\}\to 0\underset{\dot{}}{⨣}u=u$$
12	1	signspval	$$⊢\left(u\in \left\{-1,0,1\right\}\wedge 0\in \left\{-1,0,1\right\}\right)\to u\underset{\dot{}}{⨣}0=if\left(0=0,u,0\right)$$
13	3 12	mpan2	$$⊢u\in \left\{-1,0,1\right\}\to u\underset{\dot{}}{⨣}0=if\left(0=0,u,0\right)$$
14		eqid	$$⊢0=0$$
15	14	iftruei	$$⊢if\left(0=0,u,0\right)=u$$
16	13 15	eqtrdi	$$⊢u\in \left\{-1,0,1\right\}\to u\underset{\dot{}}{⨣}0=u$$
17	11 16	jca	$$⊢u\in \left\{-1,0,1\right\}\to \left(0\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}0=u\right)$$
18	17	rgen	$$⊢\forall u\in \left\{-1,0,1\right\}\left(0\underset{\dot{}}{⨣}u=u\wedge u\underset{\dot{}}{⨣}0=u\right)$$