adjsym - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > adjsym		Structured version Visualization version GIF version

Theorem adjsym 29297

Description: Symmetry property of an adjoint. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)

**Assertion**
Ref	Expression
adjsym	⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·_ih 𝑦)))

Distinct variable groups: 𝑥,𝑦,𝑆 𝑥,𝑇,𝑦

Proof of Theorem adjsym Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffvelrn 6721	. . . . . . . . . . . 12 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → (𝑇‘𝑦) ∈ ℋ)
2		ax-his1 28546	. . . . . . . . . . . 12 ⊢ (((𝑇‘𝑦) ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑦) ·_ih 𝑥) = (∗‘(𝑥 ·_ih (𝑇‘𝑦))))
3	1, 2	sylan 580	. . . . . . . . . . 11 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑦) ·_ih 𝑥) = (∗‘(𝑥 ·_ih (𝑇‘𝑦))))
4	3	adantrl 712	. . . . . . . . . 10 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ)) → ((𝑇‘𝑦) ·_ih 𝑥) = (∗‘(𝑥 ·_ih (𝑇‘𝑦))))
5		ffvelrn 6721	. . . . . . . . . . . 12 ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (𝑆‘𝑥) ∈ ℋ)
6		ax-his1 28546	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℋ ∧ (𝑆‘𝑥) ∈ ℋ) → (𝑦 ·_ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·_ih 𝑦)))
7	5, 6	sylan2 592	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℋ ∧ (𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ)) → (𝑦 ·_ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·_ih 𝑦)))
8	7	adantll 710	. . . . . . . . . 10 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ)) → (𝑦 ·_ih (𝑆‘𝑥)) = (∗‘((𝑆‘𝑥) ·_ih 𝑦)))
9	4, 8	eqeq12d 2812	. . . . . . . . 9 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ)) → (((𝑇‘𝑦) ·_ih 𝑥) = (𝑦 ·_ih (𝑆‘𝑥)) ↔ (∗‘(𝑥 ·_ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·_ih 𝑦))))
10	9	ancoms 459	. . . . . . . 8 ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑇‘𝑦) ·_ih 𝑥) = (𝑦 ·_ih (𝑆‘𝑥)) ↔ (∗‘(𝑥 ·_ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·_ih 𝑦))))
11		hicl 28544	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ) → (𝑥 ·_ih (𝑇‘𝑦)) ∈ ℂ)
12	1, 11	sylan2 592	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℋ ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih (𝑇‘𝑦)) ∈ ℂ)
13	12	adantll 710	. . . . . . . . 9 ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih (𝑇‘𝑦)) ∈ ℂ)
14		hicl 28544	. . . . . . . . . . 11 ⊢ (((𝑆‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘𝑥) ·_ih 𝑦) ∈ ℂ)
15	5, 14	sylan 580	. . . . . . . . . 10 ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧ 𝑦 ∈ ℋ) → ((𝑆‘𝑥) ·_ih 𝑦) ∈ ℂ)
16	15	adantrl 712	. . . . . . . . 9 ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑆‘𝑥) ·_ih 𝑦) ∈ ℂ)
17		cj11 14359	. . . . . . . . 9 ⊢ (((𝑥 ·_ih (𝑇‘𝑦)) ∈ ℂ ∧ ((𝑆‘𝑥) ·_ih 𝑦) ∈ ℂ) → ((∗‘(𝑥 ·_ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·_ih 𝑦)) ↔ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·_ih 𝑦)))
18	13, 16, 17	syl2anc 584	. . . . . . . 8 ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ)) → ((∗‘(𝑥 ·_ih (𝑇‘𝑦))) = (∗‘((𝑆‘𝑥) ·_ih 𝑦)) ↔ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·_ih 𝑦)))
19	10, 18	bitr2d 281	. . . . . . 7 ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑥 ·_ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·_ih 𝑦) ↔ ((𝑇‘𝑦) ·_ih 𝑥) = (𝑦 ·_ih (𝑆‘𝑥))))
20	19	an4s 656	. . . . . 6 ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑥 ·_ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·_ih 𝑦) ↔ ((𝑇‘𝑦) ·_ih 𝑥) = (𝑦 ·_ih (𝑆‘𝑥))))
21	20	anassrs 468	. . . . 5 ⊢ ((((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) ∧ 𝑦 ∈ ℋ) → ((𝑥 ·_ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·_ih 𝑦) ↔ ((𝑇‘𝑦) ·_ih 𝑥) = (𝑦 ·_ih (𝑆‘𝑥))))
22		eqcom 2804	. . . . 5 ⊢ (((𝑇‘𝑦) ·_ih 𝑥) = (𝑦 ·_ih (𝑆‘𝑥)) ↔ (𝑦 ·_ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·_ih 𝑥))
23	21, 22	syl6bb 288	. . . 4 ⊢ ((((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) ∧ 𝑦 ∈ ℋ) → ((𝑥 ·_ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·_ih 𝑦) ↔ (𝑦 ·_ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·_ih 𝑥)))
24	23	ralbidva 3165	. . 3 ⊢ (((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·_ih 𝑦) ↔ ∀𝑦 ∈ ℋ (𝑦 ·_ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·_ih 𝑥)))
25	24	ralbidva 3165	. 2 ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·_ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦 ·_ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·_ih 𝑥)))
26		ralcom 3317	. . . 4 ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦) ↔ ∀𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦))
27		fveq2 6545	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑆‘𝑧) = (𝑆‘𝑦))
28	27	oveq2d 7039	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑥 ·_ih (𝑆‘𝑧)) = (𝑥 ·_ih (𝑆‘𝑦)))
29		oveq2 7031	. . . . . . 7 ⊢ (𝑧 = 𝑦 → ((𝑇‘𝑥) ·_ih 𝑧) = ((𝑇‘𝑥) ·_ih 𝑦))
30	28, 29	eqeq12d 2812	. . . . . 6 ⊢ (𝑧 = 𝑦 → ((𝑥 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·_ih 𝑧) ↔ (𝑥 ·_ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦)))
31	30	ralbidv 3166	. . . . 5 ⊢ (𝑧 = 𝑦 → (∀𝑥 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·_ih 𝑧) ↔ ∀𝑥 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦)))
32	31	cbvralv 3405	. . . 4 ⊢ (∀𝑧 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·_ih 𝑧) ↔ ∀𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦))
33	26, 32	bitr4i 279	. . 3 ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦) ↔ ∀𝑧 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·_ih 𝑧))
34		oveq1 7030	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ·_ih (𝑆‘𝑧)) = (𝑦 ·_ih (𝑆‘𝑧)))
35		fveq2 6545	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑇‘𝑥) = (𝑇‘𝑦))
36	35	oveq1d 7038	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑇‘𝑥) ·_ih 𝑧) = ((𝑇‘𝑦) ·_ih 𝑧))
37	34, 36	eqeq12d 2812	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·_ih 𝑧) ↔ (𝑦 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·_ih 𝑧)))
38	37	cbvralv 3405	. . . 4 ⊢ (∀𝑥 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·_ih 𝑧) ↔ ∀𝑦 ∈ ℋ (𝑦 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·_ih 𝑧))
39	38	ralbii 3134	. . 3 ⊢ (∀𝑧 ∈ ℋ ∀𝑥 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑥) ·_ih 𝑧) ↔ ∀𝑧 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·_ih 𝑧))
40		fveq2 6545	. . . . . . 7 ⊢ (𝑧 = 𝑥 → (𝑆‘𝑧) = (𝑆‘𝑥))
41	40	oveq2d 7039	. . . . . 6 ⊢ (𝑧 = 𝑥 → (𝑦 ·_ih (𝑆‘𝑧)) = (𝑦 ·_ih (𝑆‘𝑥)))
42		oveq2 7031	. . . . . 6 ⊢ (𝑧 = 𝑥 → ((𝑇‘𝑦) ·_ih 𝑧) = ((𝑇‘𝑦) ·_ih 𝑥))
43	41, 42	eqeq12d 2812	. . . . 5 ⊢ (𝑧 = 𝑥 → ((𝑦 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·_ih 𝑧) ↔ (𝑦 ·_ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·_ih 𝑥)))
44	43	ralbidv 3166	. . . 4 ⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ ℋ (𝑦 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·_ih 𝑧) ↔ ∀𝑦 ∈ ℋ (𝑦 ·_ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·_ih 𝑥)))
45	44	cbvralv 3405	. . 3 ⊢ (∀𝑧 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦 ·_ih (𝑆‘𝑧)) = ((𝑇‘𝑦) ·_ih 𝑧) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦 ·_ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·_ih 𝑥))
46	33, 39, 45	3bitri 298	. 2 ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑦 ·_ih (𝑆‘𝑥)) = ((𝑇‘𝑦) ·_ih 𝑥))
47	25, 46	syl6rbbr 291	1 ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑆‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑆‘𝑥) ·_ih 𝑦)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1525 ∈ wcel 2083 ∀wral 3107 ⟶wf 6228 ‘cfv 6232 (class class class)co 7023 ℂcc 10388 ∗ccj 14293 ℋchba 28383 ·_ih csp 28386

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 ax-pre-mulgt0 10467 ax-hfi 28543 ax-his1 28546

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-po 5369 df-so 5370 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-er 8146 df-en 8365 df-dom 8366 df-sdom 8367 df-pnf 10530 df-mnf 10531 df-xr 10532 df-ltxr 10533 df-le 10534 df-sub 10725 df-neg 10726 df-div 11152 df-2 11554 df-cj 14296 df-re 14297 df-im 14298

This theorem is referenced by: dfadj2 29349 adjval2 29355 cnlnadjeui 29541 cnlnssadj 29544 adjbdln 29547

W3C validator