efginvrel2 - Metamath Proof Explorer

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

Theorem efginvrel2 19595

Description: The inverse of the reverse of a word composed with the word relates to the identity. (This provides an explicit expression for the representation of the group inverse, given a representative of the free group equivalence class.) (Contributed by Mario Carneiro, 1-Oct-2015.)

**Hypotheses**
Ref	Expression
efgval.w	⊢ 𝑊 = ( I ‘Word (𝐼 × 2_o))
efgval.r	⊢ ∼ = ( ~_FG ‘𝐼)
efgval2.m	⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_o ↦ ⟨𝑦, (1_o ∖ 𝑧)⟩)
efgval2.t	⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2_o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))

**Assertion**
Ref	Expression
efginvrel2	⊢ (𝐴 ∈ 𝑊 → (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼ ∅)

Distinct variable groups: 𝑦,𝑧 𝑣,𝑛,𝑤,𝑦,𝑧 𝑛,𝑀,𝑣,𝑤 𝑛,𝑊,𝑣,𝑤,𝑦,𝑧 𝑦, ∼ ,𝑧 𝑛,𝐼,𝑣,𝑤,𝑦,𝑧 Allowed substitution hints: 𝐴(𝑦,𝑧,𝑤,𝑣,𝑛) ∼ (𝑤,𝑣,𝑛) 𝑇(𝑦,𝑧,𝑤,𝑣,𝑛) 𝑀(𝑦,𝑧)

Proof of Theorem efginvrel2 Dummy variables 𝑎 𝑏 𝑐 𝑢 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		efgval.w	. . . 4 ⊢ 𝑊 = ( I ‘Word (𝐼 × 2_o))
2		fviss 6969	. . . 4 ⊢ ( I ‘Word (𝐼 × 2_o)) ⊆ Word (𝐼 × 2_o)
3	1, 2	eqsstri 4017	. . 3 ⊢ 𝑊 ⊆ Word (𝐼 × 2_o)
4	3	sseli 3979	. 2 ⊢ (𝐴 ∈ 𝑊 → 𝐴 ∈ Word (𝐼 × 2_o))
5		id 22	. . . . . 6 ⊢ (𝑐 = ∅ → 𝑐 = ∅)
6		fveq2 6892	. . . . . . . . 9 ⊢ (𝑐 = ∅ → (reverse‘𝑐) = (reverse‘∅))
7		rev0 14714	. . . . . . . . 9 ⊢ (reverse‘∅) = ∅
8	6, 7	eqtrdi 2789	. . . . . . . 8 ⊢ (𝑐 = ∅ → (reverse‘𝑐) = ∅)
9	8	coeq2d 5863	. . . . . . 7 ⊢ (𝑐 = ∅ → (𝑀 ∘ (reverse‘𝑐)) = (𝑀 ∘ ∅))
10		co02 6260	. . . . . . 7 ⊢ (𝑀 ∘ ∅) = ∅
11	9, 10	eqtrdi 2789	. . . . . 6 ⊢ (𝑐 = ∅ → (𝑀 ∘ (reverse‘𝑐)) = ∅)
12	5, 11	oveq12d 7427	. . . . 5 ⊢ (𝑐 = ∅ → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) = (∅ ++ ∅))
13	12	breq1d 5159	. . . 4 ⊢ (𝑐 = ∅ → ((𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅ ↔ (∅ ++ ∅) ∼ ∅))
14	13	imbi2d 341	. . 3 ⊢ (𝑐 = ∅ → ((𝐴 ∈ 𝑊 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅) ↔ (𝐴 ∈ 𝑊 → (∅ ++ ∅) ∼ ∅)))
15		id 22	. . . . . 6 ⊢ (𝑐 = 𝑎 → 𝑐 = 𝑎)
16		fveq2 6892	. . . . . . 7 ⊢ (𝑐 = 𝑎 → (reverse‘𝑐) = (reverse‘𝑎))
17	16	coeq2d 5863	. . . . . 6 ⊢ (𝑐 = 𝑎 → (𝑀 ∘ (reverse‘𝑐)) = (𝑀 ∘ (reverse‘𝑎)))
18	15, 17	oveq12d 7427	. . . . 5 ⊢ (𝑐 = 𝑎 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) = (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))
19	18	breq1d 5159	. . . 4 ⊢ (𝑐 = 𝑎 → ((𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅ ↔ (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ∅))
20	19	imbi2d 341	. . 3 ⊢ (𝑐 = 𝑎 → ((𝐴 ∈ 𝑊 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅) ↔ (𝐴 ∈ 𝑊 → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ∅)))
21		id 22	. . . . . 6 ⊢ (𝑐 = (𝑎 ++ ⟨“𝑏”⟩) → 𝑐 = (𝑎 ++ ⟨“𝑏”⟩))
22		fveq2 6892	. . . . . . 7 ⊢ (𝑐 = (𝑎 ++ ⟨“𝑏”⟩) → (reverse‘𝑐) = (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))
23	22	coeq2d 5863	. . . . . 6 ⊢ (𝑐 = (𝑎 ++ ⟨“𝑏”⟩) → (𝑀 ∘ (reverse‘𝑐)) = (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩))))
24	21, 23	oveq12d 7427	. . . . 5 ⊢ (𝑐 = (𝑎 ++ ⟨“𝑏”⟩) → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) = ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))))
25	24	breq1d 5159	. . . 4 ⊢ (𝑐 = (𝑎 ++ ⟨“𝑏”⟩) → ((𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅ ↔ ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) ∼ ∅))
26	25	imbi2d 341	. . 3 ⊢ (𝑐 = (𝑎 ++ ⟨“𝑏”⟩) → ((𝐴 ∈ 𝑊 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅) ↔ (𝐴 ∈ 𝑊 → ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) ∼ ∅)))
27		id 22	. . . . . 6 ⊢ (𝑐 = 𝐴 → 𝑐 = 𝐴)
28		fveq2 6892	. . . . . . 7 ⊢ (𝑐 = 𝐴 → (reverse‘𝑐) = (reverse‘𝐴))
29	28	coeq2d 5863	. . . . . 6 ⊢ (𝑐 = 𝐴 → (𝑀 ∘ (reverse‘𝑐)) = (𝑀 ∘ (reverse‘𝐴)))
30	27, 29	oveq12d 7427	. . . . 5 ⊢ (𝑐 = 𝐴 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) = (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))))
31	30	breq1d 5159	. . . 4 ⊢ (𝑐 = 𝐴 → ((𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅ ↔ (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼ ∅))
32	31	imbi2d 341	. . 3 ⊢ (𝑐 = 𝐴 → ((𝐴 ∈ 𝑊 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅) ↔ (𝐴 ∈ 𝑊 → (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼ ∅)))
33		ccatidid 14540	. . . 4 ⊢ (∅ ++ ∅) = ∅
34		efgval.r	. . . . . . 7 ⊢ ∼ = ( ~_FG ‘𝐼)
35	1, 34	efger 19586	. . . . . 6 ⊢ ∼ Er 𝑊
36	35	a1i 11	. . . . 5 ⊢ (𝐴 ∈ 𝑊 → ∼ Er 𝑊)
37		wrd0 14489	. . . . . 6 ⊢ ∅ ∈ Word (𝐼 × 2_o)
38	1	efgrcl 19583	. . . . . . 7 ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2_o)))
39	38	simprd 497	. . . . . 6 ⊢ (𝐴 ∈ 𝑊 → 𝑊 = Word (𝐼 × 2_o))
40	37, 39	eleqtrrid 2841	. . . . 5 ⊢ (𝐴 ∈ 𝑊 → ∅ ∈ 𝑊)
41	36, 40	erref 8723	. . . 4 ⊢ (𝐴 ∈ 𝑊 → ∅ ∼ ∅)
42	33, 41	eqbrtrid 5184	. . 3 ⊢ (𝐴 ∈ 𝑊 → (∅ ++ ∅) ∼ ∅)
43	35	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ∼ Er 𝑊)
44		simprl 770	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → 𝑎 ∈ Word (𝐼 × 2_o))
45		revcl 14711	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ Word (𝐼 × 2_o) → (reverse‘𝑎) ∈ Word (𝐼 × 2_o))
46	45	ad2antrl 727	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (reverse‘𝑎) ∈ Word (𝐼 × 2_o))
47		efgval2.m	. . . . . . . . . . . 12 ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_o ↦ ⟨𝑦, (1_o ∖ 𝑧)⟩)
48	47	efgmf 19581	. . . . . . . . . . 11 ⊢ 𝑀:(𝐼 × 2_o)⟶(𝐼 × 2_o)
49		wrdco 14782	. . . . . . . . . . 11 ⊢ (((reverse‘𝑎) ∈ Word (𝐼 × 2_o) ∧ 𝑀:(𝐼 × 2_o)⟶(𝐼 × 2_o)) → (𝑀 ∘ (reverse‘𝑎)) ∈ Word (𝐼 × 2_o))
50	46, 48, 49	sylancl 587	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑀 ∘ (reverse‘𝑎)) ∈ Word (𝐼 × 2_o))
51		ccatcl 14524	. . . . . . . . . 10 ⊢ ((𝑎 ∈ Word (𝐼 × 2_o) ∧ (𝑀 ∘ (reverse‘𝑎)) ∈ Word (𝐼 × 2_o)) → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ Word (𝐼 × 2_o))
52	44, 50, 51	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ Word (𝐼 × 2_o))
53	39	adantr 482	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → 𝑊 = Word (𝐼 × 2_o))
54	52, 53	eleqtrrd 2837	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ 𝑊)
55		lencl 14483	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ Word (𝐼 × 2_o) → (♯‘𝑎) ∈ ℕ₀)
56	55	ad2antrl 727	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘𝑎) ∈ ℕ₀)
57		nn0uz 12864	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
58	56, 57	eleqtrdi 2844	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘𝑎) ∈ (ℤ_≥‘0))
59		ccatlen 14525	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ Word (𝐼 × 2_o) ∧ (𝑀 ∘ (reverse‘𝑎)) ∈ Word (𝐼 × 2_o)) → (♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) = ((♯‘𝑎) + (♯‘(𝑀 ∘ (reverse‘𝑎)))))
60	44, 50, 59	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) = ((♯‘𝑎) + (♯‘(𝑀 ∘ (reverse‘𝑎)))))
61	56	nn0zd 12584	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘𝑎) ∈ ℤ)
62	61	uzidd 12838	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘𝑎) ∈ (ℤ_≥‘(♯‘𝑎)))
63		lencl 14483	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∘ (reverse‘𝑎)) ∈ Word (𝐼 × 2_o) → (♯‘(𝑀 ∘ (reverse‘𝑎))) ∈ ℕ₀)
64	50, 63	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘(𝑀 ∘ (reverse‘𝑎))) ∈ ℕ₀)
65		uzaddcl 12888	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝑎) ∈ (ℤ_≥‘(♯‘𝑎)) ∧ (♯‘(𝑀 ∘ (reverse‘𝑎))) ∈ ℕ₀) → ((♯‘𝑎) + (♯‘(𝑀 ∘ (reverse‘𝑎)))) ∈ (ℤ_≥‘(♯‘𝑎)))
66	62, 64, 65	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((♯‘𝑎) + (♯‘(𝑀 ∘ (reverse‘𝑎)))) ∈ (ℤ_≥‘(♯‘𝑎)))
67	60, 66	eqeltrd 2834	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) ∈ (ℤ_≥‘(♯‘𝑎)))
68		elfzuzb 13495	. . . . . . . . . . . 12 ⊢ ((♯‘𝑎) ∈ (0...(♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) ↔ ((♯‘𝑎) ∈ (ℤ_≥‘0) ∧ (♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) ∈ (ℤ_≥‘(♯‘𝑎))))
69	58, 67, 68	sylanbrc 584	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘𝑎) ∈ (0...(♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))))
70		simprr 772	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → 𝑏 ∈ (𝐼 × 2_o))
71		efgval2.t	. . . . . . . . . . . 12 ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2_o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
72	1, 34, 47, 71	efgtval 19591	. . . . . . . . . . 11 ⊢ (((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ 𝑊 ∧ (♯‘𝑎) ∈ (0...(♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) ∧ 𝑏 ∈ (𝐼 × 2_o)) → ((♯‘𝑎)(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))𝑏) = ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) splice ⟨(♯‘𝑎), (♯‘𝑎), ⟨“𝑏(𝑀‘𝑏)”⟩⟩))
73	54, 69, 70, 72	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((♯‘𝑎)(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))𝑏) = ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) splice ⟨(♯‘𝑎), (♯‘𝑎), ⟨“𝑏(𝑀‘𝑏)”⟩⟩))
74	37	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ∅ ∈ Word (𝐼 × 2_o))
75	48	ffvelcdmi 7086	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (𝐼 × 2_o) → (𝑀‘𝑏) ∈ (𝐼 × 2_o))
76	75	ad2antll 728	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑀‘𝑏) ∈ (𝐼 × 2_o))
77	70, 76	s2cld 14822	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ⟨“𝑏(𝑀‘𝑏)”⟩ ∈ Word (𝐼 × 2_o))
78		ccatrid 14537	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ Word (𝐼 × 2_o) → (𝑎 ++ ∅) = 𝑎)
79	78	ad2antrl 727	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑎 ++ ∅) = 𝑎)
80	79	eqcomd 2739	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → 𝑎 = (𝑎 ++ ∅))
81	80	oveq1d 7424	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) = ((𝑎 ++ ∅) ++ (𝑀 ∘ (reverse‘𝑎))))
82		eqidd 2734	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘𝑎) = (♯‘𝑎))
83		hash0 14327	. . . . . . . . . . . . 13 ⊢ (♯‘∅) = 0
84	83	oveq2i 7420	. . . . . . . . . . . 12 ⊢ ((♯‘𝑎) + (♯‘∅)) = ((♯‘𝑎) + 0)
85	56	nn0cnd 12534	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘𝑎) ∈ ℂ)
86	85	addridd 11414	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((♯‘𝑎) + 0) = (♯‘𝑎))
87	84, 86	eqtr2id 2786	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (♯‘𝑎) = ((♯‘𝑎) + (♯‘∅)))
88	44, 74, 50, 77, 81, 82, 87	splval2 14707	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) splice ⟨(♯‘𝑎), (♯‘𝑎), ⟨“𝑏(𝑀‘𝑏)”⟩⟩) = ((𝑎 ++ ⟨“𝑏(𝑀‘𝑏)”⟩) ++ (𝑀 ∘ (reverse‘𝑎))))
89	70	s1cld 14553	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ⟨“𝑏”⟩ ∈ Word (𝐼 × 2_o))
90		revccat 14716	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ Word (𝐼 × 2_o) ∧ ⟨“𝑏”⟩ ∈ Word (𝐼 × 2_o)) → (reverse‘(𝑎 ++ ⟨“𝑏”⟩)) = ((reverse‘⟨“𝑏”⟩) ++ (reverse‘𝑎)))
91	44, 89, 90	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (reverse‘(𝑎 ++ ⟨“𝑏”⟩)) = ((reverse‘⟨“𝑏”⟩) ++ (reverse‘𝑎)))
92		revs1 14715	. . . . . . . . . . . . . . . 16 ⊢ (reverse‘⟨“𝑏”⟩) = ⟨“𝑏”⟩
93	92	oveq1i 7419	. . . . . . . . . . . . . . 15 ⊢ ((reverse‘⟨“𝑏”⟩) ++ (reverse‘𝑎)) = (⟨“𝑏”⟩ ++ (reverse‘𝑎))
94	91, 93	eqtrdi 2789	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (reverse‘(𝑎 ++ ⟨“𝑏”⟩)) = (⟨“𝑏”⟩ ++ (reverse‘𝑎)))
95	94	coeq2d 5863	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩))) = (𝑀 ∘ (⟨“𝑏”⟩ ++ (reverse‘𝑎))))
96	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → 𝑀:(𝐼 × 2_o)⟶(𝐼 × 2_o))
97		ccatco 14786	. . . . . . . . . . . . . 14 ⊢ ((⟨“𝑏”⟩ ∈ Word (𝐼 × 2_o) ∧ (reverse‘𝑎) ∈ Word (𝐼 × 2_o) ∧ 𝑀:(𝐼 × 2_o)⟶(𝐼 × 2_o)) → (𝑀 ∘ (⟨“𝑏”⟩ ++ (reverse‘𝑎))) = ((𝑀 ∘ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘𝑎))))
98	89, 46, 96, 97	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑀 ∘ (⟨“𝑏”⟩ ++ (reverse‘𝑎))) = ((𝑀 ∘ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘𝑎))))
99		s1co 14784	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ (𝐼 × 2_o) ∧ 𝑀:(𝐼 × 2_o)⟶(𝐼 × 2_o)) → (𝑀 ∘ ⟨“𝑏”⟩) = ⟨“(𝑀‘𝑏)”⟩)
100	70, 48, 99	sylancl 587	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑀 ∘ ⟨“𝑏”⟩) = ⟨“(𝑀‘𝑏)”⟩)
101	100	oveq1d 7424	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((𝑀 ∘ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘𝑎))) = (⟨“(𝑀‘𝑏)”⟩ ++ (𝑀 ∘ (reverse‘𝑎))))
102	95, 98, 101	3eqtrd 2777	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩))) = (⟨“(𝑀‘𝑏)”⟩ ++ (𝑀 ∘ (reverse‘𝑎))))
103	102	oveq2d 7425	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) = ((𝑎 ++ ⟨“𝑏”⟩) ++ (⟨“(𝑀‘𝑏)”⟩ ++ (𝑀 ∘ (reverse‘𝑎)))))
104		ccatcl 14524	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ Word (𝐼 × 2_o) ∧ ⟨“𝑏”⟩ ∈ Word (𝐼 × 2_o)) → (𝑎 ++ ⟨“𝑏”⟩) ∈ Word (𝐼 × 2_o))
105	44, 89, 104	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑎 ++ ⟨“𝑏”⟩) ∈ Word (𝐼 × 2_o))
106	76	s1cld 14553	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ⟨“(𝑀‘𝑏)”⟩ ∈ Word (𝐼 × 2_o))
107		ccatass 14538	. . . . . . . . . . . 12 ⊢ (((𝑎 ++ ⟨“𝑏”⟩) ∈ Word (𝐼 × 2_o) ∧ ⟨“(𝑀‘𝑏)”⟩ ∈ Word (𝐼 × 2_o) ∧ (𝑀 ∘ (reverse‘𝑎)) ∈ Word (𝐼 × 2_o)) → (((𝑎 ++ ⟨“𝑏”⟩) ++ ⟨“(𝑀‘𝑏)”⟩) ++ (𝑀 ∘ (reverse‘𝑎))) = ((𝑎 ++ ⟨“𝑏”⟩) ++ (⟨“(𝑀‘𝑏)”⟩ ++ (𝑀 ∘ (reverse‘𝑎)))))
108	105, 106, 50, 107	syl3anc 1372	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (((𝑎 ++ ⟨“𝑏”⟩) ++ ⟨“(𝑀‘𝑏)”⟩) ++ (𝑀 ∘ (reverse‘𝑎))) = ((𝑎 ++ ⟨“𝑏”⟩) ++ (⟨“(𝑀‘𝑏)”⟩ ++ (𝑀 ∘ (reverse‘𝑎)))))
109		ccatass 14538	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ Word (𝐼 × 2_o) ∧ ⟨“𝑏”⟩ ∈ Word (𝐼 × 2_o) ∧ ⟨“(𝑀‘𝑏)”⟩ ∈ Word (𝐼 × 2_o)) → ((𝑎 ++ ⟨“𝑏”⟩) ++ ⟨“(𝑀‘𝑏)”⟩) = (𝑎 ++ (⟨“𝑏”⟩ ++ ⟨“(𝑀‘𝑏)”⟩)))
110	44, 89, 106, 109	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((𝑎 ++ ⟨“𝑏”⟩) ++ ⟨“(𝑀‘𝑏)”⟩) = (𝑎 ++ (⟨“𝑏”⟩ ++ ⟨“(𝑀‘𝑏)”⟩)))
111		df-s2 14799	. . . . . . . . . . . . . 14 ⊢ ⟨“𝑏(𝑀‘𝑏)”⟩ = (⟨“𝑏”⟩ ++ ⟨“(𝑀‘𝑏)”⟩)
112	111	oveq2i 7420	. . . . . . . . . . . . 13 ⊢ (𝑎 ++ ⟨“𝑏(𝑀‘𝑏)”⟩) = (𝑎 ++ (⟨“𝑏”⟩ ++ ⟨“(𝑀‘𝑏)”⟩))
113	110, 112	eqtr4di 2791	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((𝑎 ++ ⟨“𝑏”⟩) ++ ⟨“(𝑀‘𝑏)”⟩) = (𝑎 ++ ⟨“𝑏(𝑀‘𝑏)”⟩))
114	113	oveq1d 7424	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (((𝑎 ++ ⟨“𝑏”⟩) ++ ⟨“(𝑀‘𝑏)”⟩) ++ (𝑀 ∘ (reverse‘𝑎))) = ((𝑎 ++ ⟨“𝑏(𝑀‘𝑏)”⟩) ++ (𝑀 ∘ (reverse‘𝑎))))
115	103, 108, 114	3eqtr2rd 2780	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((𝑎 ++ ⟨“𝑏(𝑀‘𝑏)”⟩) ++ (𝑀 ∘ (reverse‘𝑎))) = ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))))
116	73, 88, 115	3eqtrd 2777	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((♯‘𝑎)(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))𝑏) = ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))))
117	1, 34, 47, 71	efgtf 19590	. . . . . . . . . . . . 13 ⊢ ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ 𝑊 → ((𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) = (𝑚 ∈ (0...(♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))), 𝑢 ∈ (𝐼 × 2_o) ↦ ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) splice ⟨𝑚, 𝑚, ⟨“𝑢(𝑀‘𝑢)”⟩⟩)) ∧ (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))):((0...(♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 × 2_o))⟶𝑊))
118	117	simprd 497	. . . . . . . . . . . 12 ⊢ ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ 𝑊 → (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))):((0...(♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 × 2_o))⟶𝑊)
119	54, 118	syl 17	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))):((0...(♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 × 2_o))⟶𝑊)
120	119	ffnd 6719	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) Fn ((0...(♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 × 2_o)))
121		fnovrn 7582	. . . . . . . . . 10 ⊢ (((𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) Fn ((0...(♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 × 2_o)) ∧ (♯‘𝑎) ∈ (0...(♯‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) ∧ 𝑏 ∈ (𝐼 × 2_o)) → ((♯‘𝑎)(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))𝑏) ∈ ran (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))))
122	120, 69, 70, 121	syl3anc 1372	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((♯‘𝑎)(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))𝑏) ∈ ran (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))))
123	116, 122	eqeltrrd 2835	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) ∈ ran (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))))
124	1, 34, 47, 71	efgi2 19593	. . . . . . . 8 ⊢ (((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ 𝑊 ∧ ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) ∈ ran (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))))
125	54, 123, 124	syl2anc 585	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))))
126	43, 125	ersym 8715	. . . . . 6 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) ∼ (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))
127	43	ertr 8718	. . . . . 6 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) ∼ (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∧ (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ∅) → ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) ∼ ∅))
128	126, 127	mpand 694	. . . . 5 ⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o))) → ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ∅ → ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) ∼ ∅))
129	128	expcom 415	. . . 4 ⊢ ((𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o)) → (𝐴 ∈ 𝑊 → ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ∅ → ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) ∼ ∅)))
130	129	a2d 29	. . 3 ⊢ ((𝑎 ∈ Word (𝐼 × 2_o) ∧ 𝑏 ∈ (𝐼 × 2_o)) → ((𝐴 ∈ 𝑊 → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ∅) → (𝐴 ∈ 𝑊 → ((𝑎 ++ ⟨“𝑏”⟩) ++ (𝑀 ∘ (reverse‘(𝑎 ++ ⟨“𝑏”⟩)))) ∼ ∅)))
131	14, 20, 26, 32, 42, 130	wrdind 14672	. 2 ⊢ (𝐴 ∈ Word (𝐼 × 2_o) → (𝐴 ∈ 𝑊 → (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼ ∅))
132	4, 131	mpcom 38	1 ⊢ (𝐴 ∈ 𝑊 → (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼ ∅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 Vcvv 3475 ∖ cdif 3946 ∅c0 4323 ⟨cop 4635 ⟨cotp 4637 class class class wbr 5149 ↦ cmpt 5232 I cid 5574 × cxp 5675 ran crn 5678 ∘ ccom 5681 Fn wfn 6539 ⟶wf 6540 ‘cfv 6544 (class class class)co 7409 ∈ cmpo 7411 1_oc1o 8459 2_oc2o 8460 Er wer 8700 0cc0 11110 + caddc 11113 ℕ₀cn0 12472 ℤ_≥cuz 12822 ...cfz 13484 ♯chash 14290 Word cword 14464 ++ cconcat 14520 ⟨“cs1 14545 splice csplice 14699 reversecreverse 14708 ⟨“cs2 14792 ~_FG cefg 19574

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-ot 4638 df-uni 4910 df-int 4952 df-iun 5000 df-iin 5001 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-2o 8467 df-er 8703 df-ec 8705 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-card 9934 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-nn 12213 df-n0 12473 df-xnn0 12545 df-z 12559 df-uz 12823 df-fz 13485 df-fzo 13628 df-hash 14291 df-word 14465 df-lsw 14513 df-concat 14521 df-s1 14546 df-substr 14591 df-pfx 14621 df-splice 14700 df-reverse 14709 df-s2 14799 df-efg 19577

This theorem is referenced by: efginvrel1 19596 frgpinv 19632

W3C validator