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	$$⊢\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	signswbase	$$⊢\left\{-1,0,1\right\}={\mathrm{Base}}_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	2	grpbase	$$⊢\left\{-1,0,1\right\}\in \mathrm{V}\to \left\{-1,0,1\right\}={\mathrm{Base}}_W$$
5	3 4	ax-mp	$$⊢\left\{-1,0,1\right\}={\mathrm{Base}}_W$$