Metamath Proof Explorer

Theorem ofs1

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

Ref Expression
Assertion ofs1 ⊢ A ∈ S ∧ B ∈ T → ⟨“ A ”⟩ R f ⟨“ B ”⟩ = ⟨“ A R B ”⟩

Proof

Step Hyp Ref Expression
1 snex ⊢ 0 ∈ V
2 1 a1i ⊢ A ∈ S ∧ B ∈ T → 0 ∈ V
3 simpll ⊢ A ∈ S ∧ B ∈ T ∧ i ∈ 0 → A ∈ S
4 simplr ⊢ A ∈ S ∧ B ∈ T ∧ i ∈ 0 → B ∈ T
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 s1val ⊢ B ∈ T → ⟨“ B ”⟩ = 0 B
12 fmptsn ⊢ 0 ∈ ℕ 0 ∧ B ∈ T → 0 B = i ∈ 0 ⟼ B
13 6 12 mpan ⊢ B ∈ T → 0 B = i ∈ 0 ⟼ B
14 11 13 eqtrd ⊢ B ∈ T → ⟨“ B ”⟩ = i ∈ 0 ⟼ B
15 14 adantl ⊢ A ∈ S ∧ B ∈ T → ⟨“ B ”⟩ = i ∈ 0 ⟼ B
16 2 3 4 10 15 offval2 ⊢ A ∈ S ∧ B ∈ T → ⟨“ A ”⟩ R f ⟨“ B ”⟩ = i ∈ 0 ⟼ A R B
17 ovex ⊢ A R B ∈ V
18 s1val ⊢ A R B ∈ V → ⟨“ A R B ”⟩ = 0 A R B
19 17 18 ax-mp ⊢ ⟨“ A R B ”⟩ = 0 A R B
20 fmptsn ⊢ 0 ∈ ℕ 0 ∧ A R B ∈ V → 0 A R B = i ∈ 0 ⟼ A R B
21 6 17 20 mp2an ⊢ 0 A R B = i ∈ 0 ⟼ A R B
22 19 21 eqtri ⊢ ⟨“ A R B ”⟩ = i ∈ 0 ⟼ A R B
23 16 22 eqtr4di ⊢ A ∈ S ∧ B ∈ T → ⟨“ A ”⟩ R f ⟨“ B ”⟩ = ⟨“ A R B ”⟩