efgrelexlema

Description: If two words A , B are related under the free group equivalence, then there exist two extension sequences a , b such that a ends at A , b ends at B , and a and B have the same starting point. (Contributed by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Hypotheses	efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
	efgval.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
	efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
	efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2_o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
	efgred.d	⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
	efgred.s	⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
	efgrelexlem.1	⊢ 𝐿 = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ∃ 𝑐 ∈ ( ^◡ 𝑆 “ { 𝑖 } ) ∃ 𝑑 ∈ ( ^◡ 𝑆 “ { 𝑗 } ) ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) }
Assertion	efgrelexlema	⊢ ( 𝐴 𝐿 𝐵 ↔ ∃ 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝐵 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
2		efgval.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
3		efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
4		efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2_o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5		efgred.d	⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
6		efgred.s	⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
7		efgrelexlem.1	⊢ 𝐿 = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ∃ 𝑐 ∈ ( ^◡ 𝑆 “ { 𝑖 } ) ∃ 𝑑 ∈ ( ^◡ 𝑆 “ { 𝑗 } ) ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) }
8	7	bropaex12	⊢ ( 𝐴 𝐿 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
9		n0i	⊢ ( 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) → ¬ ( ^◡ 𝑆 “ { 𝐴 } ) = ∅ )
10		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
11		imaeq2	⊢ ( { 𝐴 } = ∅ → ( ^◡ 𝑆 “ { 𝐴 } ) = ( ^◡ 𝑆 “ ∅ ) )
12	10 11	sylbi	⊢ ( ¬ 𝐴 ∈ V → ( ^◡ 𝑆 “ { 𝐴 } ) = ( ^◡ 𝑆 “ ∅ ) )
13		ima0	⊢ ( ^◡ 𝑆 “ ∅ ) = ∅
14	12 13	eqtrdi	⊢ ( ¬ 𝐴 ∈ V → ( ^◡ 𝑆 “ { 𝐴 } ) = ∅ )
15	9 14	nsyl2	⊢ ( 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) → 𝐴 ∈ V )
16		n0i	⊢ ( 𝑏 ∈ ( ^◡ 𝑆 “ { 𝐵 } ) → ¬ ( ^◡ 𝑆 “ { 𝐵 } ) = ∅ )
17		snprc	⊢ ( ¬ 𝐵 ∈ V ↔ { 𝐵 } = ∅ )
18		imaeq2	⊢ ( { 𝐵 } = ∅ → ( ^◡ 𝑆 “ { 𝐵 } ) = ( ^◡ 𝑆 “ ∅ ) )
19	17 18	sylbi	⊢ ( ¬ 𝐵 ∈ V → ( ^◡ 𝑆 “ { 𝐵 } ) = ( ^◡ 𝑆 “ ∅ ) )
20	19 13	eqtrdi	⊢ ( ¬ 𝐵 ∈ V → ( ^◡ 𝑆 “ { 𝐵 } ) = ∅ )
21	16 20	nsyl2	⊢ ( 𝑏 ∈ ( ^◡ 𝑆 “ { 𝐵 } ) → 𝐵 ∈ V )
22	15 21	anim12i	⊢ ( ( 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) ∧ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝐵 } ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
23	22	a1d	⊢ ( ( 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) ∧ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝐵 } ) ) → ( ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
24	23	rexlimivv	⊢ ( ∃ 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝐵 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
25		fveq1	⊢ ( 𝑐 = 𝑎 → ( 𝑐 ‘ 0 ) = ( 𝑎 ‘ 0 ) )
26	25	eqeq1d	⊢ ( 𝑐 = 𝑎 → ( ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ↔ ( 𝑎 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) )
27		fveq1	⊢ ( 𝑑 = 𝑏 → ( 𝑑 ‘ 0 ) = ( 𝑏 ‘ 0 ) )
28	27	eqeq2d	⊢ ( 𝑑 = 𝑏 → ( ( 𝑎 ‘ 0 ) = ( 𝑑 ‘ 0 ) ↔ ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
29	26 28	cbvrex2vw	⊢ ( ∃ 𝑐 ∈ ( ^◡ 𝑆 “ { 𝑖 } ) ∃ 𝑑 ∈ ( ^◡ 𝑆 “ { 𝑗 } ) ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ↔ ∃ 𝑎 ∈ ( ^◡ 𝑆 “ { 𝑖 } ) ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝑗 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) )
30		sneq	⊢ ( 𝑖 = 𝐴 → { 𝑖 } = { 𝐴 } )
31	30	imaeq2d	⊢ ( 𝑖 = 𝐴 → ( ^◡ 𝑆 “ { 𝑖 } ) = ( ^◡ 𝑆 “ { 𝐴 } ) )
32	31	rexeqdv	⊢ ( 𝑖 = 𝐴 → ( ∃ 𝑎 ∈ ( ^◡ 𝑆 “ { 𝑖 } ) ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝑗 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ∃ 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝑗 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
33	29 32	bitrid	⊢ ( 𝑖 = 𝐴 → ( ∃ 𝑐 ∈ ( ^◡ 𝑆 “ { 𝑖 } ) ∃ 𝑑 ∈ ( ^◡ 𝑆 “ { 𝑗 } ) ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ↔ ∃ 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝑗 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
34		sneq	⊢ ( 𝑗 = 𝐵 → { 𝑗 } = { 𝐵 } )
35	34	imaeq2d	⊢ ( 𝑗 = 𝐵 → ( ^◡ 𝑆 “ { 𝑗 } ) = ( ^◡ 𝑆 “ { 𝐵 } ) )
36	35	rexeqdv	⊢ ( 𝑗 = 𝐵 → ( ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝑗 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝐵 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
37	36	rexbidv	⊢ ( 𝑗 = 𝐵 → ( ∃ 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝑗 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ∃ 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝐵 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
38	33 37 7	brabg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 𝐿 𝐵 ↔ ∃ 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝐵 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
39	8 24 38	pm5.21nii	⊢ ( 𝐴 𝐿 𝐵 ↔ ∃ 𝑎 ∈ ( ^◡ 𝑆 “ { 𝐴 } ) ∃ 𝑏 ∈ ( ^◡ 𝑆 “ { 𝐵 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) )

Metamath Proof Explorer

Theorem efgrelexlema

Proof