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 

ovexd 
⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑊 ) → ( 𝐻 Σ_{g} ( 𝑇 ∘ 𝑔 ) ) ∈ V ) 
13 
7 8

efger 
⊢ ∼ Er 𝑊 
14 
13

a1i 
⊢ ( 𝜑 → ∼ Er 𝑊 ) 
15 
7

fvexi 
⊢ 𝑊 ∈ V 
16 
15

a1i 
⊢ ( 𝜑 → 𝑊 ∈ V ) 
17 

coeq2 
⊢ ( 𝑔 = 𝐴 → ( 𝑇 ∘ 𝑔 ) = ( 𝑇 ∘ 𝐴 ) ) 
18 
17

oveq2d 
⊢ ( 𝑔 = 𝐴 → ( 𝐻 Σ_{g} ( 𝑇 ∘ 𝑔 ) ) = ( 𝐻 Σ_{g} ( 𝑇 ∘ 𝐴 ) ) ) 
19 
1 2 3 4 5 6 7 8 9 10 11

frgpupf 
⊢ ( 𝜑 → 𝐸 : 𝑋 ⟶ 𝐵 ) 
20 
19

ffund 
⊢ ( 𝜑 → Fun 𝐸 ) 
21 
11 12 14 16 18 20

qliftval 
⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐸 ‘ [ 𝐴 ] ∼ ) = ( 𝐻 Σ_{g} ( 𝑇 ∘ 𝐴 ) ) ) 