ofs2

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

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

Proof

Step	Hyp	Ref	Expression
1		df-s2	$⊢ ⟨“ A B ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩$
2		df-s2	$⊢ ⟨“ C D ”⟩ = ⟨“ C ”⟩ ++ ⟨“ D ”⟩$
3	1 2	oveq12i	$⊢ ⟨“ A B ”⟩ R_{f} ⟨“ C D ”⟩ = (⟨“ A ”⟩ ++ ⟨“ B ”⟩) R_{f} (⟨“ C ”⟩ ++ ⟨“ D ”⟩)$
4		simpll	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to A \in S$
5	4	s1cld	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to ⟨“ A ”⟩ \in Word S$
6		simplr	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to B \in S$
7	6	s1cld	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to ⟨“ B ”⟩ \in Word S$
8		simprl	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to C \in T$
9	8	s1cld	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to ⟨“ C ”⟩ \in Word T$
10		simprr	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to D \in T$
11	10	s1cld	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to ⟨“ D ”⟩ \in Word T$
12		s1len	$⊢ \|⟨“ A ”⟩\| = 1$
13		s1len	$⊢ \|⟨“ C ”⟩\| = 1$
14	12 13	eqtr4i	$⊢ \|⟨“ A ”⟩\| = \|⟨“ C ”⟩\|$
15	14	a1i	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to \|⟨“ A ”⟩\| = \|⟨“ C ”⟩\|$
16		s1len	$⊢ \|⟨“ B ”⟩\| = 1$
17		s1len	$⊢ \|⟨“ D ”⟩\| = 1$
18	16 17	eqtr4i	$⊢ \|⟨“ B ”⟩\| = \|⟨“ D ”⟩\|$
19	18	a1i	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to \|⟨“ B ”⟩\| = \|⟨“ D ”⟩\|$
20	5 7 9 11 15 19	ofccat	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to (⟨“ A ”⟩ ++ ⟨“ B ”⟩) R_{f} (⟨“ C ”⟩ ++ ⟨“ D ”⟩) = (⟨“ A ”⟩ R_{f} ⟨“ C ”⟩) ++ (⟨“ B ”⟩ R_{f} ⟨“ D ”⟩)$
21	3 20	syl5eq	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to ⟨“ A B ”⟩ R_{f} ⟨“ C D ”⟩ = (⟨“ A ”⟩ R_{f} ⟨“ C ”⟩) ++ (⟨“ B ”⟩ R_{f} ⟨“ D ”⟩)$
22		ofs1	$⊢ (A \in S \land C \in T) \to ⟨“ A ”⟩ R_{f} ⟨“ C ”⟩ = ⟨“ (A R C) ”⟩$
23	4 8 22	syl2anc	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to ⟨“ A ”⟩ R_{f} ⟨“ C ”⟩ = ⟨“ (A R C) ”⟩$
24		ofs1	$⊢ (B \in S \land D \in T) \to ⟨“ B ”⟩ R_{f} ⟨“ D ”⟩ = ⟨“ (B R D) ”⟩$
25	6 10 24	syl2anc	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to ⟨“ B ”⟩ R_{f} ⟨“ D ”⟩ = ⟨“ (B R D) ”⟩$
26	23 25	oveq12d	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to (⟨“ A ”⟩ R_{f} ⟨“ C ”⟩) ++ (⟨“ B ”⟩ R_{f} ⟨“ D ”⟩) = ⟨“ (A R C) ”⟩ ++ ⟨“ (B R D) ”⟩$
27		df-s2	$⊢ ⟨“ (A R C) (B R D) ”⟩ = ⟨“ (A R C) ”⟩ ++ ⟨“ (B R D) ”⟩$
28	26 27	eqtr4di	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to (⟨“ A ”⟩ R_{f} ⟨“ C ”⟩) ++ (⟨“ B ”⟩ R_{f} ⟨“ D ”⟩) = ⟨“ (A R C) (B R D) ”⟩$
29	21 28	eqtrd	$⊢ ((A \in S \land B \in S) \land (C \in T \land D \in T)) \to ⟨“ A B ”⟩ R_{f} ⟨“ C D ”⟩ = ⟨“ (A R C) (B R D) ”⟩$

Metamath Proof Explorer

Theorem ofs2

Proof