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

Metamath Proof Explorer

Theorem s1co

Description: Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s1co ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ⟨“ 𝑆 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ )

Proof

Step Hyp Ref Expression
1 s1val ⊢ ( 𝑆 ∈ 𝐴 → ⟨“ 𝑆 ”⟩ = { ⟨ 0 , 𝑆 ⟩ } )
2 0cn ⊢ 0 ∈ ℂ
3 xpsng ⊢ ( ( 0 ∈ ℂ ∧ 𝑆 ∈ 𝐴 ) → ( { 0 } × { 𝑆 } ) = { ⟨ 0 , 𝑆 ⟩ } )
4 2 3 mpan ⊢ ( 𝑆 ∈ 𝐴 → ( { 0 } × { 𝑆 } ) = { ⟨ 0 , 𝑆 ⟩ } )
5 1 4 eqtr4d ⊢ ( 𝑆 ∈ 𝐴 → ⟨“ 𝑆 ”⟩ = ( { 0 } × { 𝑆 } ) )
6 5 adantr ⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ⟨“ 𝑆 ”⟩ = ( { 0 } × { 𝑆 } ) )
7 6 coeq2d ⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ⟨“ 𝑆 ”⟩ ) = ( 𝐹 ∘ ( { 0 } × { 𝑆 } ) ) )
8 fvex ⊢ ( 𝐹 ‘ 𝑆 ) ∈ V
9 s1val ⊢ ( ( 𝐹 ‘ 𝑆 ) ∈ V → ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ = { ⟨ 0 , ( 𝐹 ‘ 𝑆 ) ⟩ } )
10 8 9 ax-mp ⊢ ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ = { ⟨ 0 , ( 𝐹 ‘ 𝑆 ) ⟩ }
11 c0ex ⊢ 0 ∈ V
12 11 8 xpsn ⊢ ( { 0 } × { ( 𝐹 ‘ 𝑆 ) } ) = { ⟨ 0 , ( 𝐹 ‘ 𝑆 ) ⟩ }
13 10 12 eqtr4i ⊢ ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ = ( { 0 } × { ( 𝐹 ‘ 𝑆 ) } )
14 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
15 id ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ 𝐴 )
16 fcoconst ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝐹 ∘ ( { 0 } × { 𝑆 } ) ) = ( { 0 } × { ( 𝐹 ‘ 𝑆 ) } ) )
17 14 15 16 syl2anr ⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( { 0 } × { 𝑆 } ) ) = ( { 0 } × { ( 𝐹 ‘ 𝑆 ) } ) )
18 13 17 eqtr4id ⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ = ( 𝐹 ∘ ( { 0 } × { 𝑆 } ) ) )
19 7 18 eqtr4d ⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ⟨“ 𝑆 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝑆 ) ”⟩ )