signstf0

Description: Sign of a single letter word. (Contributed by Thierry Arnoux, 8-Oct-2018)

	Ref	Expression
Hypotheses	signsv.p	$⊢ \underset{˙}{⨣} = (a \in \{- 1, 0, 1\}, b \in \{- 1, 0, 1\} ⟼ if (b = 0, a, b))$
	signsv.w	$⊢ W = \{⟨{Base}_{ndx}, \{- 1, 0, 1\}⟩, ⟨+_{ndx}, \underset{˙}{⨣}⟩\}$
	signsv.t	$⊢ T = (f \in Word ℝ ⟼ (n \in (0 ..^\|f\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (f (i))))$
	signsv.v	$⊢ V = (f \in Word ℝ ⟼ \sum_{j \in (1 ..^\|f\|)} if (T (f) (j) \neq T (f) (j - 1), 1, 0))$
Assertion	signstf0	$⊢ K \in ℝ \to T (⟨“ K ”⟩) = ⟨“ sgn (K) ”⟩$

Proof

Step	Hyp	Ref	Expression
1		signsv.p	$⊢ \underset{˙}{⨣} = (a \in \{- 1, 0, 1\}, b \in \{- 1, 0, 1\} ⟼ if (b = 0, a, b))$
2		signsv.w	$⊢ W = \{⟨{Base}_{ndx}, \{- 1, 0, 1\}⟩, ⟨+_{ndx}, \underset{˙}{⨣}⟩\}$
3		signsv.t	$⊢ T = (f \in Word ℝ ⟼ (n \in (0 ..^\|f\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (f (i))))$
4		signsv.v	$⊢ V = (f \in Word ℝ ⟼ \sum_{j \in (1 ..^\|f\|)} if (T (f) (j) \neq T (f) (j - 1), 1, 0))$
5		s1len	$⊢ \|⟨“ K ”⟩\| = 1$
6	5	oveq2i	$⊢ (0 ..^\|⟨“ K ”⟩\|) = (0 ..^1)$
7		fzo01	$⊢ (0 ..^1) = \{0\}$
8	6 7	eqtri	$⊢ (0 ..^\|⟨“ K ”⟩\|) = \{0\}$
9	8	a1i	$⊢ K \in ℝ \to (0 ..^\|⟨“ K ”⟩\|) = \{0\}$
10		simpr	$⊢ (K \in ℝ \land n \in (0 ..^\|⟨“ K ”⟩\|)) \to n \in (0 ..^\|⟨“ K ”⟩\|)$
11	10 8	eleqtrdi	$⊢ (K \in ℝ \land n \in (0 ..^\|⟨“ K ”⟩\|)) \to n \in \{0\}$
12		velsn	$⊢ n \in \{0\} \leftrightarrow n = 0$
13	11 12	sylib	$⊢ (K \in ℝ \land n \in (0 ..^\|⟨“ K ”⟩\|)) \to n = 0$
14		oveq2	$⊢ n = 0 \to (0 \dots n) = (0 \dots 0)$
15		0z	$⊢ 0 \in ℤ$
16		fzsn	$⊢ 0 \in ℤ \to (0 \dots 0) = \{0\}$
17	15 16	ax-mp	$⊢ (0 \dots 0) = \{0\}$
18	14 17	eqtrdi	$⊢ n = 0 \to (0 \dots n) = \{0\}$
19	18	mpteq1d	$⊢ n = 0 \to (i \in (0 \dots n) ⟼ sgn (⟨“ K ”⟩ (i))) = (i \in \{0\} ⟼ sgn (⟨“ K ”⟩ (i)))$
20	19	oveq2d	$⊢ n = 0 \to {\sum_{W}}_{i = 0}^{n} sgn (⟨“ K ”⟩ (i)) = \underset{i \in \{0\}}{\sum_{W}} sgn (⟨“ K ”⟩ (i))$
21	20	adantl	$⊢ (K \in ℝ \land n = 0) \to {\sum_{W}}_{i = 0}^{n} sgn (⟨“ K ”⟩ (i)) = \underset{i \in \{0\}}{\sum_{W}} sgn (⟨“ K ”⟩ (i))$
22	1 2	signswmnd	$⊢ W \in Mnd$
23	22	a1i	$⊢ K \in ℝ \to W \in Mnd$
24		0re	$⊢ 0 \in ℝ$
25	24	a1i	$⊢ K \in ℝ \to 0 \in ℝ$
26		s1fv	$⊢ K \in ℝ \to ⟨“ K ”⟩ (0) = K$
27		id	$⊢ K \in ℝ \to K \in ℝ$
28	26 27	eqeltrd	$⊢ K \in ℝ \to ⟨“ K ”⟩ (0) \in ℝ$
29	28	rexrd	$⊢ K \in ℝ \to ⟨“ K ”⟩ (0) \in ℝ^{*}$
30		sgncl	$⊢ ⟨“ K ”⟩ (0) \in ℝ^{*} \to sgn (⟨“ K ”⟩ (0)) \in \{- 1, 0, 1\}$
31	29 30	syl	$⊢ K \in ℝ \to sgn (⟨“ K ”⟩ (0)) \in \{- 1, 0, 1\}$
32	1 2	signswbase	$⊢ \{- 1, 0, 1\} = {Base}_{W}$
33		2fveq3	$⊢ i = 0 \to sgn (⟨“ K ”⟩ (i)) = sgn (⟨“ K ”⟩ (0))$
34	32 33	gsumsn	$⊢ (W \in Mnd \land 0 \in ℝ \land sgn (⟨“ K ”⟩ (0)) \in \{- 1, 0, 1\}) \to \underset{i \in \{0\}}{\sum_{W}} sgn (⟨“ K ”⟩ (i)) = sgn (⟨“ K ”⟩ (0))$
35	23 25 31 34	syl3anc	$⊢ K \in ℝ \to \underset{i \in \{0\}}{\sum_{W}} sgn (⟨“ K ”⟩ (i)) = sgn (⟨“ K ”⟩ (0))$
36	35	adantr	$⊢ (K \in ℝ \land n = 0) \to \underset{i \in \{0\}}{\sum_{W}} sgn (⟨“ K ”⟩ (i)) = sgn (⟨“ K ”⟩ (0))$
37	26	fveq2d	$⊢ K \in ℝ \to sgn (⟨“ K ”⟩ (0)) = sgn (K)$
38	37	adantr	$⊢ (K \in ℝ \land n = 0) \to sgn (⟨“ K ”⟩ (0)) = sgn (K)$
39	21 36 38	3eqtrd	$⊢ (K \in ℝ \land n = 0) \to {\sum_{W}}_{i = 0}^{n} sgn (⟨“ K ”⟩ (i)) = sgn (K)$
40	13 39	syldan	$⊢ (K \in ℝ \land n \in (0 ..^\|⟨“ K ”⟩\|)) \to {\sum_{W}}_{i = 0}^{n} sgn (⟨“ K ”⟩ (i)) = sgn (K)$
41	9 40	mpteq12dva	$⊢ K \in ℝ \to (n \in (0 ..^\|⟨“ K ”⟩\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (⟨“ K ”⟩ (i))) = (n \in \{0\} ⟼ sgn (K))$
42		s1cl	$⊢ K \in ℝ \to ⟨“ K ”⟩ \in Word ℝ$
43	1 2 3 4	signstfv	$⊢ ⟨“ K ”⟩ \in Word ℝ \to T (⟨“ K ”⟩) = (n \in (0 ..^\|⟨“ K ”⟩\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (⟨“ K ”⟩ (i)))$
44	42 43	syl	$⊢ K \in ℝ \to T (⟨“ K ”⟩) = (n \in (0 ..^\|⟨“ K ”⟩\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (⟨“ K ”⟩ (i)))$
45		sgnclre	$⊢ K \in ℝ \to sgn (K) \in ℝ$
46		s1val	$⊢ sgn (K) \in ℝ \to ⟨“ sgn (K) ”⟩ = \{⟨0, sgn (K)⟩\}$
47	45 46	syl	$⊢ K \in ℝ \to ⟨“ sgn (K) ”⟩ = \{⟨0, sgn (K)⟩\}$
48		fmptsn	$⊢ (0 \in ℝ \land sgn (K) \in ℝ) \to \{⟨0, sgn (K)⟩\} = (n \in \{0\} ⟼ sgn (K))$
49	24 45 48	sylancr	$⊢ K \in ℝ \to \{⟨0, sgn (K)⟩\} = (n \in \{0\} ⟼ sgn (K))$
50	47 49	eqtrd	$⊢ K \in ℝ \to ⟨“ sgn (K) ”⟩ = (n \in \{0\} ⟼ sgn (K))$
51	41 44 50	3eqtr4d	$⊢ K \in ℝ \to T (⟨“ K ”⟩) = ⟨“ sgn (K) ”⟩$

Metamath Proof Explorer

Theorem signstf0

Proof