Metamath Proof Explorer

Theorem efgtlen

Description: Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
Assertion efgtlen ⊢ X ∈ W ∧ A ∈ ran ⁡ T ⁡ X → A = X + 2

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
2 efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
3 efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
4 efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
5 1 2 3 4 efgtf ⊢ X ∈ W → T ⁡ X = a ∈ 0 … X , b ∈ I × 2 𝑜 ⟼ X splice a a ⟨“ b M ⁡ b ”⟩ ∧ T ⁡ X : 0 … X × I × 2 𝑜 ⟶ W
6 5 simpld ⊢ X ∈ W → T ⁡ X = a ∈ 0 … X , b ∈ I × 2 𝑜 ⟼ X splice a a ⟨“ b M ⁡ b ”⟩
7 6 rneqd ⊢ X ∈ W → ran ⁡ T ⁡ X = ran ⁡ a ∈ 0 … X , b ∈ I × 2 𝑜 ⟼ X splice a a ⟨“ b M ⁡ b ”⟩
8 7 eleq2d ⊢ X ∈ W → A ∈ ran ⁡ T ⁡ X ↔ A ∈ ran ⁡ a ∈ 0 … X , b ∈ I × 2 𝑜 ⟼ X splice a a ⟨“ b M ⁡ b ”⟩
9 eqid ⊢ a ∈ 0 … X , b ∈ I × 2 𝑜 ⟼ X splice a a ⟨“ b M ⁡ b ”⟩ = a ∈ 0 … X , b ∈ I × 2 𝑜 ⟼ X splice a a ⟨“ b M ⁡ b ”⟩
10 ovex ⊢ X splice a a ⟨“ b M ⁡ b ”⟩ ∈ V
11 9 10 elrnmpo ⊢ A ∈ ran ⁡ a ∈ 0 … X , b ∈ I × 2 𝑜 ⟼ X splice a a ⟨“ b M ⁡ b ”⟩ ↔ ∃ a ∈ 0 … X ∃ b ∈ I × 2 𝑜 A = X splice a a ⟨“ b M ⁡ b ”⟩
12 8 11 bitrdi ⊢ X ∈ W → A ∈ ran ⁡ T ⁡ X ↔ ∃ a ∈ 0 … X ∃ b ∈ I × 2 𝑜 A = X splice a a ⟨“ b M ⁡ b ”⟩
13 fviss ⊢ I ⁡ Word I × 2 𝑜 ⊆ Word I × 2 𝑜
14 1 13 eqsstri ⊢ W ⊆ Word I × 2 𝑜
15 simpl ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → X ∈ W
16 14 15 sselid ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → X ∈ Word I × 2 𝑜
17 elfzuz ⊢ a ∈ 0 … X → a ∈ ℤ ≥ 0
18 17 ad2antrl ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → a ∈ ℤ ≥ 0
19 eluzfz2b ⊢ a ∈ ℤ ≥ 0 ↔ a ∈ 0 … a
20 18 19 sylib ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → a ∈ 0 … a
21 simprl ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → a ∈ 0 … X
22 simprr ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → b ∈ I × 2 𝑜
23 3 efgmf ⊢ M : I × 2 𝑜 ⟶ I × 2 𝑜
24 23 ffvelrni ⊢ b ∈ I × 2 𝑜 → M ⁡ b ∈ I × 2 𝑜
25 22 24 syl ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → M ⁡ b ∈ I × 2 𝑜
26 22 25 s2cld ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → ⟨“ b M ⁡ b ”⟩ ∈ Word I × 2 𝑜
27 16 20 21 26 spllen ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → X splice a a ⟨“ b M ⁡ b ”⟩ = X + ⟨“ b M ⁡ b ”⟩ - a − a
28 s2len ⊢ ⟨“ b M ⁡ b ”⟩ = 2
29 28 a1i ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → ⟨“ b M ⁡ b ”⟩ = 2
30 eluzelcn ⊢ a ∈ ℤ ≥ 0 → a ∈ ℂ
31 18 30 syl ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → a ∈ ℂ
32 31 subidd ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → a − a = 0
33 29 32 oveq12d ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → ⟨“ b M ⁡ b ”⟩ − a − a = 2 − 0
34 2cn ⊢ 2 ∈ ℂ
35 34 subid1i ⊢ 2 − 0 = 2
36 33 35 eqtrdi ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → ⟨“ b M ⁡ b ”⟩ − a − a = 2
37 36 oveq2d ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → X + ⟨“ b M ⁡ b ”⟩ - a − a = X + 2
38 27 37 eqtrd ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → X splice a a ⟨“ b M ⁡ b ”⟩ = X + 2
39 fveqeq2 ⊢ A = X splice a a ⟨“ b M ⁡ b ”⟩ → A = X + 2 ↔ X splice a a ⟨“ b M ⁡ b ”⟩ = X + 2
40 38 39 syl5ibrcom ⊢ X ∈ W ∧ a ∈ 0 … X ∧ b ∈ I × 2 𝑜 → A = X splice a a ⟨“ b M ⁡ b ”⟩ → A = X + 2
41 40 rexlimdvva ⊢ X ∈ W → ∃ a ∈ 0 … X ∃ b ∈ I × 2 𝑜 A = X splice a a ⟨“ b M ⁡ b ”⟩ → A = X + 2
42 12 41 sylbid ⊢ X ∈ W → A ∈ ran ⁡ T ⁡ X → A = X + 2
43 42 imp ⊢ X ∈ W ∧ A ∈ ran ⁡ T ⁡ X → A = X + 2