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 ( ( 𝑆𝐴𝐹 : 𝐴𝐵 ) → ( 𝐹 ∘ ⟨“ 𝑆 ”⟩ ) = ⟨“ ( 𝐹𝑆 ) ”⟩ )