adj0

Description: Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	adj0	$⊢ {adj}_{h} (0_{hop}) = 0_{hop}$

Step	Hyp	Ref	Expression
1		ho0f	$⊢ 0_{hop} : ℋ ⟶ ℋ$
2		ho0val	$⊢ x \in ℋ \to 0_{hop} (x) = 0_{ℎ}$
3	2	oveq1d	$⊢ x \in ℋ \to 0_{hop} (x) \cdot_{ih} y = 0_{ℎ} \cdot_{ih} y$
4		hi01	$⊢ y \in ℋ \to 0_{ℎ} \cdot_{ih} y = 0$
5	3 4	sylan9eq	$⊢ (x \in ℋ \land y \in ℋ) \to 0_{hop} (x) \cdot_{ih} y = 0$
6		ho0val	$⊢ y \in ℋ \to 0_{hop} (y) = 0_{ℎ}$
7	6	oveq2d	$⊢ y \in ℋ \to x \cdot_{ih} 0_{hop} (y) = x \cdot_{ih} 0_{ℎ}$
8		hi02	$⊢ x \in ℋ \to x \cdot_{ih} 0_{ℎ} = 0$
9	7 8	sylan9eqr	$⊢ (x \in ℋ \land y \in ℋ) \to x \cdot_{ih} 0_{hop} (y) = 0$
10	5 9	eqtr4d	$⊢ (x \in ℋ \land y \in ℋ) \to 0_{hop} (x) \cdot_{ih} y = x \cdot_{ih} 0_{hop} (y)$
11	10	rgen2	$⊢ \forall x \in ℋ \forall y \in ℋ 0_{hop} (x) \cdot_{ih} y = x \cdot_{ih} 0_{hop} (y)$
12		adjeq	$⊢ (0_{hop} : ℋ ⟶ ℋ \land 0_{hop} : ℋ ⟶ ℋ \land \forall x \in ℋ \forall y \in ℋ 0_{hop} (x) \cdot_{ih} y = x \cdot_{ih} 0_{hop} (y)) \to {adj}_{h} (0_{hop}) = 0_{hop}$
13	1 1 11 12	mp3an	$⊢ {adj}_{h} (0_{hop}) = 0_{hop}$

Metamath Proof Explorer