Theorem vrgpinv

Description: The inverse of a generating element is represented by <. A , 1 >. instead of <. A , 0 >. . (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	vrgpfval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
	vrgpfval.u	⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
	vrgpf.m	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
	vrgpinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion	vrgpinv	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑈 ‘ 𝐴 ) ) = [ ⟨“ ⟨ 𝐴 , 1o ⟩ ”⟩ ] ∼ )

Proof

Step	Hyp	Ref	Expression
1		vrgpfval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
2		vrgpfval.u	⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
3		vrgpf.m	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
4		vrgpinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
5	1 2	vrgpval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )
6	5	fveq2d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑈 ‘ 𝐴 ) ) = ( 𝑁 ‘ [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ ) )
7		simpr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → 𝐴 ∈ 𝐼 )
8		0ex	⊢ ∅ ∈ V
9	8	prid1	⊢ ∅ ∈ { ∅ , 1o }
10		df2o3	⊢ 2o = { ∅ , 1o }
11	9 10	eleqtrri	⊢ ∅ ∈ 2o
12		opelxpi	⊢ ( ( 𝐴 ∈ 𝐼 ∧ ∅ ∈ 2o ) → ⟨ 𝐴 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
13	7 11 12	sylancl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ⟨ 𝐴 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
14	13	s1cld	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) )
15		simpl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → 𝐼 ∈ 𝑉 )
16		2on	⊢ 2o ∈ On
17		xpexg	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
18	15 16 17	sylancl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝐼 × 2o ) ∈ V )
19		wrdexg	⊢ ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
20		fvi	⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
21	18 19 20	3syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
22	14 21	eleqtrrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ ( I ‘ Word ( 𝐼 × 2o ) ) )
23		eqid	⊢ ( I ‘ Word ( 𝐼 × 2o ) ) = ( I ‘ Word ( 𝐼 × 2o ) )
24		eqid	⊢ ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) = ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ )
25	23 3 1 4 24	frgpinv	⊢ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ ( I ‘ Word ( 𝐼 × 2o ) ) → ( 𝑁 ‘ [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ ) = [ ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∘ ( reverse ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) ] ∼ )
26	22 25	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑁 ‘ [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ ) = [ ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∘ ( reverse ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) ] ∼ )
27		revs1	⊢ ( reverse ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) = ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩
28	27	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( reverse ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) = ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ )
29	28	coeq2d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∘ ( reverse ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) = ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) )
30	24	efgmf	⊢ ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
31		s1co	⊢ ( ( ⟨ 𝐴 , ∅ ⟩ ∈ ( 𝐼 × 2o ) ∧ ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) ) → ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) = ⟨“ ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ‘ ⟨ 𝐴 , ∅ ⟩ ) ”⟩ )
32	13 30 31	sylancl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) = ⟨“ ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ‘ ⟨ 𝐴 , ∅ ⟩ ) ”⟩ )
33	24	efgmval	⊢ ( ( 𝐴 ∈ 𝐼 ∧ ∅ ∈ 2o ) → ( 𝐴 ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∅ ) = ⟨ 𝐴 , ( 1o ∖ ∅ ) ⟩ )
34	7 11 33	sylancl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝐴 ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∅ ) = ⟨ 𝐴 , ( 1o ∖ ∅ ) ⟩ )
35		df-ov	⊢ ( 𝐴 ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∅ ) = ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ‘ ⟨ 𝐴 , ∅ ⟩ )
36		dif0	⊢ ( 1o ∖ ∅ ) = 1o
37	36	opeq2i	⊢ ⟨ 𝐴 , ( 1o ∖ ∅ ) ⟩ = ⟨ 𝐴 , 1o ⟩
38	34 35 37	3eqtr3g	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ‘ ⟨ 𝐴 , ∅ ⟩ ) = ⟨ 𝐴 , 1o ⟩ )
39	38	s1eqd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ⟨“ ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ‘ ⟨ 𝐴 , ∅ ⟩ ) ”⟩ = ⟨“ ⟨ 𝐴 , 1o ⟩ ”⟩ )
40	29 32 39	3eqtrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∘ ( reverse ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) = ⟨“ ⟨ 𝐴 , 1o ⟩ ”⟩ )
41	40	eceq1d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → [ ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 2o ↦ ⟨ 𝑥 , ( 1o ∖ 𝑦 ) ⟩ ) ∘ ( reverse ‘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) ] ∼ = [ ⟨“ ⟨ 𝐴 , 1o ⟩ ”⟩ ] ∼ )
42	6 26 41	3eqtrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑈 ‘ 𝐴 ) ) = [ ⟨“ ⟨ 𝐴 , 1o ⟩ ”⟩ ] ∼ )