Theorem hmoplint 9866

Description: A Hermitian operator is linear.

Assertion

Ref	Expression
hmoplint	|- (T e. HrmOp -> T e. LinOp)

Proof of Theorem hmoplint

Step	Hyp	Ref	Expression
1		hmopft 9801	. . 3 |- (T e. HrmOp -> T:H~-->H~)
2		hmopt 9846	. . . . . . . . . . 11 |- ((T e. HrmOp /\ ((x .h y) +h z) e. H~ /\ w e. H~) -> (((x .h y) +h z) .ih (T` w)) = ((T` ((x .h y) +h z)) .ih w))
3	2	eqcomd 1480	. . . . . . . . . 10 |- ((T e. HrmOp /\ ((x .h y) +h z) e. H~ /\ w e. H~) -> ((T` ((x .h y) +h z)) .ih w) = (((x .h y) +h z) .ih (T` w)))
4		pm3.26 319	. . . . . . . . . . 11 |- ((T e. HrmOp /\ (x e. CC /\ y e. H~)) -> T e. HrmOp)
5	4	ad2antrr 404	. . . . . . . . . 10 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> T e. HrmOp)
6		hvaddclt 8882	. . . . . . . . . . . . 13 |- (((x .h y) e. H~ /\ z e. H~) -> ((x .h y) +h z) e. H~)
7		hvmulclt 8883	. . . . . . . . . . . . 13 |- ((x e. CC /\ y e. H~) -> (x .h y) e. H~)
8	6, 7	sylan 448	. . . . . . . . . . . 12 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> ((x .h y) +h z) e. H~)
9	8	adantll 392	. . . . . . . . . . 11 |- (((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) -> ((x .h y) +h z) e. H~)
10	9	adantr 389	. . . . . . . . . 10 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((x .h y) +h z) e. H~)
11		pm3.27 323	. . . . . . . . . 10 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> w e. H~)
12	3, 5, 10, 11	syl3anc 858	. . . . . . . . 9 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((T` ((x .h y) +h z)) .ih w) = (((x .h y) +h z) .ih (T` w)))
13		hiassdit 8957	. . . . . . . . . 10 |- (((x e. CC /\ y e. H~) /\ (z e. H~ /\ (T` w) e. H~)) -> (((x .h y) +h z) .ih (T` w)) = ((x x. (y .ih (T` w))) + (z .ih (T` w))))
14		simprl 414	. . . . . . . . . . 11 |- ((T e. HrmOp /\ (x e. CC /\ y e. H~)) -> x e. CC)
15	14	ad2antrr 404	. . . . . . . . . 10 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> x e. CC)
16		simprr 415	. . . . . . . . . . 11 |- ((T e. HrmOp /\ (x e. CC /\ y e. H~)) -> y e. H~)
17	16	ad2antrr 404	. . . . . . . . . 10 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> y e. H~)
18		simplr 413	. . . . . . . . . 10 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> z e. H~)
19		ffvelrn 3814	. . . . . . . . . . . . 13 |- ((T:H~-->H~ /\ w e. H~) -> (T` w) e. H~)
20	19, 1	sylan 448	. . . . . . . . . . . 12 |- ((T e. HrmOp /\ w e. H~) -> (T` w) e. H~)
21	20	adantlr 393	. . . . . . . . . . 11 |- (((T e. HrmOp /\ z e. H~) /\ w e. H~) -> (T` w) e. H~)
22	21	adantllr 397	. . . . . . . . . 10 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (T` w) e. H~)
23	13, 15, 17, 18, 22	syl2anc 472	. . . . . . . . 9 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (((x .h y) +h z) .ih (T` w)) = ((x x. (y .ih (T` w))) + (z .ih (T` w))))
24		hiassdit 8957	. . . . . . . . . . 11 |- (((x e. CC /\ (T` y) e. H~) /\ ((T` z) e. H~ /\ w e. H~)) -> (((x .h (T` y)) +h (T` z)) .ih w) = ((x x. ((T` y) .ih w)) + ((T` z) .ih w)))
25		ffvelrn 3814	. . . . . . . . . . . . . 14 |- ((T:H~-->H~ /\ y e. H~) -> (T` y) e. H~)
26	25, 1	sylan 448	. . . . . . . . . . . . 13 |- ((T e. HrmOp /\ y e. H~) -> (T` y) e. H~)
27	26	adantrl 394	. . . . . . . . . . . 12 |- ((T e. HrmOp /\ (x e. CC /\ y e. H~)) -> (T` y) e. H~)
28	27	ad2antrr 404	. . . . . . . . . . 11 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (T` y) e. H~)
29		ffvelrn 3814	. . . . . . . . . . . . . 14 |- ((T:H~-->H~ /\ z e. H~) -> (T` z) e. H~)
30	29, 1	sylan 448	. . . . . . . . . . . . 13 |- ((T e. HrmOp /\ z e. H~) -> (T` z) e. H~)
31	30	adantr 389	. . . . . . . . . . . 12 |- (((T e. HrmOp /\ z e. H~) /\ w e. H~) -> (T` z) e. H~)
32	31	adantllr 397	. . . . . . . . . . 11 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (T` z) e. H~)
33	24, 15, 28, 32, 11	syl2anc 472	. . . . . . . . . 10 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (((x .h (T` y)) +h (T` z)) .ih w) = ((x x. ((T` y) .ih w)) + ((T` z) .ih w)))
34		hmopt 9846	. . . . . . . . . . . . . . . 16 |- ((T e. HrmOp /\ y e. H~ /\ w e. H~) -> (y .ih (T` w)) = ((T` y) .ih w))
35	34	eqcomd 1480	. . . . . . . . . . . . . . 15 |- ((T e. HrmOp /\ y e. H~ /\ w e. H~) -> ((T` y) .ih w) = (y .ih (T` w)))
36	35	3expa 833	. . . . . . . . . . . . . 14 |- (((T e. HrmOp /\ y e. H~) /\ w e. H~) -> ((T` y) .ih w) = (y .ih (T` w)))
37	36	opreq2d 3976	. . . . . . . . . . . . 13 |- (((T e. HrmOp /\ y e. H~) /\ w e. H~) -> (x x. ((T` y) .ih w)) = (x x. (y .ih (T` w))))
38	37	adantlrl 398	. . . . . . . . . . . 12 |- (((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ w e. H~) -> (x x. ((T` y) .ih w)) = (x x. (y .ih (T` w))))
39	38	adantlr 393	. . . . . . . . . . 11 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> (x x. ((T` y) .ih w)) = (x x. (y .ih (T` w))))
40		hmopt 9846	. . . . . . . . . . . . . 14 |- ((T e. HrmOp /\ z e. H~ /\ w e. H~) -> (z .ih (T` w)) = ((T` z) .ih w))
41	40	eqcomd 1480	. . . . . . . . . . . . 13 |- ((T e. HrmOp /\ z e. H~ /\ w e. H~) -> ((T` z) .ih w) = (z .ih (T` w)))
42	41	3expa 833	. . . . . . . . . . . 12 |- (((T e. HrmOp /\ z e. H~) /\ w e. H~) -> ((T` z) .ih w) = (z .ih (T` w)))
43	42	adantllr 397	. . . . . . . . . . 11 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((T` z) .ih w) = (z .ih (T` w)))
44	39, 43	opreq12d 3978	. . . . . . . . . 10 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((x x. ((T` y) .ih w)) + ((T` z) .ih w)) = ((x x. (y .ih (T` w))) + (z .ih (T` w))))
45	33, 44	eqtr2d 1508	. . . . . . . . 9 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((x x. (y .ih (T` w))) + (z .ih (T` w))) = (((x .h (T` y)) +h (T` z)) .ih w))
46	12, 23, 45	3eqtrd 1511	. . . . . . . 8 |- ((((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) /\ w e. H~) -> ((T` ((x .h y) +h z)) .ih w) = (((x .h (T` y)) +h (T` z)) .ih w))
47	46	r19.21aiva 1714	. . . . . . 7 |- (((T e. HrmOp /\ (x e. CC /\ y e. H~)) /\ z e. H~) -> A.w e. H~ ((T` ((x .h y) +h z)) .ih w) = (((x .h (T` y)) +h (T` z)) .ih w))
48		hial2eqt 8972	. . . . . . . . 9 |- (((T` ((x .h y) +h z)) e. H~ /\ ((x .h (T` y)) +h (T` z)) e. H~) -> (A.w e. H~ ((T` ((x .h y) +h z)) .ih w) = (((x .h (T` y)) +h (T` z)) .ih w) <-> (T` ((x .h y) +h z)) = ((x .h (T` y)) +h (T` z))))
49		ffvelrn 3814	. . . . . . . . . . 11 |- ((T:H~-->H~ /\ ((x .h y) +h z) e. H~) -> (T` ((x .h y) +h z)) e. H~)
50	49, 8