Metamath Proof Explorer

Theorem ofcs2

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

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

Proof

Step	Hyp	Ref	Expression
1		df-s2	$⊢ ⟨“ A B ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩$
2	1	oveq1i	$⊢ ⟨“ A B ”⟩ \circ_{fc} R C = (⟨“ A ”⟩ ++ ⟨“ B ”⟩) \circ_{fc} R C$
3		simp1	$⊢ (A \in S \land B \in S \land C \in T) \to A \in S$
4	3	s1cld	$⊢ (A \in S \land B \in S \land C \in T) \to ⟨“ A ”⟩ \in Word S$
5		simp2	$⊢ (A \in S \land B \in S \land C \in T) \to B \in S$
6	5	s1cld	$⊢ (A \in S \land B \in S \land C \in T) \to ⟨“ B ”⟩ \in Word S$
7		simp3	$⊢ (A \in S \land B \in S \land C \in T) \to C \in T$
8	4 6 7	ofcccat	$⊢ (A \in S \land B \in S \land C \in T) \to (⟨“ A ”⟩ ++ ⟨“ B ”⟩) \circ_{fc} R C = (⟨“ A ”⟩ \circ_{fc} R C) ++ (⟨“ B ”⟩ \circ_{fc} R C)$
9	2 8	eqtrid	$⊢ (A \in S \land B \in S \land C \in T) \to ⟨“ A B ”⟩ \circ_{fc} R C = (⟨“ A ”⟩ \circ_{fc} R C) ++ (⟨“ B ”⟩ \circ_{fc} R C)$
10		ofcs1	$⊢ (A \in S \land C \in T) \to ⟨“ A ”⟩ \circ_{fc} R C = ⟨“ (A R C) ”⟩$
11	3 7 10	syl2anc	$⊢ (A \in S \land B \in S \land C \in T) \to ⟨“ A ”⟩ \circ_{fc} R C = ⟨“ (A R C) ”⟩$
12		ofcs1	$⊢ (B \in S \land C \in T) \to ⟨“ B ”⟩ \circ_{fc} R C = ⟨“ (B R C) ”⟩$
13	5 7 12	syl2anc	$⊢ (A \in S \land B \in S \land C \in T) \to ⟨“ B ”⟩ \circ_{fc} R C = ⟨“ (B R C) ”⟩$
14	11 13	oveq12d	$⊢ (A \in S \land B \in S \land C \in T) \to (⟨“ A ”⟩ \circ_{fc} R C) ++ (⟨“ B ”⟩ \circ_{fc} R C) = ⟨“ (A R C) ”⟩ ++ ⟨“ (B R C) ”⟩$
15		df-s2	$⊢ ⟨“ (A R C) (B R C) ”⟩ = ⟨“ (A R C) ”⟩ ++ ⟨“ (B R C) ”⟩$
16	14 15	eqtr4di	$⊢ (A \in S \land B \in S \land C \in T) \to (⟨“ A ”⟩ \circ_{fc} R C) ++ (⟨“ B ”⟩ \circ_{fc} R C) = ⟨“ (A R C) (B R C) ”⟩$
17	9 16	eqtrd	$⊢ (A \in S \land B \in S \land C \in T) \to ⟨“ A B ”⟩ \circ_{fc} R C = ⟨“ (A R C) (B R C) ”⟩$