ccatsymb

Description: The symbol at a given position in a concatenated word. (Contributed by AV, 26-May-2018) (Proof shortened by AV, 24-Nov-2018)

		Ref	Expression
	Assertion	ccatsymb	$⊢ (A \in Word V \land B \in Word V \land I \in ℤ) \to (A ++ B) (I) = if (I < \|A\|, A (I), B (I - \|A\|))$

Proof

Step	Hyp	Ref	Expression
1		simprll	$⊢ (0 \leq I \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < \|A\|)) \to (A \in Word V \land B \in Word V)$
2		simpr	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < \|A\|) \to I < \|A\|$
3	2	anim2i	$⊢ (0 \leq I \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < \|A\|)) \to (0 \leq I \land I < \|A\|)$
4		simpr	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to I \in ℤ$
5		0zd	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to 0 \in ℤ$
6		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
7	6	nn0zd	$⊢ A \in Word V \to \|A\| \in ℤ$
8	7	ad2antrr	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to \|A\| \in ℤ$
9		elfzo	$⊢ (I \in ℤ \land 0 \in ℤ \land \|A\| \in ℤ) \to (I \in (0 ..^\|A\|) \leftrightarrow (0 \leq I \land I < \|A\|))$
10	4 5 8 9	syl3anc	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (I \in (0 ..^\|A\|) \leftrightarrow (0 \leq I \land I < \|A\|))$
11	10	ad2antrl	$⊢ (0 \leq I \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < \|A\|)) \to (I \in (0 ..^\|A\|) \leftrightarrow (0 \leq I \land I < \|A\|))$
12	3 11	mpbird	$⊢ (0 \leq I \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < \|A\|)) \to I \in (0 ..^\|A\|)$
13		df-3an	$⊢ (A \in Word V \land B \in Word V \land I \in (0 ..^\|A\|)) \leftrightarrow ((A \in Word V \land B \in Word V) \land I \in (0 ..^\|A\|))$
14	1 12 13	sylanbrc	$⊢ (0 \leq I \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < \|A\|)) \to (A \in Word V \land B \in Word V \land I \in (0 ..^\|A\|))$
15		ccatval1	$⊢ (A \in Word V \land B \in Word V \land I \in (0 ..^\|A\|)) \to (A ++ B) (I) = A (I)$
16	15	eqcomd	$⊢ (A \in Word V \land B \in Word V \land I \in (0 ..^\|A\|)) \to A (I) = (A ++ B) (I)$
17	14 16	syl	$⊢ (0 \leq I \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < \|A\|)) \to A (I) = (A ++ B) (I)$
18	17	ex	$⊢ 0 \leq I \to ((((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < \|A\|) \to A (I) = (A ++ B) (I))$
19		zre	$⊢ I \in ℤ \to I \in ℝ$
20		0red	$⊢ I \in ℤ \to 0 \in ℝ$
21	19 20	ltnled	$⊢ I \in ℤ \to (I < 0 \leftrightarrow \neg 0 \leq I)$
22	21	adantl	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (I < 0 \leftrightarrow \neg 0 \leq I)$
23		simpl	$⊢ (A \in Word V \land B \in Word V) \to A \in Word V$
24	23	anim1i	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (A \in Word V \land I \in ℤ)$
25	24	adantr	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < 0) \to (A \in Word V \land I \in ℤ)$
26		animorrl	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < 0) \to (I < 0 \lor \|A\| \leq I)$
27		wrdsymb0	$⊢ (A \in Word V \land I \in ℤ) \to ((I < 0 \lor \|A\| \leq I) \to A (I) = \emptyset)$
28	25 26 27	sylc	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < 0) \to A (I) = \emptyset$
29		ccatcl	$⊢ (A \in Word V \land B \in Word V) \to A ++ B \in Word V$
30	29	anim1i	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (A ++ B \in Word V \land I \in ℤ)$
31	30	adantr	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < 0) \to (A ++ B \in Word V \land I \in ℤ)$
32		animorrl	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < 0) \to (I < 0 \lor \|A ++ B\| \leq I)$
33		wrdsymb0	$⊢ (A ++ B \in Word V \land I \in ℤ) \to ((I < 0 \lor \|A ++ B\| \leq I) \to (A ++ B) (I) = \emptyset)$
34	31 32 33	sylc	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < 0) \to (A ++ B) (I) = \emptyset$
35	28 34	eqtr4d	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < 0) \to A (I) = (A ++ B) (I)$
36	35	ex	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (I < 0 \to A (I) = (A ++ B) (I))$
37	22 36	sylbird	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (\neg 0 \leq I \to A (I) = (A ++ B) (I))$
38	37	com12	$⊢ \neg 0 \leq I \to (((A \in Word V \land B \in Word V) \land I \in ℤ) \to A (I) = (A ++ B) (I))$
39	38	adantrd	$⊢ \neg 0 \leq I \to ((((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < \|A\|) \to A (I) = (A ++ B) (I))$
40	18 39	pm2.61i	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land I < \|A\|) \to A (I) = (A ++ B) (I)$
41		simprll	$⊢ (I < \|A\| + \|B\| \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \neg I < \|A\|)) \to (A \in Word V \land B \in Word V)$
42		id	$⊢ I < \|A\| + \|B\| \to I < \|A\| + \|B\|$
43	6	nn0red	$⊢ A \in Word V \to \|A\| \in ℝ$
44		lenlt	$⊢ (\|A\| \in ℝ \land I \in ℝ) \to (\|A\| \leq I \leftrightarrow \neg I < \|A\|)$
45	43 19 44	syl2an	$⊢ (A \in Word V \land I \in ℤ) \to (\|A\| \leq I \leftrightarrow \neg I < \|A\|)$
46	45	adantlr	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (\|A\| \leq I \leftrightarrow \neg I < \|A\|)$
47	46	biimpar	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \neg I < \|A\|) \to \|A\| \leq I$
48	42 47	anim12ci	$⊢ (I < \|A\| + \|B\| \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \neg I < \|A\|)) \to (\|A\| \leq I \land I < \|A\| + \|B\|)$
49		lencl	$⊢ B \in Word V \to \|B\| \in ℕ_{0}$
50	49	nn0zd	$⊢ B \in Word V \to \|B\| \in ℤ$
51		zaddcl	$⊢ (\|A\| \in ℤ \land \|B\| \in ℤ) \to \|A\| + \|B\| \in ℤ$
52	7 50 51	syl2an	$⊢ (A \in Word V \land B \in Word V) \to \|A\| + \|B\| \in ℤ$
53	52	adantr	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to \|A\| + \|B\| \in ℤ$
54		elfzo	$⊢ (I \in ℤ \land \|A\| \in ℤ \land \|A\| + \|B\| \in ℤ) \to (I \in (\|A\| ..^\|A\| + \|B\|) \leftrightarrow (\|A\| \leq I \land I < \|A\| + \|B\|))$
55	4 8 53 54	syl3anc	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (I \in (\|A\| ..^\|A\| + \|B\|) \leftrightarrow (\|A\| \leq I \land I < \|A\| + \|B\|))$
56	55	ad2antrl	$⊢ (I < \|A\| + \|B\| \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \neg I < \|A\|)) \to (I \in (\|A\| ..^\|A\| + \|B\|) \leftrightarrow (\|A\| \leq I \land I < \|A\| + \|B\|))$
57	48 56	mpbird	$⊢ (I < \|A\| + \|B\| \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \neg I < \|A\|)) \to I \in (\|A\| ..^\|A\| + \|B\|)$
58		df-3an	$⊢ (A \in Word V \land B \in Word V \land I \in (\|A\| ..^\|A\| + \|B\|)) \leftrightarrow ((A \in Word V \land B \in Word V) \land I \in (\|A\| ..^\|A\| + \|B\|))$
59	41 57 58	sylanbrc	$⊢ (I < \|A\| + \|B\| \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \neg I < \|A\|)) \to (A \in Word V \land B \in Word V \land I \in (\|A\| ..^\|A\| + \|B\|))$
60		ccatval2	$⊢ (A \in Word V \land B \in Word V \land I \in (\|A\| ..^\|A\| + \|B\|)) \to (A ++ B) (I) = B (I - \|A\|)$
61	60	eqcomd	$⊢ (A \in Word V \land B \in Word V \land I \in (\|A\| ..^\|A\| + \|B\|)) \to B (I - \|A\|) = (A ++ B) (I)$
62	59 61	syl	$⊢ (I < \|A\| + \|B\| \land (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \neg I < \|A\|)) \to B (I - \|A\|) = (A ++ B) (I)$
63	62	ex	$⊢ I < \|A\| + \|B\| \to ((((A \in Word V \land B \in Word V) \land I \in ℤ) \land \neg I < \|A\|) \to B (I - \|A\|) = (A ++ B) (I))$
64	49	nn0red	$⊢ B \in Word V \to \|B\| \in ℝ$
65		readdcl	$⊢ (\|A\| \in ℝ \land \|B\| \in ℝ) \to \|A\| + \|B\| \in ℝ$
66	43 64 65	syl2an	$⊢ (A \in Word V \land B \in Word V) \to \|A\| + \|B\| \in ℝ$
67		lenlt	$⊢ (\|A\| + \|B\| \in ℝ \land I \in ℝ) \to (\|A\| + \|B\| \leq I \leftrightarrow \neg I < \|A\| + \|B\|)$
68	66 19 67	syl2an	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (\|A\| + \|B\| \leq I \leftrightarrow \neg I < \|A\| + \|B\|)$
69		simplr	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to B \in Word V$
70		simpr	$⊢ (A \in Word V \land I \in ℤ) \to I \in ℤ$
71	7	adantr	$⊢ (A \in Word V \land I \in ℤ) \to \|A\| \in ℤ$
72	70 71	zsubcld	$⊢ (A \in Word V \land I \in ℤ) \to I - \|A\| \in ℤ$
73	72	adantlr	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to I - \|A\| \in ℤ$
74	69 73	jca	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (B \in Word V \land I - \|A\| \in ℤ)$
75	74	adantr	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to (B \in Word V \land I - \|A\| \in ℤ)$
76	43	ad2antrr	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to \|A\| \in ℝ$
77	64	ad2antlr	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to \|B\| \in ℝ$
78	19	adantl	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to I \in ℝ$
79	76 77 78	leaddsub2d	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (\|A\| + \|B\| \leq I \leftrightarrow \|B\| \leq I - \|A\|)$
80	79	biimpa	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to \|B\| \leq I - \|A\|$
81	80	olcd	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to (I - \|A\| < 0 \lor \|B\| \leq I - \|A\|)$
82		wrdsymb0	$⊢ (B \in Word V \land I - \|A\| \in ℤ) \to ((I - \|A\| < 0 \lor \|B\| \leq I - \|A\|) \to B (I - \|A\|) = \emptyset)$
83	75 81 82	sylc	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to B (I - \|A\|) = \emptyset$
84	30	adantr	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to (A ++ B \in Word V \land I \in ℤ)$
85		ccatlen	$⊢ (A \in Word V \land B \in Word V) \to \|A ++ B\| = \|A\| + \|B\|$
86	85	ad2antrr	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to \|A ++ B\| = \|A\| + \|B\|$
87		simpr	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to \|A\| + \|B\| \leq I$
88	86 87	eqbrtrd	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to \|A ++ B\| \leq I$
89	88	olcd	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to (I < 0 \lor \|A ++ B\| \leq I)$
90	84 89 33	sylc	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to (A ++ B) (I) = \emptyset$
91	83 90	eqtr4d	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \|A\| + \|B\| \leq I) \to B (I - \|A\|) = (A ++ B) (I)$
92	91	ex	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (\|A\| + \|B\| \leq I \to B (I - \|A\|) = (A ++ B) (I))$
93	68 92	sylbird	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (\neg I < \|A\| + \|B\| \to B (I - \|A\|) = (A ++ B) (I))$
94	93	com12	$⊢ \neg I < \|A\| + \|B\| \to (((A \in Word V \land B \in Word V) \land I \in ℤ) \to B (I - \|A\|) = (A ++ B) (I))$
95	94	adantrd	$⊢ \neg I < \|A\| + \|B\| \to ((((A \in Word V \land B \in Word V) \land I \in ℤ) \land \neg I < \|A\|) \to B (I - \|A\|) = (A ++ B) (I))$
96	63 95	pm2.61i	$⊢ (((A \in Word V \land B \in Word V) \land I \in ℤ) \land \neg I < \|A\|) \to B (I - \|A\|) = (A ++ B) (I)$
97	40 96	ifeqda	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to if (I < \|A\|, A (I), B (I - \|A\|)) = (A ++ B) (I)$
98	97	eqcomd	$⊢ ((A \in Word V \land B \in Word V) \land I \in ℤ) \to (A ++ B) (I) = if (I < \|A\|, A (I), B (I - \|A\|))$
99	98	3impa	$⊢ (A \in Word V \land B \in Word V \land I \in ℤ) \to (A ++ B) (I) = if (I < \|A\|, A (I), B (I - \|A\|))$

Metamath Proof Explorer

Theorem ccatsymb

Proof