counop

Description: The composition of two unitary operators is unitary. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	counop	$⊢ (S \in UniOp \land T \in UniOp) \to S \circ T \in UniOp$

Proof

Step	Hyp	Ref	Expression
1		unopf1o	$⊢ S \in UniOp \to S : ℋ \underset{1-1 onto}{⟶} ℋ$
2		unopf1o	$⊢ T \in UniOp \to T : ℋ \underset{1-1 onto}{⟶} ℋ$
3		f1oco	$⊢ (S : ℋ \underset{1-1 onto}{⟶} ℋ \land T : ℋ \underset{1-1 onto}{⟶} ℋ) \to (S \circ T) : ℋ \underset{1-1 onto}{⟶} ℋ$
4	1 2 3	syl2an	$⊢ (S \in UniOp \land T \in UniOp) \to (S \circ T) : ℋ \underset{1-1 onto}{⟶} ℋ$
5		f1ofo	$⊢ (S \circ T) : ℋ \underset{1-1 onto}{⟶} ℋ \to (S \circ T) : ℋ \underset{onto}{⟶} ℋ$
6	4 5	syl	$⊢ (S \in UniOp \land T \in UniOp) \to (S \circ T) : ℋ \underset{onto}{⟶} ℋ$
7		f1of	$⊢ T : ℋ \underset{1-1 onto}{⟶} ℋ \to T : ℋ ⟶ ℋ$
8	2 7	syl	$⊢ T \in UniOp \to T : ℋ ⟶ ℋ$
9	8	adantl	$⊢ (S \in UniOp \land T \in UniOp) \to T : ℋ ⟶ ℋ$
10		simpl	$⊢ (x \in ℋ \land y \in ℋ) \to x \in ℋ$
11		fvco3	$⊢ (T : ℋ ⟶ ℋ \land x \in ℋ) \to (S \circ T) (x) = S (T (x))$
12	9 10 11	syl2an	$⊢ ((S \in UniOp \land T \in UniOp) \land (x \in ℋ \land y \in ℋ)) \to (S \circ T) (x) = S (T (x))$
13		simpr	$⊢ (x \in ℋ \land y \in ℋ) \to y \in ℋ$
14		fvco3	$⊢ (T : ℋ ⟶ ℋ \land y \in ℋ) \to (S \circ T) (y) = S (T (y))$
15	9 13 14	syl2an	$⊢ ((S \in UniOp \land T \in UniOp) \land (x \in ℋ \land y \in ℋ)) \to (S \circ T) (y) = S (T (y))$
16	12 15	oveq12d	$⊢ ((S \in UniOp \land T \in UniOp) \land (x \in ℋ \land y \in ℋ)) \to (S \circ T) (x) \cdot_{ih} (S \circ T) (y) = S (T (x)) \cdot_{ih} S (T (y))$
17		ffvelrn	$⊢ (T : ℋ ⟶ ℋ \land x \in ℋ) \to T (x) \in ℋ$
18		ffvelrn	$⊢ (T : ℋ ⟶ ℋ \land y \in ℋ) \to T (y) \in ℋ$
19	17 18	anim12dan	$⊢ (T : ℋ ⟶ ℋ \land (x \in ℋ \land y \in ℋ)) \to (T (x) \in ℋ \land T (y) \in ℋ)$
20	8 19	sylan	$⊢ (T \in UniOp \land (x \in ℋ \land y \in ℋ)) \to (T (x) \in ℋ \land T (y) \in ℋ)$
21		unop	$⊢ (S \in UniOp \land T (x) \in ℋ \land T (y) \in ℋ) \to S (T (x)) \cdot_{ih} S (T (y)) = T (x) \cdot_{ih} T (y)$
22	21	3expb	$⊢ (S \in UniOp \land (T (x) \in ℋ \land T (y) \in ℋ)) \to S (T (x)) \cdot_{ih} S (T (y)) = T (x) \cdot_{ih} T (y)$
23	20 22	sylan2	$⊢ (S \in UniOp \land (T \in UniOp \land (x \in ℋ \land y \in ℋ))) \to S (T (x)) \cdot_{ih} S (T (y)) = T (x) \cdot_{ih} T (y)$
24	23	anassrs	$⊢ ((S \in UniOp \land T \in UniOp) \land (x \in ℋ \land y \in ℋ)) \to S (T (x)) \cdot_{ih} S (T (y)) = T (x) \cdot_{ih} T (y)$
25		unop	$⊢ (T \in UniOp \land x \in ℋ \land y \in ℋ) \to T (x) \cdot_{ih} T (y) = x \cdot_{ih} y$
26	25	3expb	$⊢ (T \in UniOp \land (x \in ℋ \land y \in ℋ)) \to T (x) \cdot_{ih} T (y) = x \cdot_{ih} y$
27	26	adantll	$⊢ ((S \in UniOp \land T \in UniOp) \land (x \in ℋ \land y \in ℋ)) \to T (x) \cdot_{ih} T (y) = x \cdot_{ih} y$
28	16 24 27	3eqtrd	$⊢ ((S \in UniOp \land T \in UniOp) \land (x \in ℋ \land y \in ℋ)) \to (S \circ T) (x) \cdot_{ih} (S \circ T) (y) = x \cdot_{ih} y$
29	28	ralrimivva	$⊢ (S \in UniOp \land T \in UniOp) \to \forall x \in ℋ \forall y \in ℋ (S \circ T) (x) \cdot_{ih} (S \circ T) (y) = x \cdot_{ih} y$
30		elunop	$⊢ S \circ T \in UniOp \leftrightarrow ((S \circ T) : ℋ \underset{onto}{⟶} ℋ \land \forall x \in ℋ \forall y \in ℋ (S \circ T) (x) \cdot_{ih} (S \circ T) (y) = x \cdot_{ih} y)$
31	6 29 30	sylanbrc	$⊢ (S \in UniOp \land T \in UniOp) \to S \circ T \in UniOp$

Metamath Proof Explorer

Theorem counop

Proof