adjadd

Description: The adjoint of the sum of two operators. Theorem 3.11(iii) of Beran p. 106. (Contributed by NM, 22-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	adjadd	$⊢ (S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \to {adj}_{h} (S +_{op} T) = {adj}_{h} (S) +_{op} {adj}_{h} (T)$

Proof

Step	Hyp	Ref	Expression
1		dmadjop	$⊢ S \in dom {adj}_{h} \to S : ℋ ⟶ ℋ$
2		dmadjop	$⊢ T \in dom {adj}_{h} \to T : ℋ ⟶ ℋ$
3		hoaddcl	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (S +_{op} T) : ℋ ⟶ ℋ$
4	1 2 3	syl2an	$⊢ (S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \to (S +_{op} T) : ℋ ⟶ ℋ$
5		dmadjrn	$⊢ S \in dom {adj}_{h} \to {adj}_{h} (S) \in dom {adj}_{h}$
6		dmadjop	$⊢ {adj}_{h} (S) \in dom {adj}_{h} \to {adj}_{h} (S) : ℋ ⟶ ℋ$
7	5 6	syl	$⊢ S \in dom {adj}_{h} \to {adj}_{h} (S) : ℋ ⟶ ℋ$
8		dmadjrn	$⊢ T \in dom {adj}_{h} \to {adj}_{h} (T) \in dom {adj}_{h}$
9		dmadjop	$⊢ {adj}_{h} (T) \in dom {adj}_{h} \to {adj}_{h} (T) : ℋ ⟶ ℋ$
10	8 9	syl	$⊢ T \in dom {adj}_{h} \to {adj}_{h} (T) : ℋ ⟶ ℋ$
11		hoaddcl	$⊢ ({adj}_{h} (S) : ℋ ⟶ ℋ \land {adj}_{h} (T) : ℋ ⟶ ℋ) \to ({adj}_{h} (S) +_{op} {adj}_{h} (T)) : ℋ ⟶ ℋ$
12	7 10 11	syl2an	$⊢ (S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \to ({adj}_{h} (S) +_{op} {adj}_{h} (T)) : ℋ ⟶ ℋ$
13		adj2	$⊢ (S \in dom {adj}_{h} \land x \in ℋ \land y \in ℋ) \to S (x) \cdot_{ih} y = x \cdot_{ih} {adj}_{h} (S) (y)$
14	13	3expb	$⊢ (S \in dom {adj}_{h} \land (x \in ℋ \land y \in ℋ)) \to S (x) \cdot_{ih} y = x \cdot_{ih} {adj}_{h} (S) (y)$
15	14	adantlr	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to S (x) \cdot_{ih} y = x \cdot_{ih} {adj}_{h} (S) (y)$
16		adj2	$⊢ (T \in dom {adj}_{h} \land x \in ℋ \land y \in ℋ) \to T (x) \cdot_{ih} y = x \cdot_{ih} {adj}_{h} (T) (y)$
17	16	3expb	$⊢ (T \in dom {adj}_{h} \land (x \in ℋ \land y \in ℋ)) \to T (x) \cdot_{ih} y = x \cdot_{ih} {adj}_{h} (T) (y)$
18	17	adantll	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to T (x) \cdot_{ih} y = x \cdot_{ih} {adj}_{h} (T) (y)$
19	15 18	oveq12d	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (S (x) \cdot_{ih} y) + (T (x) \cdot_{ih} y) = (x \cdot_{ih} {adj}_{h} (S) (y)) + (x \cdot_{ih} {adj}_{h} (T) (y))$
20	1	ffvelrnda	$⊢ (S \in dom {adj}_{h} \land x \in ℋ) \to S (x) \in ℋ$
21	20	ad2ant2r	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to S (x) \in ℋ$
22	2	ffvelrnda	$⊢ (T \in dom {adj}_{h} \land x \in ℋ) \to T (x) \in ℋ$
23	22	ad2ant2lr	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to T (x) \in ℋ$
24		simprr	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to y \in ℋ$
25		ax-his2	$⊢ (S (x) \in ℋ \land T (x) \in ℋ \land y \in ℋ) \to (S (x) +_{ℎ} T (x)) \cdot_{ih} y = (S (x) \cdot_{ih} y) + (T (x) \cdot_{ih} y)$
26	21 23 24 25	syl3anc	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (S (x) +_{ℎ} T (x)) \cdot_{ih} y = (S (x) \cdot_{ih} y) + (T (x) \cdot_{ih} y)$
27		simprl	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to x \in ℋ$
28		adjcl	$⊢ (S \in dom {adj}_{h} \land y \in ℋ) \to {adj}_{h} (S) (y) \in ℋ$
29	28	ad2ant2rl	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to {adj}_{h} (S) (y) \in ℋ$
30		adjcl	$⊢ (T \in dom {adj}_{h} \land y \in ℋ) \to {adj}_{h} (T) (y) \in ℋ$
31	30	ad2ant2l	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to {adj}_{h} (T) (y) \in ℋ$
32		his7	$⊢ (x \in ℋ \land {adj}_{h} (S) (y) \in ℋ \land {adj}_{h} (T) (y) \in ℋ) \to x \cdot_{ih} ({adj}_{h} (S) (y) +_{ℎ} {adj}_{h} (T) (y)) = (x \cdot_{ih} {adj}_{h} (S) (y)) + (x \cdot_{ih} {adj}_{h} (T) (y))$
33	27 29 31 32	syl3anc	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} ({adj}_{h} (S) (y) +_{ℎ} {adj}_{h} (T) (y)) = (x \cdot_{ih} {adj}_{h} (S) (y)) + (x \cdot_{ih} {adj}_{h} (T) (y))$
34	19 26 33	3eqtr4rd	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} ({adj}_{h} (S) (y) +_{ℎ} {adj}_{h} (T) (y)) = (S (x) +_{ℎ} T (x)) \cdot_{ih} y$
35	7 10	anim12i	$⊢ (S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \to ({adj}_{h} (S) : ℋ ⟶ ℋ \land {adj}_{h} (T) : ℋ ⟶ ℋ)$
36		hosval	$⊢ ({adj}_{h} (S) : ℋ ⟶ ℋ \land {adj}_{h} (T) : ℋ ⟶ ℋ \land y \in ℋ) \to ({adj}_{h} (S) +_{op} {adj}_{h} (T)) (y) = {adj}_{h} (S) (y) +_{ℎ} {adj}_{h} (T) (y)$
37	36	3expa	$⊢ (({adj}_{h} (S) : ℋ ⟶ ℋ \land {adj}_{h} (T) : ℋ ⟶ ℋ) \land y \in ℋ) \to ({adj}_{h} (S) +_{op} {adj}_{h} (T)) (y) = {adj}_{h} (S) (y) +_{ℎ} {adj}_{h} (T) (y)$
38	35 37	sylan	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land y \in ℋ) \to ({adj}_{h} (S) +_{op} {adj}_{h} (T)) (y) = {adj}_{h} (S) (y) +_{ℎ} {adj}_{h} (T) (y)$
39	38	adantrl	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to ({adj}_{h} (S) +_{op} {adj}_{h} (T)) (y) = {adj}_{h} (S) (y) +_{ℎ} {adj}_{h} (T) (y)$
40	39	oveq2d	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to x \cdot_{ih} ({adj}_{h} (S) +_{op} {adj}_{h} (T)) (y) = x \cdot_{ih} ({adj}_{h} (S) (y) +_{ℎ} {adj}_{h} (T) (y))$
41	1 2	anim12i	$⊢ (S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \to (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ)$
42		hosval	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land x \in ℋ) \to (S +_{op} T) (x) = S (x) +_{ℎ} T (x)$
43	42	3expa	$⊢ ((S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to (S +_{op} T) (x) = S (x) +_{ℎ} T (x)$
44	41 43	sylan	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land x \in ℋ) \to (S +_{op} T) (x) = S (x) +_{ℎ} T (x)$
45	44	adantrr	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (S +_{op} T) (x) = S (x) +_{ℎ} T (x)$
46	45	oveq1d	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (S +_{op} T) (x) \cdot_{ih} y = (S (x) +_{ℎ} T (x)) \cdot_{ih} y$
47	34 40 46	3eqtr4rd	$⊢ ((S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \land (x \in ℋ \land y \in ℋ)) \to (S +_{op} T) (x) \cdot_{ih} y = x \cdot_{ih} ({adj}_{h} (S) +_{op} {adj}_{h} (T)) (y)$
48	47	ralrimivva	$⊢ (S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \to \forall x \in ℋ \forall y \in ℋ (S +_{op} T) (x) \cdot_{ih} y = x \cdot_{ih} ({adj}_{h} (S) +_{op} {adj}_{h} (T)) (y)$
49		adjeq	$⊢ ((S +_{op} T) : ℋ ⟶ ℋ \land ({adj}_{h} (S) +_{op} {adj}_{h} (T)) : ℋ ⟶ ℋ \land \forall x \in ℋ \forall y \in ℋ (S +_{op} T) (x) \cdot_{ih} y = x \cdot_{ih} ({adj}_{h} (S) +_{op} {adj}_{h} (T)) (y)) \to {adj}_{h} (S +_{op} T) = {adj}_{h} (S) +_{op} {adj}_{h} (T)$
50	4 12 48 49	syl3anc	$⊢ (S \in dom {adj}_{h} \land T \in dom {adj}_{h}) \to {adj}_{h} (S +_{op} T) = {adj}_{h} (S) +_{op} {adj}_{h} (T)$

Metamath Proof Explorer

Theorem adjadd

Proof