Metamath Proof Explorer

Theorem ofcs1

Description: Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018)

Ref Expression
Assertion ofcs1 ⊢ A ∈ S ∧ B ∈ T → ⟨“ A ”⟩ ∘ fc ⁡ R B = ⟨“ A R B ”⟩

Proof

Step Hyp Ref Expression
1 snex ⊢ 0 ∈ V
2 1 a1i ⊢ A ∈ S ∧ B ∈ T → 0 ∈ V
3 simpr ⊢ A ∈ S ∧ B ∈ T → B ∈ T
4 simpll ⊢ A ∈ S ∧ B ∈ T ∧ i ∈ 0 → A ∈ S
5 s1val ⊢ A ∈ S → ⟨“ A ”⟩ = 0 A
6 0nn0 ⊢ 0 ∈ ℕ 0
7 fmptsn ⊢ 0 ∈ ℕ 0 ∧ A ∈ S → 0 A = i ∈ 0 ⟼ A
8 6 7 mpan ⊢ A ∈ S → 0 A = i ∈ 0 ⟼ A
9 5 8 eqtrd ⊢ A ∈ S → ⟨“ A ”⟩ = i ∈ 0 ⟼ A
10 9 adantr ⊢ A ∈ S ∧ B ∈ T → ⟨“ A ”⟩ = i ∈ 0 ⟼ A
11 2 3 4 10 ofcfval2 ⊢ A ∈ S ∧ B ∈ T → ⟨“ A ”⟩ ∘ fc ⁡ R B = i ∈ 0 ⟼ A R B
12 ovex ⊢ A R B ∈ V
13 s1val ⊢ A R B ∈ V → ⟨“ A R B ”⟩ = 0 A R B
14 12 13 ax-mp ⊢ ⟨“ A R B ”⟩ = 0 A R B
15 fmptsn ⊢ 0 ∈ ℕ 0 ∧ A R B ∈ V → 0 A R B = i ∈ 0 ⟼ A R B
16 6 12 15 mp2an ⊢ 0 A R B = i ∈ 0 ⟼ A R B
17 14 16 eqtri ⊢ ⟨“ A R B ”⟩ = i ∈ 0 ⟼ A R B
18 11 17 eqtr4di ⊢ A ∈ S ∧ B ∈ T → ⟨“ A ”⟩ ∘ fc ⁡ R B = ⟨“ A R B ”⟩