Theorem signswplusg

Description: The operation 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	signswplusg	$$⊢\underset{\dot{}}{⨣}={+}_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		tpex	$$⊢\left\{-1,0,1\right\}\in \mathrm{V}$$
4	3 3	mpoex	$$⊢\left(a\in \left\{-1,0,1\right\},b\in \left\{-1,0,1\right\}⟼if\left(b=0,a,b\right)\right)\in \mathrm{V}$$
5	1 4	eqeltri	$$⊢\underset{\dot{}}{⨣}\in \mathrm{V}$$
6	2	grpplusg	$$⊢\underset{\dot{}}{⨣}\in \mathrm{V}\to \underset{\dot{}}{⨣}={+}_W$$
7	5 6	ax-mp	$$⊢\underset{\dot{}}{⨣}={+}_W$$