ofcs1

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

		Ref	Expression
	Assertion	ofcs1	$⊢ (A \in S \land B \in T) \to ⟨“ A ”⟩ \circ_{fc} R B = ⟨“ (A R B) ”⟩$

Step	Hyp	Ref	Expression
1		snex	$⊢ \{0\} \in V$
2	1	a1i	$⊢ (A \in S \land B \in T) \to \{0\} \in V$
3		simpr	$⊢ (A \in S \land B \in T) \to B \in T$
4		simpll	$⊢ ((A \in S \land B \in T) \land i \in \{0\}) \to A \in S$
5		s1val	$⊢ A \in S \to ⟨“ A ”⟩ = \{⟨0, A⟩\}$
6		0nn0	$⊢ 0 \in ℕ_{0}$
7		fmptsn	$⊢ (0 \in ℕ_{0} \land A \in S) \to \{⟨0, A⟩\} = (i \in \{0\} ⟼ A)$
8	6 7	mpan	$⊢ A \in S \to \{⟨0, A⟩\} = (i \in \{0\} ⟼ A)$
9	5 8	eqtrd	$⊢ A \in S \to ⟨“ A ”⟩ = (i \in \{0\} ⟼ A)$
10	9	adantr	$⊢ (A \in S \land B \in T) \to ⟨“ A ”⟩ = (i \in \{0\} ⟼ A)$
11	2 3 4 10	ofcfval2	$⊢ (A \in S \land B \in T) \to ⟨“ A ”⟩ \circ_{fc} R B = (i \in \{0\} ⟼ A R B)$
12		ovex	$⊢ A R B \in V$
13		s1val	$⊢ A R B \in V \to ⟨“ (A R B) ”⟩ = \{⟨0, A R B⟩\}$
14	12 13	ax-mp	$⊢ ⟨“ (A R B) ”⟩ = \{⟨0, A R B⟩\}$
15		fmptsn	$⊢ (0 \in ℕ_{0} \land A R B \in V) \to \{⟨0, A R B⟩\} = (i \in \{0\} ⟼ A R B)$
16	6 12 15	mp2an	$⊢ \{⟨0, A R B⟩\} = (i \in \{0\} ⟼ A R B)$
17	14 16	eqtri	$⊢ ⟨“ (A R B) ”⟩ = (i \in \{0\} ⟼ A R B)$
18	11 17	eqtr4di	$⊢ (A \in S \land B \in T) \to ⟨“ A ”⟩ \circ_{fc} R B = ⟨“ (A R B) ”⟩$

Metamath Proof Explorer