ccatco - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ccatco		Structured version Visualization version GIF version

Theorem ccatco 13801

Description: Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015.)

**Assertion**
Ref	Expression
ccatco	⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)))

Proof of Theorem ccatco Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lenco 13798	. . . . . . 7 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑆)) = (♯‘𝑆))
2	1	3adant2 1126	. . . . . 6 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑆)) = (♯‘𝑆))
3		lenco 13798	. . . . . . 7 ⊢ ((𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑇)) = (♯‘𝑇))
4	3	3adant1 1125	. . . . . 6 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑇)) = (♯‘𝑇))
5	2, 4	oveq12d 6832	. . . . 5 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇))) = ((♯‘𝑆) + (♯‘𝑇)))
6	5	oveq2d 6830	. . . 4 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇)))) = (0..^((♯‘𝑆) + (♯‘𝑇))))
7	6	mpteq1d 4890	. . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))))) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))))))
8	2	oveq2d 6830	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^(♯‘(𝐹 ∘ 𝑆))) = (0..^(♯‘𝑆)))
9	8	adantr 472	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → (0..^(♯‘(𝐹 ∘ 𝑆))) = (0..^(♯‘𝑆)))
10	9	eleq2d 2825	. . . . . 6 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))) ↔ 𝑥 ∈ (0..^(♯‘𝑆))))
11	10	ifbid 4252	. . . . 5 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))) = if(𝑥 ∈ (0..^(♯‘𝑆)), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))))
12		wrdf 13516	. . . . . . . . . . 11 ⊢ (𝑆 ∈ Word 𝐴 → 𝑆:(0..^(♯‘𝑆))⟶𝐴)
13	12	3ad2ant1 1128	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑆:(0..^(♯‘𝑆))⟶𝐴)
14	13	adantr 472	. . . . . . . . 9 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑆:(0..^(♯‘𝑆))⟶𝐴)
15		ffn 6206	. . . . . . . . 9 ⊢ (𝑆:(0..^(♯‘𝑆))⟶𝐴 → 𝑆 Fn (0..^(♯‘𝑆)))
16	14, 15	syl 17	. . . . . . . 8 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑆 Fn (0..^(♯‘𝑆)))
17		fvco2 6436	. . . . . . . 8 ⊢ ((𝑆 Fn (0..^(♯‘𝑆)) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝐹 ∘ 𝑆)‘𝑥) = (𝐹‘(𝑆‘𝑥)))
18	16, 17	sylan 489	. . . . . . 7 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝐹 ∘ 𝑆)‘𝑥) = (𝐹‘(𝑆‘𝑥)))
19		iftrue 4236	. . . . . . . 8 ⊢ (𝑥 ∈ (0..^(♯‘𝑆)) → if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) = (𝐹‘(𝑆‘𝑥)))
20	19	adantl 473	. . . . . . 7 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) = (𝐹‘(𝑆‘𝑥)))
21	18, 20	eqtr4d 2797	. . . . . 6 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝐹 ∘ 𝑆)‘𝑥) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))))
22		wrdf 13516	. . . . . . . . . . 11 ⊢ (𝑇 ∈ Word 𝐴 → 𝑇:(0..^(♯‘𝑇))⟶𝐴)
23	22	3ad2ant2 1129	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑇:(0..^(♯‘𝑇))⟶𝐴)
24	23	ad2antrr 764	. . . . . . . . 9 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑆))) → 𝑇:(0..^(♯‘𝑇))⟶𝐴)
25		ffn 6206	. . . . . . . . 9 ⊢ (𝑇:(0..^(♯‘𝑇))⟶𝐴 → 𝑇 Fn (0..^(♯‘𝑇)))
26	24, 25	syl 17	. . . . . . . 8 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑆))) → 𝑇 Fn (0..^(♯‘𝑇)))
27		lencl 13530	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈ ℕ₀)
28	27	nn0zd 11692	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈ ℤ)
29	28	3ad2ant1 1128	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘𝑆) ∈ ℤ)
30		fzospliti 12714	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ∧ (♯‘𝑆) ∈ ℤ) → (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))))
31	30	ancoms 468	. . . . . . . . . . 11 ⊢ (((♯‘𝑆) ∈ ℤ ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))))
32	29, 31	sylan 489	. . . . . . . . . 10 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))))
33	32	orcanai 990	. . . . . . . . 9 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑆))) → 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))
34		lencl 13530	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ ℕ₀)
35	34	nn0zd 11692	. . . . . . . . . . 11 ⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ ℤ)
36	35	3ad2ant2 1129	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘𝑇) ∈ ℤ)
37	36	ad2antrr 764	. . . . . . . . 9 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑆))) → (♯‘𝑇) ∈ ℤ)
38		fzosubel3 12743	. . . . . . . . 9 ⊢ ((𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ∧ (♯‘𝑇) ∈ ℤ) → (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇)))
39	33, 37, 38	syl2anc 696	. . . . . . . 8 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇)))
40		fvco2 6436	. . . . . . . 8 ⊢ ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇))) → ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘𝑆))) = (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))
41	26, 39, 40	syl2anc 696	. . . . . . 7 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘𝑆))) = (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))
42	2	oveq2d 6830	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 − (♯‘(𝐹 ∘ 𝑆))) = (𝑥 − (♯‘𝑆)))
43	42	fveq2d 6357	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))) = ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘𝑆))))
44	43	ad2antrr 764	. . . . . . 7 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))) = ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘𝑆))))
45		iffalse 4239	. . . . . . . 8 ⊢ (¬ 𝑥 ∈ (0..^(♯‘𝑆)) → if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) = (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))
46	45	adantl 473	. . . . . . 7 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑆))) → if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) = (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))
47	41, 44, 46	3eqtr4d 2804	. . . . . 6 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))))
48	21, 47	ifeqda 4265	. . . . 5 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → if(𝑥 ∈ (0..^(♯‘𝑆)), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))))
49	11, 48	eqtrd 2794	. . . 4 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))))
50	49	mpteq2dva 4896	. . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))))) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))))
51	7, 50	eqtr2d 2795	. 2 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))) = (𝑥 ∈ (0..^((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))))))
52	14	ffvelrnda 6523	. . . 4 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆‘𝑥) ∈ 𝐴)
53	24, 39	ffvelrnd 6524	. . . 4 ⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑇‘(𝑥 − (♯‘𝑆))) ∈ 𝐴)
54	52, 53	ifclda 4264	. . 3 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))) ∈ 𝐴)
55		ccatfval 13565	. . . 4 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆))))))
56	55	3adant3 1127	. . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆))))))
57		simp3 1133	. . . 4 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴⟶𝐵)
58	57	feqmptd 6412	. . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 = (𝑦 ∈ 𝐴 ↦ (𝐹‘𝑦)))
59		fveq2 6353	. . . 4 ⊢ (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))) → (𝐹‘𝑦) = (𝐹‘if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆))))))
60		fvif 6366	. . . 4 ⊢ (𝐹‘if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆))))) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))
61	59, 60	syl6eq 2810	. . 3 ⊢ (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))) → (𝐹‘𝑦) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))))
62	54, 56, 58, 61	fmptco 6560	. 2 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))))
63		ffun 6209	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
64	63	3ad2ant3 1130	. . . 4 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → Fun 𝐹)
65		simp1 1131	. . . 4 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑆 ∈ Word 𝐴)
66		cofunexg 7296	. . . 4 ⊢ ((Fun 𝐹 ∧ 𝑆 ∈ Word 𝐴) → (𝐹 ∘ 𝑆) ∈ V)
67	64, 65, 66	syl2anc 696	. . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑆) ∈ V)
68		simp2 1132	. . . 4 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑇 ∈ Word 𝐴)
69		cofunexg 7296	. . . 4 ⊢ ((Fun 𝐹 ∧ 𝑇 ∈ Word 𝐴) → (𝐹 ∘ 𝑇) ∈ V)
70	64, 68, 69	syl2anc 696	. . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑇) ∈ V)
71		ccatfval 13565	. . 3 ⊢ (((𝐹 ∘ 𝑆) ∈ V ∧ (𝐹 ∘ 𝑇) ∈ V) → ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)) = (𝑥 ∈ (0..^((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))))))
72	67, 70, 71	syl2anc 696	. 2 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)) = (𝑥 ∈ (0..^((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))))))
73	51, 62, 72	3eqtr4d 2804	1 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∨ wo 382 ∧ wa 383 ∧ w3a 1072 = wceq 1632 ∈ wcel 2139 Vcvv 3340 ifcif 4230 ↦ cmpt 4881 ∘ ccom 5270 Fun wfun 6043 Fn wfn 6044 ⟶wf 6045 ‘cfv 6049 (class class class)co 6814 0cc0 10148 + caddc 10151 − cmin 10478 ℤcz 11589 ..^cfzo 12679 ♯chash 13331 Word cword 13497 ++ cconcat 13499

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-rep 4923 ax-sep 4933 ax-nul 4941 ax-pow 4992 ax-pr 5055 ax-un 7115 ax-cnex 10204 ax-resscn 10205 ax-1cn 10206 ax-icn 10207 ax-addcl 10208 ax-addrcl 10209 ax-mulcl 10210 ax-mulrcl 10211 ax-mulcom 10212 ax-addass 10213 ax-mulass 10214 ax-distr 10215 ax-i2m1 10216 ax-1ne0 10217 ax-1rid 10218 ax-rnegex 10219 ax-rrecex 10220 ax-cnre 10221 ax-pre-lttri 10222 ax-pre-lttrn 10223 ax-pre-ltadd 10224 ax-pre-mulgt0 10225

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ne 2933 df-nel 3036 df-ral 3055 df-rex 3056 df-reu 3057 df-rab 3059 df-v 3342 df-sbc 3577 df-csb 3675 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-pss 3731 df-nul 4059 df-if 4231 df-pw 4304 df-sn 4322 df-pr 4324 df-tp 4326 df-op 4328 df-uni 4589 df-int 4628 df-iun 4674 df-br 4805 df-opab 4865 df-mpt 4882 df-tr 4905 df-id 5174 df-eprel 5179 df-po 5187 df-so 5188 df-fr 5225 df-we 5227 df-xp 5272 df-rel 5273 df-cnv 5274 df-co 5275 df-dm 5276 df-rn 5277 df-res 5278 df-ima 5279 df-pred 5841 df-ord 5887 df-on 5888 df-lim 5889 df-suc 5890 df-iota 6012 df-fun 6051 df-fn 6052 df-f 6053 df-f1 6054 df-fo 6055 df-f1o 6056 df-fv 6057 df-riota 6775 df-ov 6817 df-oprab 6818 df-mpt2 6819 df-om 7232 df-1st 7334 df-2nd 7335 df-wrecs 7577 df-recs 7638 df-rdg 7676 df-1o 7730 df-oadd 7734 df-er 7913 df-en 8124 df-dom 8125 df-sdom 8126 df-fin 8127 df-card 8975 df-pnf 10288 df-mnf 10289 df-xr 10290 df-ltxr 10291 df-le 10292 df-sub 10480 df-neg 10481 df-nn 11233 df-n0 11505 df-z 11590 df-uz 11900 df-fz 12540 df-fzo 12680 df-hash 13332 df-word 13505 df-concat 13507

This theorem is referenced by: cats1co 13821 frmdgsum 17620 frmdup1 17622 efginvrel2 18360 frgpuplem 18405 frgpup1 18408 mrsubccat 31743

W3C validator