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 eqtrid ⊢ ( 𝜑 → 𝑊 = 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 ⊢ ( 𝜑 → 𝐴 = 𝐵 )