ofs1

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

		Ref	Expression
	Assertion	ofs1	$⊢ (A \in S \land B \in T) \to ⟨“ A ”⟩ R_{f} ⟨“ B ”⟩ = ⟨“ (A R B) ”⟩$

Proof

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

Metamath Proof Explorer

Theorem ofs1

Proof