This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vrgpval

Description: The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses vrgpfval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
vrgpfval.u ⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
Assertion vrgpval ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )

Proof

Step Hyp Ref Expression
1 vrgpfval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
2 vrgpfval.u ⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
3 1 2 vrgpfval ⊢ ( 𝐼 ∈ 𝑉 → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) )
4 3 fveq1d ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑈 ‘ 𝐴 ) = ( ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) ‘ 𝐴 ) )
5 opeq1 ⊢ ( 𝑗 = 𝐴 → ⟨ 𝑗 , ∅ ⟩ = ⟨ 𝐴 , ∅ ⟩ )
6 5 s1eqd ⊢ ( 𝑗 = 𝐴 → ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ = ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ )
7 6 eceq1d ⊢ ( 𝑗 = 𝐴 → [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )
8 eqid ⊢ ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) = ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ )
9 1 fvexi ⊢ ∼ ∈ V
10 ecexg ⊢ ( ∼ ∈ V → [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ ∈ V )
11 9 10 ax-mp ⊢ [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ ∈ V
12 7 8 11 fvmpt ⊢ ( 𝐴 ∈ 𝐼 → ( ( 𝑗 ∈ 𝐼 ↦ [ ⟨“ ⟨ 𝑗 , ∅ ⟩ ”⟩ ] ∼ ) ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )
13 4 12 sylan9eq ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )