frgpup3lem

Description: The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 28-Feb-2016)

	Ref	Expression
Hypotheses	frgpup.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
	frgpup.n	⊢ 𝑁 = ( inv_g ‘ 𝐻 )
	frgpup.t	⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
	frgpup.h	⊢ ( 𝜑 → 𝐻 ∈ Grp )
	frgpup.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	frgpup.a	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
	frgpup.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
	frgpup.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
	frgpup.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
	frgpup.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	frgpup.e	⊢ 𝐸 = ran ( 𝑔 ∈ 𝑊 ↦ ⟨ [ 𝑔 ] ∼ , ( 𝐻 Σ_g ( 𝑇 ∘ 𝑔 ) ) ⟩ )
	frgpup.u	⊢ 𝑈 = ( var_FGrp ‘ 𝐼 )
	frgpup3.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 GrpHom 𝐻 ) )
	frgpup3.e	⊢ ( 𝜑 → ( 𝐾 ∘ 𝑈 ) = 𝐹 )
Assertion	frgpup3lem	⊢ ( 𝜑 → 𝐾 = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		frgpup.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
2		frgpup.n	⊢ 𝑁 = ( inv_g ‘ 𝐻 )
3		frgpup.t	⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
4		frgpup.h	⊢ ( 𝜑 → 𝐻 ∈ Grp )
5		frgpup.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		frgpup.a	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
7		frgpup.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
8		frgpup.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
9		frgpup.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
10		frgpup.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
11		frgpup.e	⊢ 𝐸 = ran ( 𝑔 ∈ 𝑊 ↦ ⟨ [ 𝑔 ] ∼ , ( 𝐻 Σ_g ( 𝑇 ∘ 𝑔 ) ) ⟩ )
12		frgpup.u	⊢ 𝑈 = ( var_FGrp ‘ 𝐼 )
13		frgpup3.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 GrpHom 𝐻 ) )
14		frgpup3.e	⊢ ( 𝜑 → ( 𝐾 ∘ 𝑈 ) = 𝐹 )
15	10 1	ghmf	⊢ ( 𝐾 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐾 : 𝑋 ⟶ 𝐵 )
16		ffn	⊢ ( 𝐾 : 𝑋 ⟶ 𝐵 → 𝐾 Fn 𝑋 )
17	13 15 16	3syl	⊢ ( 𝜑 → 𝐾 Fn 𝑋 )
18	1 2 3 4 5 6 7 8 9 10 11	frgpup1	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐺 GrpHom 𝐻 ) )
19	10 1	ghmf	⊢ ( 𝐸 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐸 : 𝑋 ⟶ 𝐵 )
20		ffn	⊢ ( 𝐸 : 𝑋 ⟶ 𝐵 → 𝐸 Fn 𝑋 )
21	18 19 20	3syl	⊢ ( 𝜑 → 𝐸 Fn 𝑋 )
22		eqid	⊢ ( freeMnd ‘ ( 𝐼 × 2_o ) ) = ( freeMnd ‘ ( 𝐼 × 2_o ) )
23	9 22 8	frgpval	⊢ ( 𝐼 ∈ 𝑉 → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) /_s ∼ ) )
24	5 23	syl	⊢ ( 𝜑 → 𝐺 = ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) /_s ∼ ) )
25		2on	⊢ 2_o ∈ On
26		xpexg	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 2_o ∈ On ) → ( 𝐼 × 2_o ) ∈ V )
27	5 25 26	sylancl	⊢ ( 𝜑 → ( 𝐼 × 2_o ) ∈ V )
28		wrdexg	⊢ ( ( 𝐼 × 2_o ) ∈ V → Word ( 𝐼 × 2_o ) ∈ V )
29		fvi	⊢ ( Word ( 𝐼 × 2_o ) ∈ V → ( I ‘ Word ( 𝐼 × 2_o ) ) = Word ( 𝐼 × 2_o ) )
30	27 28 29	3syl	⊢ ( 𝜑 → ( I ‘ Word ( 𝐼 × 2_o ) ) = Word ( 𝐼 × 2_o ) )
31	7 30	syl5eq	⊢ ( 𝜑 → 𝑊 = Word ( 𝐼 × 2_o ) )
32		eqid	⊢ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) )
33	22 32	frmdbas	⊢ ( ( 𝐼 × 2_o ) ∈ V → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) = Word ( 𝐼 × 2_o ) )
34	27 33	syl	⊢ ( 𝜑 → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) = Word ( 𝐼 × 2_o ) )
35	31 34	eqtr4d	⊢ ( 𝜑 → 𝑊 = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) )
36	8	fvexi	⊢ ∼ ∈ V
37	36	a1i	⊢ ( 𝜑 → ∼ ∈ V )
38		fvexd	⊢ ( 𝜑 → ( freeMnd ‘ ( 𝐼 × 2_o ) ) ∈ V )
39	24 35 37 38	qusbas	⊢ ( 𝜑 → ( 𝑊 / ∼ ) = ( Base ‘ 𝐺 ) )
40	10 39	eqtr4id	⊢ ( 𝜑 → 𝑋 = ( 𝑊 / ∼ ) )
41		eqimss	⊢ ( 𝑋 = ( 𝑊 / ∼ ) → 𝑋 ⊆ ( 𝑊 / ∼ ) )
42	40 41	syl	⊢ ( 𝜑 → 𝑋 ⊆ ( 𝑊 / ∼ ) )
43	42	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑋 ) → 𝑎 ∈ ( 𝑊 / ∼ ) )
44		eqid	⊢ ( 𝑊 / ∼ ) = ( 𝑊 / ∼ )
45		fveq2	⊢ ( [ 𝑡 ] ∼ = 𝑎 → ( 𝐾 ‘ [ 𝑡 ] ∼ ) = ( 𝐾 ‘ 𝑎 ) )
46		fveq2	⊢ ( [ 𝑡 ] ∼ = 𝑎 → ( 𝐸 ‘ [ 𝑡 ] ∼ ) = ( 𝐸 ‘ 𝑎 ) )
47	45 46	eqeq12d	⊢ ( [ 𝑡 ] ∼ = 𝑎 → ( ( 𝐾 ‘ [ 𝑡 ] ∼ ) = ( 𝐸 ‘ [ 𝑡 ] ∼ ) ↔ ( 𝐾 ‘ 𝑎 ) = ( 𝐸 ‘ 𝑎 ) ) )
48		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝑡 ∈ 𝑊 )
49	31	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝑊 = Word ( 𝐼 × 2_o ) )
50	48 49	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝑡 ∈ Word ( 𝐼 × 2_o ) )
51		wrdf	⊢ ( 𝑡 ∈ Word ( 𝐼 × 2_o ) → 𝑡 : ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ⟶ ( 𝐼 × 2_o ) )
52	50 51	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝑡 : ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ⟶ ( 𝐼 × 2_o ) )
53	52	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ) → ( 𝑡 ‘ 𝑛 ) ∈ ( 𝐼 × 2_o ) )
54		elxp2	⊢ ( ( 𝑡 ‘ 𝑛 ) ∈ ( 𝐼 × 2_o ) ↔ ∃ 𝑖 ∈ 𝐼 ∃ 𝑗 ∈ 2_o ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ )
55	53 54	sylib	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ) → ∃ 𝑖 ∈ 𝐼 ∃ 𝑗 ∈ 2_o ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ )
56		fveq2	⊢ ( 𝑦 = 𝑖 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑖 ) )
57	56	fveq2d	⊢ ( 𝑦 = 𝑖 → ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) )
58	56 57	ifeq12d	⊢ ( 𝑦 = 𝑖 → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
59		eqeq1	⊢ ( 𝑧 = 𝑗 → ( 𝑧 = ∅ ↔ 𝑗 = ∅ ) )
60	59	ifbid	⊢ ( 𝑧 = 𝑗 → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
61		fvex	⊢ ( 𝐹 ‘ 𝑖 ) ∈ V
62		fvex	⊢ ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ V
63	61 62	ifex	⊢ if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∈ V
64	58 60 3 63	ovmpo	⊢ ( ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2_o ) → ( 𝑖 𝑇 𝑗 ) = if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
65	64	adantl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2_o ) ) → ( 𝑖 𝑇 𝑗 ) = if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
66		elpri	⊢ ( 𝑗 ∈ { ∅ , 1_o } → ( 𝑗 = ∅ ∨ 𝑗 = 1_o ) )
67		df2o3	⊢ 2_o = { ∅ , 1_o }
68	66 67	eleq2s	⊢ ( 𝑗 ∈ 2_o → ( 𝑗 = ∅ ∨ 𝑗 = 1_o ) )
69	14	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝐾 ∘ 𝑈 ) = 𝐹 )
70	69	fveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝐾 ∘ 𝑈 ) ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) )
71	8 12 9 10	vrgpf	⊢ ( 𝐼 ∈ 𝑉 → 𝑈 : 𝐼 ⟶ 𝑋 )
72	5 71	syl	⊢ ( 𝜑 → 𝑈 : 𝐼 ⟶ 𝑋 )
73		fvco3	⊢ ( ( 𝑈 : 𝐼 ⟶ 𝑋 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝐾 ∘ 𝑈 ) ‘ 𝑖 ) = ( 𝐾 ‘ ( 𝑈 ‘ 𝑖 ) ) )
74	72 73	sylan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝐾 ∘ 𝑈 ) ‘ 𝑖 ) = ( 𝐾 ‘ ( 𝑈 ‘ 𝑖 ) ) )
75	70 74	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑖 ) = ( 𝐾 ‘ ( 𝑈 ‘ 𝑖 ) ) )
76	75	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = ∅ ) → ( 𝐹 ‘ 𝑖 ) = ( 𝐾 ‘ ( 𝑈 ‘ 𝑖 ) ) )
77		iftrue	⊢ ( 𝑗 = ∅ → if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ 𝑖 ) )
78	77	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = ∅ ) → if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ 𝑖 ) )
79		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = ∅ ) → 𝑗 = ∅ )
80	79	opeq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = ∅ ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑖 , ∅ ⟩ )
81	80	s1eqd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = ∅ ) → ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ = ⟨“ ⟨ 𝑖 , ∅ ⟩ ”⟩ )
82	81	eceq1d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = ∅ ) → [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ = [ ⟨“ ⟨ 𝑖 , ∅ ⟩ ”⟩ ] ∼ )
83	8 12	vrgpval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑖 ) = [ ⟨“ ⟨ 𝑖 , ∅ ⟩ ”⟩ ] ∼ )
84	5 83	sylan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑖 ) = [ ⟨“ ⟨ 𝑖 , ∅ ⟩ ”⟩ ] ∼ )
85	84	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = ∅ ) → ( 𝑈 ‘ 𝑖 ) = [ ⟨“ ⟨ 𝑖 , ∅ ⟩ ”⟩ ] ∼ )
86	82 85	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = ∅ ) → [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ = ( 𝑈 ‘ 𝑖 ) )
87	86	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = ∅ ) → ( 𝐾 ‘ [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ ) = ( 𝐾 ‘ ( 𝑈 ‘ 𝑖 ) ) )
88	76 78 87	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = ∅ ) → if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ ) )
89	75	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) = ( 𝑁 ‘ ( 𝐾 ‘ ( 𝑈 ‘ 𝑖 ) ) ) )
90	72	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑈 ‘ 𝑖 ) ∈ 𝑋 )
91		eqid	⊢ ( inv_g ‘ 𝐺 ) = ( inv_g ‘ 𝐺 )
92	10 91 2	ghminv	⊢ ( ( 𝐾 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( 𝑈 ‘ 𝑖 ) ∈ 𝑋 ) → ( 𝐾 ‘ ( ( inv_g ‘ 𝐺 ) ‘ ( 𝑈 ‘ 𝑖 ) ) ) = ( 𝑁 ‘ ( 𝐾 ‘ ( 𝑈 ‘ 𝑖 ) ) ) )
93	13 90 92	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝐾 ‘ ( ( inv_g ‘ 𝐺 ) ‘ ( 𝑈 ‘ 𝑖 ) ) ) = ( 𝑁 ‘ ( 𝐾 ‘ ( 𝑈 ‘ 𝑖 ) ) ) )
94	89 93	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) = ( 𝐾 ‘ ( ( inv_g ‘ 𝐺 ) ‘ ( 𝑈 ‘ 𝑖 ) ) ) )
95	94	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) = ( 𝐾 ‘ ( ( inv_g ‘ 𝐺 ) ‘ ( 𝑈 ‘ 𝑖 ) ) ) )
96		1n0	⊢ 1_o ≠ ∅
97		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → 𝑗 = 1_o )
98	97	neeq1d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → ( 𝑗 ≠ ∅ ↔ 1_o ≠ ∅ ) )
99	96 98	mpbiri	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → 𝑗 ≠ ∅ )
100		ifnefalse	⊢ ( 𝑗 ≠ ∅ → if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) )
101	99 100	syl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) )
102	97	opeq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑖 , 1_o ⟩ )
103	102	s1eqd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ = ⟨“ ⟨ 𝑖 , 1_o ⟩ ”⟩ )
104	103	eceq1d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ = [ ⟨“ ⟨ 𝑖 , 1_o ⟩ ”⟩ ] ∼ )
105	8 12 9 91	vrgpinv	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑖 ∈ 𝐼 ) → ( ( inv_g ‘ 𝐺 ) ‘ ( 𝑈 ‘ 𝑖 ) ) = [ ⟨“ ⟨ 𝑖 , 1_o ⟩ ”⟩ ] ∼ )
106	5 105	sylan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( inv_g ‘ 𝐺 ) ‘ ( 𝑈 ‘ 𝑖 ) ) = [ ⟨“ ⟨ 𝑖 , 1_o ⟩ ”⟩ ] ∼ )
107	106	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → ( ( inv_g ‘ 𝐺 ) ‘ ( 𝑈 ‘ 𝑖 ) ) = [ ⟨“ ⟨ 𝑖 , 1_o ⟩ ”⟩ ] ∼ )
108	104 107	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ = ( ( inv_g ‘ 𝐺 ) ‘ ( 𝑈 ‘ 𝑖 ) ) )
109	108	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → ( 𝐾 ‘ [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ ) = ( 𝐾 ‘ ( ( inv_g ‘ 𝐺 ) ‘ ( 𝑈 ‘ 𝑖 ) ) ) )
110	95 101 109	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 = 1_o ) → if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ ) )
111	88 110	jaodan	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ( 𝑗 = ∅ ∨ 𝑗 = 1_o ) ) → if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ ) )
112	68 111	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 2_o ) → if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ ) )
113	112	anasss	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2_o ) ) → if ( 𝑗 = ∅ , ( 𝐹 ‘ 𝑖 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ ) )
114	65 113	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2_o ) ) → ( 𝑖 𝑇 𝑗 ) = ( 𝐾 ‘ [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ ) )
115		fveq2	⊢ ( ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑇 ‘ ( 𝑡 ‘ 𝑛 ) ) = ( 𝑇 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) )
116		df-ov	⊢ ( 𝑖 𝑇 𝑗 ) = ( 𝑇 ‘ ⟨ 𝑖 , 𝑗 ⟩ )
117	115 116	eqtr4di	⊢ ( ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑇 ‘ ( 𝑡 ‘ 𝑛 ) ) = ( 𝑖 𝑇 𝑗 ) )
118		s1eq	⊢ ( ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ → ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ = ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ )
119	118	eceq1d	⊢ ( ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ → [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ = [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ )
120	119	fveq2d	⊢ ( ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝐾 ‘ [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ) = ( 𝐾 ‘ [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ ) )
121	117 120	eqeq12d	⊢ ( ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ → ( ( 𝑇 ‘ ( 𝑡 ‘ 𝑛 ) ) = ( 𝐾 ‘ [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ) ↔ ( 𝑖 𝑇 𝑗 ) = ( 𝐾 ‘ [ ⟨“ ⟨ 𝑖 , 𝑗 ⟩ ”⟩ ] ∼ ) ) )
122	114 121	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2_o ) ) → ( ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑇 ‘ ( 𝑡 ‘ 𝑛 ) ) = ( 𝐾 ‘ [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ) ) )
123	122	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ 𝐼 ∃ 𝑗 ∈ 2_o ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑇 ‘ ( 𝑡 ‘ 𝑛 ) ) = ( 𝐾 ‘ [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ) ) )
124	123	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ) → ( ∃ 𝑖 ∈ 𝐼 ∃ 𝑗 ∈ 2_o ( 𝑡 ‘ 𝑛 ) = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑇 ‘ ( 𝑡 ‘ 𝑛 ) ) = ( 𝐾 ‘ [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ) ) )
125	55 124	mpd	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ) → ( 𝑇 ‘ ( 𝑡 ‘ 𝑛 ) ) = ( 𝐾 ‘ [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ) )
126	125	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ↦ ( 𝑇 ‘ ( 𝑡 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ↦ ( 𝐾 ‘ [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ) ) )
127	1 2 3 4 5 6	frgpuptf	⊢ ( 𝜑 → 𝑇 : ( 𝐼 × 2_o ) ⟶ 𝐵 )
128		fcompt	⊢ ( ( 𝑇 : ( 𝐼 × 2_o ) ⟶ 𝐵 ∧ 𝑡 : ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ⟶ ( 𝐼 × 2_o ) ) → ( 𝑇 ∘ 𝑡 ) = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ↦ ( 𝑇 ‘ ( 𝑡 ‘ 𝑛 ) ) ) )
129	127 52 128	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝑇 ∘ 𝑡 ) = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ↦ ( 𝑇 ‘ ( 𝑡 ‘ 𝑛 ) ) ) )
130	53	s1cld	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ) → ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ∈ Word ( 𝐼 × 2_o ) )
131	31	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ) → 𝑊 = Word ( 𝐼 × 2_o ) )
132	130 131	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ) → ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ∈ 𝑊 )
133	9 8 7 10	frgpeccl	⊢ ( ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ∈ 𝑊 → [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ∈ 𝑋 )
134	132 133	syl	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ) → [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ∈ 𝑋 )
135	52	feqmptd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝑡 = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ↦ ( 𝑡 ‘ 𝑛 ) ) )
136	5	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝐼 ∈ 𝑉 )
137	136 25 26	sylancl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝐼 × 2_o ) ∈ V )
138		eqid	⊢ ( var_FMnd ‘ ( 𝐼 × 2_o ) ) = ( var_FMnd ‘ ( 𝐼 × 2_o ) )
139	138	vrmdfval	⊢ ( ( 𝐼 × 2_o ) ∈ V → ( var_FMnd ‘ ( 𝐼 × 2_o ) ) = ( 𝑤 ∈ ( 𝐼 × 2_o ) ↦ ⟨“ 𝑤 ”⟩ ) )
140	137 139	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( var_FMnd ‘ ( 𝐼 × 2_o ) ) = ( 𝑤 ∈ ( 𝐼 × 2_o ) ↦ ⟨“ 𝑤 ”⟩ ) )
141		s1eq	⊢ ( 𝑤 = ( 𝑡 ‘ 𝑛 ) → ⟨“ 𝑤 ”⟩ = ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ )
142	53 135 140 141	fmptco	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ↦ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ) )
143		eqidd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) = ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) )
144		eceq1	⊢ ( 𝑤 = ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ → [ 𝑤 ] ∼ = [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ )
145	132 142 143 144	fmptco	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ↦ [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ) )
146	13	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝐾 ∈ ( 𝐺 GrpHom 𝐻 ) )
147	146 15	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝐾 : 𝑋 ⟶ 𝐵 )
148	147	feqmptd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝐾 = ( 𝑤 ∈ 𝑋 ↦ ( 𝐾 ‘ 𝑤 ) ) )
149		fveq2	⊢ ( 𝑤 = [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ → ( 𝐾 ‘ 𝑤 ) = ( 𝐾 ‘ [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ) )
150	134 145 148 149	fmptco	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝐾 ∘ ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ↦ ( 𝐾 ‘ [ ⟨“ ( 𝑡 ‘ 𝑛 ) ”⟩ ] ∼ ) ) )
151	126 129 150	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝑇 ∘ 𝑡 ) = ( 𝐾 ∘ ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) )
152	151	oveq2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝐻 Σ_g ( 𝑇 ∘ 𝑡 ) ) = ( 𝐻 Σ_g ( 𝐾 ∘ ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) ) )
153	1 2 3 4 5 6 7 8 9 10 11	frgpupval	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝐸 ‘ [ 𝑡 ] ∼ ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑡 ) ) )
154		ghmmhm	⊢ ( 𝐾 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
155	146 154	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) )
156	138	vrmdf	⊢ ( ( 𝐼 × 2_o ) ∈ V → ( var_FMnd ‘ ( 𝐼 × 2_o ) ) : ( 𝐼 × 2_o ) ⟶ Word ( 𝐼 × 2_o ) )
157	137 156	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( var_FMnd ‘ ( 𝐼 × 2_o ) ) : ( 𝐼 × 2_o ) ⟶ Word ( 𝐼 × 2_o ) )
158	49	feq3d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) : ( 𝐼 × 2_o ) ⟶ 𝑊 ↔ ( var_FMnd ‘ ( 𝐼 × 2_o ) ) : ( 𝐼 × 2_o ) ⟶ Word ( 𝐼 × 2_o ) ) )
159	157 158	mpbird	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( var_FMnd ‘ ( 𝐼 × 2_o ) ) : ( 𝐼 × 2_o ) ⟶ 𝑊 )
160		wrdco	⊢ ( ( 𝑡 ∈ Word ( 𝐼 × 2_o ) ∧ ( var_FMnd ‘ ( 𝐼 × 2_o ) ) : ( 𝐼 × 2_o ) ⟶ 𝑊 ) → ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ∈ Word 𝑊 )
161	50 159 160	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ∈ Word 𝑊 )
162	35	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝑊 = ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) )
163	162	mpteq1d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) = ( 𝑤 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) ↦ [ 𝑤 ] ∼ ) )
164		eqid	⊢ ( 𝑤 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) ↦ [ 𝑤 ] ∼ ) = ( 𝑤 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) ↦ [ 𝑤 ] ∼ )
165	22 32 9 8 164	frgpmhm	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑤 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) ↦ [ 𝑤 ] ∼ ) ∈ ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) MndHom 𝐺 ) )
166	136 165	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝑤 ∈ ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) ↦ [ 𝑤 ] ∼ ) ∈ ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) MndHom 𝐺 ) )
167	163 166	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∈ ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) MndHom 𝐺 ) )
168	32 10	mhmf	⊢ ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∈ ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) MndHom 𝐺 ) → ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) : ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) ⟶ 𝑋 )
169	167 168	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) : ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) ⟶ 𝑋 )
170	162	feq2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) : 𝑊 ⟶ 𝑋 ↔ ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) : ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) ⟶ 𝑋 ) )
171	169 170	mpbird	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) : 𝑊 ⟶ 𝑋 )
172		wrdco	⊢ ( ( ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ∈ Word 𝑊 ∧ ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) : 𝑊 ⟶ 𝑋 ) → ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ∈ Word 𝑋 )
173	161 171 172	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ∈ Word 𝑋 )
174	10	gsumwmhm	⊢ ( ( 𝐾 ∈ ( 𝐺 MndHom 𝐻 ) ∧ ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ∈ Word 𝑋 ) → ( 𝐾 ‘ ( 𝐺 Σ_g ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) ) = ( 𝐻 Σ_g ( 𝐾 ∘ ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) ) )
175	155 173 174	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝐾 ‘ ( 𝐺 Σ_g ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) ) = ( 𝐻 Σ_g ( 𝐾 ∘ ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) ) )
176	152 153 175	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝐸 ‘ [ 𝑡 ] ∼ ) = ( 𝐾 ‘ ( 𝐺 Σ_g ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) ) )
177	22 138	frmdgsum	⊢ ( ( ( 𝐼 × 2_o ) ∈ V ∧ 𝑡 ∈ Word ( 𝐼 × 2_o ) ) → ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) Σ_g ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) = 𝑡 )
178	27 50 177	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) Σ_g ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) = 𝑡 )
179	178	fveq2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ‘ ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) Σ_g ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) = ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ‘ 𝑡 ) )
180		wrdco	⊢ ( ( 𝑡 ∈ Word ( 𝐼 × 2_o ) ∧ ( var_FMnd ‘ ( 𝐼 × 2_o ) ) : ( 𝐼 × 2_o ) ⟶ Word ( 𝐼 × 2_o ) ) → ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ∈ Word Word ( 𝐼 × 2_o ) )
181	50 157 180	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ∈ Word Word ( 𝐼 × 2_o ) )
182	34	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) = Word ( 𝐼 × 2_o ) )
183		wrdeq	⊢ ( ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) = Word ( 𝐼 × 2_o ) → Word ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) = Word Word ( 𝐼 × 2_o ) )
184	182 183	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → Word ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) = Word Word ( 𝐼 × 2_o ) )
185	181 184	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ∈ Word ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) )
186	32	gsumwmhm	⊢ ( ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∈ ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) MndHom 𝐺 ) ∧ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ∈ Word ( Base ‘ ( freeMnd ‘ ( 𝐼 × 2_o ) ) ) ) → ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ‘ ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) Σ_g ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) = ( 𝐺 Σ_g ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) )
187	167 185 186	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ‘ ( ( freeMnd ‘ ( 𝐼 × 2_o ) ) Σ_g ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) = ( 𝐺 Σ_g ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) )
188	7 8	efger	⊢ ∼ Er 𝑊
189	188	a1i	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ∼ Er 𝑊 )
190	7	fvexi	⊢ 𝑊 ∈ V
191	190	a1i	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → 𝑊 ∈ V )
192		eqid	⊢ ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) = ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ )
193	189 191 192	divsfval	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ‘ 𝑡 ) = [ 𝑡 ] ∼ )
194	179 187 193	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝐺 Σ_g ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) = [ 𝑡 ] ∼ )
195	194	fveq2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝐾 ‘ ( 𝐺 Σ_g ( ( 𝑤 ∈ 𝑊 ↦ [ 𝑤 ] ∼ ) ∘ ( ( var_FMnd ‘ ( 𝐼 × 2_o ) ) ∘ 𝑡 ) ) ) ) = ( 𝐾 ‘ [ 𝑡 ] ∼ ) )
196	176 195	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑊 ) → ( 𝐾 ‘ [ 𝑡 ] ∼ ) = ( 𝐸 ‘ [ 𝑡 ] ∼ ) )
197	44 47 196	ectocld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑊 / ∼ ) ) → ( 𝐾 ‘ 𝑎 ) = ( 𝐸 ‘ 𝑎 ) )
198	43 197	syldan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑋 ) → ( 𝐾 ‘ 𝑎 ) = ( 𝐸 ‘ 𝑎 ) )
199	17 21 198	eqfnfvd	⊢ ( 𝜑 → 𝐾 = 𝐸 )

Metamath Proof Explorer

Theorem frgpup3lem

Proof