Theorem lnophs 9926

Description: The sum of two linear operators is linear.

Hypotheses

Ref	Expression
lnopco.1	|- S e. LinOp
lnopco.2	|- T e. LinOp

Assertion

Ref	Expression
lnophs	|- (S +op T) e. LinOp

Proof of Theorem lnophs

Step	Hyp	Ref	Expression
1		ellnopt 9784	. 2 |- ((S +op T) e. LinOp <-> ((S +op T):H~-->H~ /\ A.x e. CC A.y e. H~ A.z e. H~ ((S +op T)` ((x .h y) +h z)) = ((x .h ((S +op T)` y)) +h ((S +op T)` z))))
2		lnopco.1	. . . 4 |- S e. LinOp
3	2	lnopf 9893	. . 3 |- S:H~-->H~
4		lnopco.2	. . . 4 |- T e. LinOp
5	4	lnopf 9893	. . 3 |- T:H~-->H~
6	3, 5	hoaddcl 9694	. 2 |- (S +op T):H~-->H~
7	2	lnopadd 9895	. . . . . . . 8 |- (((x .h y) e. H~ /\ z e. H~) -> (S` ((x .h y) +h z)) = ((S` (x .h y)) +h (S` z)))
8	4	lnopadd 9895	. . . . . . . 8 |- (((x .h y) e. H~ /\ z e. H~) -> (T` ((x .h y) +h z)) = ((T` (x .h y)) +h (T` z)))
9	7, 8	opreq12d 3978	. . . . . . 7 |- (((x .h y) e. H~ /\ z e. H~) -> ((S` ((x .h y) +h z)) +h (T` ((x .h y) +h z))) = (((S` (x .h y)) +h (S` z)) +h ((T` (x .h y)) +h (T` z))))
10		hvmulclt 8883	. . . . . . 7 |- ((x e. CC /\ y e. H~) -> (x .h y) e. H~)
11	9, 10	sylan 448	. . . . . 6 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((S` ((x .h y) +h z)) +h (T` ((x .h y) +h z))) = (((S` (x .h y)) +h (S` z)) +h ((T` (x .h y)) +h (T` z))))
12		hvadd4t 8905	. . . . . . 7 |- ((((S` (x .h y)) e. H~ /\ (S` z) e. H~) /\ ((T` (x .h y)) e. H~ /\ (T` z) e. H~)) -> (((S` (x .h y)) +h (S` z)) +h ((T` (x .h y)) +h (T` z))) = (((S` (x .h y)) +h (T` (x .h y))) +h ((S` z) +h (T` z))))
13	3	ffvelrni 3815	. . . . . . . . 9 |- ((x .h y) e. H~ -> (S` (x .h y)) e. H~)
14	10, 13	syl 10	. . . . . . . 8 |- ((x e. CC /\ y e. H~) -> (S` (x .h y)) e. H~)
15	3	ffvelrni 3815	. . . . . . . 8 |- (z e. H~ -> (S` z) e. H~)
16	14, 15	anim12i 333	. . . . . . 7 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((S` (x .h y)) e. H~ /\ (S` z) e. H~))
17	5	ffvelrni 3815	. . . . . . . . 9 |- ((x .h y) e. H~ -> (T` (x .h y)) e. H~)
18	10, 17	syl 10	. . . . . . . 8 |- ((x e. CC /\ y e. H~) -> (T` (x .h y)) e. H~)
19	5	ffvelrni 3815	. . . . . . . 8 |- (z e. H~ -> (T` z) e. H~)
20	18, 19	anim12i 333	. . . . . . 7 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((T` (x .h y)) e. H~ /\ (T` z) e. H~))
21	12, 16, 20	sylanc 471	. . . . . 6 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> (((S` (x .h y)) +h (S` z)) +h ((T` (x .h y)) +h (T` z))) = (((S` (x .h y)) +h (T` (x .h y))) +h ((S` z) +h (T` z))))
22	11, 21	eqtrd 1507	. . . . 5 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((S` ((x .h y) +h z)) +h (T` ((x .h y) +h z))) = (((S` (x .h y)) +h (T` (x .h y))) +h ((S` z) +h (T` z))))
23		hvaddclt 8882	. . . . . . 7 |- (((x .h y) e. H~ /\ z e. H~) -> ((x .h y) +h z) e. H~)
24	23, 10	sylan 448	. . . . . 6 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((x .h y) +h z) e. H~)
25		hosvaltOLD 9517	. . . . . . 7 |- (((S:H~-->H~ /\ T:H~-->H~) /\ ((x .h y) +h z) e. H~) -> ((S +op T)` ((x .h y) +h z)) = ((S` ((x .h y) +h z)) +h (T` ((x .h y) +h z))))
26	3, 5, 25	mpanl12 708	. . . . . 6 |- (((x .h y) +h z) e. H~ -> ((S +op T)` ((x .h y) +h z)) = ((S` ((x .h y) +h z)) +h (T` ((x .h y) +h z))))
27	24, 26	syl 10	. . . . 5 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((S +op T)` ((x .h y) +h z)) = ((S` ((x .h y) +h z)) +h (T` ((x .h y) +h z))))
28		ax-hvdistr1 8878	. . . . . . . . 9 |- ((x e. CC /\ (S` y) e. H~ /\ (T` y) e. H~) -> (x .h ((S` y) +h (T` y))) = ((x .h (S` y)) +h (x .h (T` y))))
29	28	3expb 834	. . . . . . . 8 |- ((x e. CC /\ ((S` y) e. H~ /\ (T` y) e. H~)) -> (x .h ((S` y) +h (T` y))) = ((x .h (S` y)) +h (x .h (T` y))))
30	3	ffvelrni 3815	. . . . . . . . 9 |- (y e. H~ -> (S` y) e. H~)
31	5	ffvelrni 3815	. . . . . . . . 9 |- (y e. H~ -> (T` y) e. H~)
32	30, 31	jca 288	. . . . . . . 8 |- (y e. H~ -> ((S` y) e. H~ /\ (T` y) e. H~))
33	29, 32	sylan2 451	. . . . . . 7 |- ((x e. CC /\ y e. H~) -> (x .h ((S` y) +h (T` y))) = ((x .h (S` y)) +h (x .h (T` y))))
34		hosvaltOLD 9517	. . . . . . . . . 10 |- (((S:H~-->H~ /\ T:H~-->H~) /\ y e. H~) -> ((S +op T)` y) = ((S` y) +h (T` y)))
35	3, 5, 34	mpanl12 708	. . . . . . . . 9 |- (y e. H~ -> ((S +op T)` y) = ((S` y) +h (T` y)))
36	35	opreq2d 3976	. . . . . . . 8 |- (y e. H~ -> (x .h ((S +op T)` y)) = (x .h ((S` y) +h (T` y))))
37	36	adantl 388	. . . . . . 7 |- ((x e. CC /\ y e. H~) -> (x .h ((S +op T)` y)) = (x .h ((S` y) +h (T` y))))
38	2	lnopmul 9896	. . . . . . . 8 |- ((x e. CC /\ y e. H~) -> (S` (x .h y)) = (x .h (S` y)))
39	4	lnopmul 9896	. . . . . . . 8 |- ((x e. CC /\ y e. H~) -> (T` (x .h y)) = (x .h (T` y)))
40	38, 39	opreq12d 3978	. . . . . . 7 |- ((x e. CC /\ y e. H~) -> ((S` (x .h y)) +h (T` (x .h y))) = ((x .h (S` y)) +h (x .h (T` y))))
41	33, 37, 40	3eqtr4d 1517	. . . . . 6 |- ((x e. CC /\ y e. H~) -> (x .h ((S +op T)` y)) = ((S` (x .h y)) +h (T` (x .h y))))
42		hosvaltOLD 9517	. . . . . . 7 |- (((S:H~-->H~ /\ T:H~-->H~) /\ z e. H~) -> ((S +op T)` z) = ((S` z) +h (T` z)))
43	3, 5, 42	mpanl12 708	. . . . . 6 |- (z e. H~ -> ((S +op T)` z) = ((S` z) +h (T` z)))
44	41, 43	opreqan12d 3979	. . . . 5 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((x .h ((S +op T)` y)) +h ((S +op T)` z)) = (((S` (x .h y)) +h (T` (x .h y))) +h ((S` z) +h (T` z))))
45	22, 27, 44	3eqtr4d 1517	. . . 4 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((S +op T)` ((x .h y) +h z)) = ((x .h ((S +op T)` y)) +h ((S +op T)` z)))
46	45	r19.21aiva 1714	. . 3 |- ((x e. CC /\ y e. H~) -> A.z e. H~ ((S +op T)` ((x .h y) +h z)) = ((x .h ((S +op T)` y)) +h ((S +op T)` z)))
47	46	rgen2 1723	. 2 |- A.x e. CC A.y e. H~ A.z e. H~ ((S +op T)` ((x .h y) +h z)) = ((x .h ((S +op T)` y)) +h ((S +op T)` z))
48	1, 6, 47	mpbir2an 730	1 |- (S +op T) e. LinOp

<