Metamath Proof Explorer


Theorem frgpnabllem2

Description: Lemma for frgpnabl . (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 25-Apr-2024)

Ref Expression
Hypotheses frgpnabl.g 𝐺 = ( freeGrp ‘ 𝐼 )
frgpnabl.w 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
frgpnabl.r = ( ~FG𝐼 )
frgpnabl.p + = ( +g𝐺 )
frgpnabl.m 𝑀 = ( 𝑦𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ )
frgpnabl.t 𝑇 = ( 𝑣𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀𝑤 ) ”⟩ ⟩ ) ) )
frgpnabl.d 𝐷 = ( 𝑊 𝑥𝑊 ran ( 𝑇𝑥 ) )
frgpnabl.u 𝑈 = ( varFGrp𝐼 )
frgpnabl.i ( 𝜑𝐼𝑉 )
frgpnabl.a ( 𝜑𝐴𝐼 )
frgpnabl.b ( 𝜑𝐵𝐼 )
frgpnabl.n ( 𝜑 → ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) = ( ( 𝑈𝐵 ) + ( 𝑈𝐴 ) ) )
Assertion frgpnabllem2 ( 𝜑𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 frgpnabl.g 𝐺 = ( freeGrp ‘ 𝐼 )
2 frgpnabl.w 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
3 frgpnabl.r = ( ~FG𝐼 )
4 frgpnabl.p + = ( +g𝐺 )
5 frgpnabl.m 𝑀 = ( 𝑦𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ )
6 frgpnabl.t 𝑇 = ( 𝑣𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀𝑤 ) ”⟩ ⟩ ) ) )
7 frgpnabl.d 𝐷 = ( 𝑊 𝑥𝑊 ran ( 𝑇𝑥 ) )
8 frgpnabl.u 𝑈 = ( varFGrp𝐼 )
9 frgpnabl.i ( 𝜑𝐼𝑉 )
10 frgpnabl.a ( 𝜑𝐴𝐼 )
11 frgpnabl.b ( 𝜑𝐵𝐼 )
12 frgpnabl.n ( 𝜑 → ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) = ( ( 𝑈𝐵 ) + ( 𝑈𝐴 ) ) )
13 0ex ∅ ∈ V
14 13 a1i ( 𝜑 → ∅ ∈ V )
15 difss ( 𝑊 𝑥𝑊 ran ( 𝑇𝑥 ) ) ⊆ 𝑊
16 7 15 eqsstri 𝐷𝑊
17 1 2 3 4 5 6 7 8 9 11 10 frgpnabllem1 ( 𝜑 → ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ ( 𝐷 ∩ ( ( 𝑈𝐵 ) + ( 𝑈𝐴 ) ) ) )
18 17 elin1d ( 𝜑 → ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ 𝐷 )
19 16 18 sselid ( 𝜑 → ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ 𝑊 )
20 eqid ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) ) = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
21 2 3 5 6 7 20 efgredeu ( ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ 𝑊 → ∃! 𝑑𝐷 𝑑 ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ )
22 reurmo ( ∃! 𝑑𝐷 𝑑 ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ → ∃* 𝑑𝐷 𝑑 ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ )
23 19 21 22 3syl ( 𝜑 → ∃* 𝑑𝐷 𝑑 ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ )
24 1 2 3 4 5 6 7 8 9 10 11 frgpnabllem1 ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ( 𝐷 ∩ ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) ) )
25 24 elin1d ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ 𝐷 )
26 2 3 efger Er 𝑊
27 26 a1i ( 𝜑 Er 𝑊 )
28 1 frgpgrp ( 𝐼𝑉𝐺 ∈ Grp )
29 9 28 syl ( 𝜑𝐺 ∈ Grp )
30 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
31 3 8 1 30 vrgpf ( 𝐼𝑉𝑈 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
32 9 31 syl ( 𝜑𝑈 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
33 32 10 ffvelrnd ( 𝜑 → ( 𝑈𝐴 ) ∈ ( Base ‘ 𝐺 ) )
34 32 11 ffvelrnd ( 𝜑 → ( 𝑈𝐵 ) ∈ ( Base ‘ 𝐺 ) )
35 30 4 grpcl ( ( 𝐺 ∈ Grp ∧ ( 𝑈𝐴 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑈𝐵 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) ∈ ( Base ‘ 𝐺 ) )
36 29 33 34 35 syl3anc ( 𝜑 → ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) ∈ ( Base ‘ 𝐺 ) )
37 eqid ( freeMnd ‘ ( 𝐼 × 2o ) ) = ( freeMnd ‘ ( 𝐼 × 2o ) )
38 1 37 3 frgpval ( 𝐼𝑉𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ) )
39 9 38 syl ( 𝜑𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2o ) ) /s ) )
40 2on 2o ∈ On
41 xpexg ( ( 𝐼𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
42 9 40 41 sylancl ( 𝜑 → ( 𝐼 × 2o ) ∈ V )
43 wrdexg ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
44 fvi ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
45 42 43 44 3syl ( 𝜑 → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
46 2 45 syl5eq ( 𝜑𝑊 = Word ( 𝐼 × 2o ) )
47 eqid ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) )
48 37 47 frmdbas ( ( 𝐼 × 2o ) ∈ V → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
49 42 48 syl ( 𝜑 → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) = Word ( 𝐼 × 2o ) )
50 46 49 eqtr4d ( 𝜑𝑊 = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2o ) ) ) )
51 3 fvexi ∈ V
52 51 a1i ( 𝜑 ∈ V )
53 fvexd ( 𝜑 → ( freeMnd ‘ ( 𝐼 × 2o ) ) ∈ V )
54 39 50 52 53 qusbas ( 𝜑 → ( 𝑊 / ) = ( Base ‘ 𝐺 ) )
55 36 54 eleqtrrd ( 𝜑 → ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) ∈ ( 𝑊 / ) )
56 24 elin2d ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) )
57 qsel ( ( Er 𝑊 ∧ ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) ∈ ( 𝑊 / ) ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) ) → ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ] )
58 27 55 56 57 syl3anc ( 𝜑 → ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ] )
59 17 elin2d ( 𝜑 → ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ ( ( 𝑈𝐵 ) + ( 𝑈𝐴 ) ) )
60 59 12 eleqtrrd ( 𝜑 → ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) )
61 qsel ( ( Er 𝑊 ∧ ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) ∈ ( 𝑊 / ) ∧ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) ) → ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) = [ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] )
62 27 55 60 61 syl3anc ( 𝜑 → ( ( 𝑈𝐴 ) + ( 𝑈𝐵 ) ) = [ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] )
63 58 62 eqtr3d ( 𝜑 → [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ] = [ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] )
64 16 25 sselid ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ 𝑊 )
65 27 64 erth ( 𝜑 → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ↔ [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ] = [ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ) )
66 63 65 mpbird ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ )
67 27 19 erref ( 𝜑 → ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ )
68 breq1 ( 𝑑 = ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ → ( 𝑑 ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ↔ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) )
69 breq1 ( 𝑑 = ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ → ( 𝑑 ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ↔ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) )
70 68 69 rmoi ( ( ∃* 𝑑𝐷 𝑑 ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∧ ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ∈ 𝐷 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ∧ ( ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ 𝐷 ∧ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ )
71 23 25 66 18 67 70 syl122anc ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ = ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ )
72 71 fveq1d ( 𝜑 → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ‘ 0 ) = ( ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ‘ 0 ) )
73 opex 𝐴 , ∅ ⟩ ∈ V
74 s2fv0 ( ⟨ 𝐴 , ∅ ⟩ ∈ V → ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ‘ 0 ) = ⟨ 𝐴 , ∅ ⟩ )
75 73 74 ax-mp ( ⟨“ ⟨ 𝐴 , ∅ ⟩ ⟨ 𝐵 , ∅ ⟩ ”⟩ ‘ 0 ) = ⟨ 𝐴 , ∅ ⟩
76 opex 𝐵 , ∅ ⟩ ∈ V
77 s2fv0 ( ⟨ 𝐵 , ∅ ⟩ ∈ V → ( ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ‘ 0 ) = ⟨ 𝐵 , ∅ ⟩ )
78 76 77 ax-mp ( ⟨“ ⟨ 𝐵 , ∅ ⟩ ⟨ 𝐴 , ∅ ⟩ ”⟩ ‘ 0 ) = ⟨ 𝐵 , ∅ ⟩
79 72 75 78 3eqtr3g ( 𝜑 → ⟨ 𝐴 , ∅ ⟩ = ⟨ 𝐵 , ∅ ⟩ )
80 opthg ( ( 𝐴𝐼 ∧ ∅ ∈ V ) → ( ⟨ 𝐴 , ∅ ⟩ = ⟨ 𝐵 , ∅ ⟩ ↔ ( 𝐴 = 𝐵 ∧ ∅ = ∅ ) ) )
81 80 simprbda ( ( ( 𝐴𝐼 ∧ ∅ ∈ V ) ∧ ⟨ 𝐴 , ∅ ⟩ = ⟨ 𝐵 , ∅ ⟩ ) → 𝐴 = 𝐵 )
82 10 14 79 81 syl21anc ( 𝜑𝐴 = 𝐵 )