Metamath Proof Explorer


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 I
vrgpfval.u U = var FGrp I
vrgpf.m G = freeGrp I
vrgpinv.n N = inv g G
Assertion vrgpinv I V A I N U A = ⟨“ A 1 𝑜 ”⟩ ˙

Proof

Step Hyp Ref Expression
1 vrgpfval.r ˙ = ~ FG I
2 vrgpfval.u U = var FGrp I
3 vrgpf.m G = freeGrp I
4 vrgpinv.n N = inv g G
5 1 2 vrgpval I V A I U A = ⟨“ A ”⟩ ˙
6 5 fveq2d I V A I N U A = N ⟨“ A ”⟩ ˙
7 simpr I V A I A I
8 0ex V
9 8 prid1 1 𝑜
10 df2o3 2 𝑜 = 1 𝑜
11 9 10 eleqtrri 2 𝑜
12 opelxpi A I 2 𝑜 A I × 2 𝑜
13 7 11 12 sylancl I V A I A I × 2 𝑜
14 13 s1cld I V A I ⟨“ A ”⟩ Word I × 2 𝑜
15 simpl I V A I I V
16 2on 2 𝑜 On
17 xpexg I V 2 𝑜 On I × 2 𝑜 V
18 15 16 17 sylancl I V A I I × 2 𝑜 V
19 wrdexg I × 2 𝑜 V Word I × 2 𝑜 V
20 fvi Word I × 2 𝑜 V I Word I × 2 𝑜 = Word I × 2 𝑜
21 18 19 20 3syl I V A I I Word I × 2 𝑜 = Word I × 2 𝑜
22 14 21 eleqtrrd I V A I ⟨“ A ”⟩ I Word I × 2 𝑜
23 eqid I Word I × 2 𝑜 = I Word I × 2 𝑜
24 eqid x I , y 2 𝑜 x 1 𝑜 y = x I , y 2 𝑜 x 1 𝑜 y
25 23 3 1 4 24 frgpinv ⟨“ A ”⟩ I Word I × 2 𝑜 N ⟨“ A ”⟩ ˙ = x I , y 2 𝑜 x 1 𝑜 y reverse ⟨“ A ”⟩ ˙
26 22 25 syl I V A I N ⟨“ A ”⟩ ˙ = x I , y 2 𝑜 x 1 𝑜 y reverse ⟨“ A ”⟩ ˙
27 revs1 reverse ⟨“ A ”⟩ = ⟨“ A ”⟩
28 27 a1i I V A I reverse ⟨“ A ”⟩ = ⟨“ A ”⟩
29 28 coeq2d I V A I x I , y 2 𝑜 x 1 𝑜 y reverse ⟨“ A ”⟩ = x I , y 2 𝑜 x 1 𝑜 y ⟨“ A ”⟩
30 24 efgmf x I , y 2 𝑜 x 1 𝑜 y : I × 2 𝑜 I × 2 𝑜
31 s1co A I × 2 𝑜 x I , y 2 𝑜 x 1 𝑜 y : I × 2 𝑜 I × 2 𝑜 x I , y 2 𝑜 x 1 𝑜 y ⟨“ A ”⟩ = ⟨“ x I , y 2 𝑜 x 1 𝑜 y A ”⟩
32 13 30 31 sylancl I V A I x I , y 2 𝑜 x 1 𝑜 y ⟨“ A ”⟩ = ⟨“ x I , y 2 𝑜 x 1 𝑜 y A ”⟩
33 24 efgmval A I 2 𝑜 A x I , y 2 𝑜 x 1 𝑜 y = A 1 𝑜
34 7 11 33 sylancl I V A I A x I , y 2 𝑜 x 1 𝑜 y = A 1 𝑜
35 df-ov A x I , y 2 𝑜 x 1 𝑜 y = x I , y 2 𝑜 x 1 𝑜 y A
36 dif0 1 𝑜 = 1 𝑜
37 36 opeq2i A 1 𝑜 = A 1 𝑜
38 34 35 37 3eqtr3g I V A I x I , y 2 𝑜 x 1 𝑜 y A = A 1 𝑜
39 38 s1eqd I V A I ⟨“ x I , y 2 𝑜 x 1 𝑜 y A ”⟩ = ⟨“ A 1 𝑜 ”⟩
40 29 32 39 3eqtrd I V A I x I , y 2 𝑜 x 1 𝑜 y reverse ⟨“ A ”⟩ = ⟨“ A 1 𝑜 ”⟩
41 40 eceq1d I V A I x I , y 2 𝑜 x 1 𝑜 y reverse ⟨“ A ”⟩ ˙ = ⟨“ A 1 𝑜 ”⟩ ˙
42 6 26 41 3eqtrd I V A I N U A = ⟨“ A 1 𝑜 ”⟩ ˙