Theorem hmopcot 9948

Description: The composition of two commuting Hermitian operators is Hermitian.

Assertion

Ref	Expression
hmopcot	|- ((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) -> (T o. U) e. HrmOp)

Proof of Theorem hmopcot

Step	Hyp	Ref	Expression
1		fco 3636	. . . . 5 |- ((T:H~-->H~ /\ U:H~-->H~) -> (T o. U):H~-->H~)
2		hmopft 9801	. . . . 5 |- (T e. HrmOp -> T:H~-->H~)
3		hmopft 9801	. . . . 5 |- (U e. HrmOp -> U:H~-->H~)
4	1, 2, 3	syl2an 454	. . . 4 |- ((T e. HrmOp /\ U e. HrmOp) -> (T o. U):H~-->H~)
5	4	3adant3 799	. . 3 |- ((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) -> (T o. U):H~-->H~)
6		fvco3 3776	. . . . . . . . . . . . 13 |- ((Fun T /\ U:H~-->H~ /\ y e. H~) -> ((T o. U)` y) = (T` (U` y)))
7		ffun 3629	. . . . . . . . . . . . . 14 |- (T:H~-->H~ -> Fun T)
8	2, 7	syl 10	. . . . . . . . . . . . 13 |- (T e. HrmOp -> Fun T)
9		id 59	. . . . . . . . . . . . 13 |- (y e. H~ -> y e. H~)
10	6, 8, 3, 9	syl3an 868	. . . . . . . . . . . 12 |- ((T e. HrmOp /\ U e. HrmOp /\ y e. H~) -> ((T o. U)` y) = (T` (U` y)))
11	10	3expa 833	. . . . . . . . . . 11 |- (((T e. HrmOp /\ U e. HrmOp) /\ y e. H~) -> ((T o. U)` y) = (T` (U` y)))
12	11	opreq2d 3976	. . . . . . . . . 10 |- (((T e. HrmOp /\ U e. HrmOp) /\ y e. H~) -> (x .ih ((T o. U)` y)) = (x .ih (T` (U` y))))
13	12	adantrl 394	. . . . . . . . 9 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> (x .ih ((T o. U)` y)) = (x .ih (T` (U` y))))
14		hmopt 9846	. . . . . . . . . 10 |- ((T e. HrmOp /\ x e. H~ /\ (U` y) e. H~) -> (x .ih (T` (U` y))) = ((T` x) .ih (U` y)))
15		simpll 412	. . . . . . . . . 10 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> T e. HrmOp)
16		simprl 414	. . . . . . . . . 10 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> x e. H~)
17		ffvelrn 3814	. . . . . . . . . . . 12 |- ((U:H~-->H~ /\ y e. H~) -> (U` y) e. H~)
18	17, 3	sylan 448	. . . . . . . . . . 11 |- ((U e. HrmOp /\ y e. H~) -> (U` y) e. H~)
19	18	ad2ant2l 408	. . . . . . . . . 10 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> (U` y) e. H~)
20	14, 15, 16, 19	syl3anc 858	. . . . . . . . 9 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> (x .ih (T` (U` y))) = ((T` x) .ih (U` y)))
21		hmopt 9846	. . . . . . . . . 10 |- ((U e. HrmOp /\ (T` x) e. H~ /\ y e. H~) -> ((T` x) .ih (U` y)) = ((U` (T` x)) .ih y))
22		simplr 413	. . . . . . . . . 10 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> U e. HrmOp)
23		ffvelrn 3814	. . . . . . . . . . . 12 |- ((T:H~-->H~ /\ x e. H~) -> (T` x) e. H~)
24	23, 2	sylan 448	. . . . . . . . . . 11 |- ((T e. HrmOp /\ x e. H~) -> (T` x) e. H~)
25	24	ad2ant2r 409	. . . . . . . . . 10 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> (T` x) e. H~)
26		simprr 415	. . . . . . . . . 10 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> y e. H~)
27	21, 22, 25, 26	syl3anc 858	. . . . . . . . 9 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> ((T` x) .ih (U` y)) = ((U` (T` x)) .ih y))
28	13, 20, 27	3eqtrd 1511	. . . . . . . 8 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> (x .ih ((T o. U)` y)) = ((U` (T` x)) .ih y))
29		fvco3 3776	. . . . . . . . . . . . 13 |- ((Fun U /\ T:H~-->H~ /\ x e. H~) -> ((U o. T)` x) = (U` (T` x)))
30		ffun 3629	. . . . . . . . . . . . . 14 |- (U:H~-->H~ -> Fun U)
31	3, 30	syl 10	. . . . . . . . . . . . 13 |- (U e. HrmOp -> Fun U)
32		id 59	. . . . . . . . . . . . 13 |- (x e. H~ -> x e. H~)
33	29, 31, 2, 32	syl3an 868	. . . . . . . . . . . 12 |- ((U e. HrmOp /\ T e. HrmOp /\ x e. H~) -> ((U o. T)` x) = (U` (T` x)))
34	33	3expa 833	. . . . . . . . . . 11 |- (((U e. HrmOp /\ T e. HrmOp) /\ x e. H~) -> ((U o. T)` x) = (U` (T` x)))
35	34	ancom1s 490	. . . . . . . . . 10 |- (((T e. HrmOp /\ U e. HrmOp) /\ x e. H~) -> ((U o. T)` x) = (U` (T` x)))
36	35	opreq1d 3975	. . . . . . . . 9 |- (((T e. HrmOp /\ U e. HrmOp) /\ x e. H~) -> (((U o. T)` x) .ih y) = ((U` (T` x)) .ih y))
37	36	adantrr 395	. . . . . . . 8 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> (((U o. T)` x) .ih y) = ((U` (T` x)) .ih y))
38	28, 37	eqtr4d 1510	. . . . . . 7 |- (((T e. HrmOp /\ U e. HrmOp) /\ (x e. H~ /\ y e. H~)) -> (x .ih ((T o. U)` y)) = (((U o. T)` x) .ih y))
39	38	3adantl3 805	. . . . . 6 |- (((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) /\ (x e. H~ /\ y e. H~)) -> (x .ih ((T o. U)` y)) = (((U o. T)` x) .ih y))
40		fveq1 3723	. . . . . . . . 9 |- ((T o. U) = (U o. T) -> ((T o. U)` x) = ((U o. T)` x))
41	40	opreq1d 3975	. . . . . . . 8 |- ((T o. U) = (U o. T) -> (((T o. U)` x) .ih y) = (((U o. T)` x) .ih y))
42	41	3ad2ant3 802	. . . . . . 7 |- ((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) -> (((T o. U)` x) .ih y) = (((U o. T)` x) .ih y))
43	42	adantr 389	. . . . . 6 |- (((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) /\ (x e. H~ /\ y e. H~)) -> (((T o. U)` x) .ih y) = (((U o. T)` x) .ih y))
44	39, 43	eqtr4d 1510	. . . . 5 |- (((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) /\ (x e. H~ /\ y e. H~)) -> (x .ih ((T o. U)` y)) = (((T o. U)` x) .ih y))
45	44	ex 373	. . . 4 |- ((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) -> ((x e. H~ /\ y e. H~) -> (x .ih ((T o. U)` y)) = (((T o. U)` x) .ih y)))
46	45	r19.21aivv 1720	. . 3 |- ((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) -> A.x e. H~ A.y e. H~ (x .ih ((T o. U)` y)) = (((T o. U)` x) .ih y))
47	5, 46	jca 288	. 2 |- ((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) -> ((T o. U):H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih ((T o. U)` y)) = (((T o. U)` x) .ih y)))
48		elhmopt 9800	. 2 |- ((T o. U) e. HrmOp <-> ((T o. U):H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih ((T o. U)` y)) = (((T o. U)` x) .ih y)))
49	47, 48	sylibr 200	1 |- ((T e. HrmOp /\ U e. HrmOp /\ (T o. U) = (U o. T)) -> (T o. U) e. HrmOp)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775   = wceq 956   e. wcel 958  A.wral 1645   o. ccom 3174  Fun wfun 3176  -->wf 3178  ` cfv 3182  (class class class)co 3963  H~chil 8788   .ih csp 8793  HrmOpcho 8819

This theorem is referenced by:  leopsqt 10062

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866  ax-hilex 8869

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-id 2835  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-f 3194  df-fv 3198  df-opr 3965  df-hmop 9770

Copyright terms: Public domain