Metamath Proof Explorer

Theorem adjsym

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

Ref Expression
Assertion adjsym ⊢S:ℋ⟶ℋ∧T:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋx⋅ihS⁡y=T⁡x⋅ihy↔∀x∈ℋ∀y∈ℋx⋅ihT⁡y=S⁡x⋅ihy

Proof

Step Hyp Ref Expression
1 ralcom ⊢∀x∈ℋ∀y∈ℋx⋅ihS⁡y=T⁡x⋅ihy↔∀y∈ℋ∀x∈ℋx⋅ihS⁡y=T⁡x⋅ihy
2 fveq2 ⊢z=y→S⁡z=S⁡y
3 2 oveq2d ⊢z=y→x⋅ihS⁡z=x⋅ihS⁡y
4 oveq2 ⊢z=y→T⁡x⋅ihz=T⁡x⋅ihy
5 3 4 eqeq12d ⊢z=y→x⋅ihS⁡z=T⁡x⋅ihz↔x⋅ihS⁡y=T⁡x⋅ihy
6 5 ralbidv ⊢z=y→∀x∈ℋx⋅ihS⁡z=T⁡x⋅ihz↔∀x∈ℋx⋅ihS⁡y=T⁡x⋅ihy
7 6 cbvralvw ⊢∀z∈ℋ∀x∈ℋx⋅ihS⁡z=T⁡x⋅ihz↔∀y∈ℋ∀x∈ℋx⋅ihS⁡y=T⁡x⋅ihy
8 1 7 bitr4i ⊢∀x∈ℋ∀y∈ℋx⋅ihS⁡y=T⁡x⋅ihy↔∀z∈ℋ∀x∈ℋx⋅ihS⁡z=T⁡x⋅ihz
9 oveq1 ⊢x=y→x⋅ihS⁡z=y⋅ihS⁡z
10 fveq2 ⊢x=y→T⁡x=T⁡y
11 10 oveq1d ⊢x=y→T⁡x⋅ihz=T⁡y⋅ihz
12 9 11 eqeq12d ⊢x=y→x⋅ihS⁡z=T⁡x⋅ihz↔y⋅ihS⁡z=T⁡y⋅ihz
13 12 cbvralvw ⊢∀x∈ℋx⋅ihS⁡z=T⁡x⋅ihz↔∀y∈ℋy⋅ihS⁡z=T⁡y⋅ihz
14 13 ralbii ⊢∀z∈ℋ∀x∈ℋx⋅ihS⁡z=T⁡x⋅ihz↔∀z∈ℋ∀y∈ℋy⋅ihS⁡z=T⁡y⋅ihz
15 fveq2 ⊢z=x→S⁡z=S⁡x
16 15 oveq2d ⊢z=x→y⋅ihS⁡z=y⋅ihS⁡x
17 oveq2 ⊢z=x→T⁡y⋅ihz=T⁡y⋅ihx
18 16 17 eqeq12d ⊢z=x→y⋅ihS⁡z=T⁡y⋅ihz↔y⋅ihS⁡x=T⁡y⋅ihx
19 18 ralbidv ⊢z=x→∀y∈ℋy⋅ihS⁡z=T⁡y⋅ihz↔∀y∈ℋy⋅ihS⁡x=T⁡y⋅ihx
20 19 cbvralvw ⊢∀z∈ℋ∀y∈ℋy⋅ihS⁡z=T⁡y⋅ihz↔∀x∈ℋ∀y∈ℋy⋅ihS⁡x=T⁡y⋅ihx
21 8 14 20 3bitri ⊢∀x∈ℋ∀y∈ℋx⋅ihS⁡y=T⁡x⋅ihy↔∀x∈ℋ∀y∈ℋy⋅ihS⁡x=T⁡y⋅ihx
22 ffvelcdm ⊢T:ℋ⟶ℋ∧y∈ℋ→T⁡y∈ℋ
23 ax-his1 ⊢T⁡y∈ℋ∧x∈ℋ→T⁡y⋅ihx=x⋅ihT⁡y‾
24 22 23 sylan ⊢T:ℋ⟶ℋ∧y∈ℋ∧x∈ℋ→T⁡y⋅ihx=x⋅ihT⁡y‾
25 24 adantrl ⊢T:ℋ⟶ℋ∧y∈ℋ∧S:ℋ⟶ℋ∧x∈ℋ→T⁡y⋅ihx=x⋅ihT⁡y‾
26 ffvelcdm ⊢S:ℋ⟶ℋ∧x∈ℋ→S⁡x∈ℋ
27 ax-his1 ⊢y∈ℋ∧S⁡x∈ℋ→y⋅ihS⁡x=S⁡x⋅ihy‾
28 26 27 sylan2 ⊢y∈ℋ∧S:ℋ⟶ℋ∧x∈ℋ→y⋅ihS⁡x=S⁡x⋅ihy‾
29 28 adantll ⊢T:ℋ⟶ℋ∧y∈ℋ∧S:ℋ⟶ℋ∧x∈ℋ→y⋅ihS⁡x=S⁡x⋅ihy‾
30 25 29 eqeq12d ⊢T:ℋ⟶ℋ∧y∈ℋ∧S:ℋ⟶ℋ∧x∈ℋ→T⁡y⋅ihx=y⋅ihS⁡x↔x⋅ihT⁡y‾=S⁡x⋅ihy‾
31 30 ancoms ⊢S:ℋ⟶ℋ∧x∈ℋ∧T:ℋ⟶ℋ∧y∈ℋ→T⁡y⋅ihx=y⋅ihS⁡x↔x⋅ihT⁡y‾=S⁡x⋅ihy‾
32 hicl ⊢x∈ℋ∧T⁡y∈ℋ→x⋅ihT⁡y∈ℂ
33 22 32 sylan2 ⊢x∈ℋ∧T:ℋ⟶ℋ∧y∈ℋ→x⋅ihT⁡y∈ℂ
34 33 adantll ⊢S:ℋ⟶ℋ∧x∈ℋ∧T:ℋ⟶ℋ∧y∈ℋ→x⋅ihT⁡y∈ℂ
35 hicl ⊢S⁡x∈ℋ∧y∈ℋ→S⁡x⋅ihy∈ℂ
36 26 35 sylan ⊢S:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→S⁡x⋅ihy∈ℂ
37 36 adantrl ⊢S:ℋ⟶ℋ∧x∈ℋ∧T:ℋ⟶ℋ∧y∈ℋ→S⁡x⋅ihy∈ℂ
38 cj11 ⊢x⋅ihT⁡y∈ℂ∧S⁡x⋅ihy∈ℂ→x⋅ihT⁡y‾=S⁡x⋅ihy‾↔x⋅ihT⁡y=S⁡x⋅ihy
39 34 37 38 syl2anc ⊢S:ℋ⟶ℋ∧x∈ℋ∧T:ℋ⟶ℋ∧y∈ℋ→x⋅ihT⁡y‾=S⁡x⋅ihy‾↔x⋅ihT⁡y=S⁡x⋅ihy
40 31 39 bitr2d ⊢S:ℋ⟶ℋ∧x∈ℋ∧T:ℋ⟶ℋ∧y∈ℋ→x⋅ihT⁡y=S⁡x⋅ihy↔T⁡y⋅ihx=y⋅ihS⁡x
41 40 an4s ⊢S:ℋ⟶ℋ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→x⋅ihT⁡y=S⁡x⋅ihy↔T⁡y⋅ihx=y⋅ihS⁡x
42 41 anassrs ⊢S:ℋ⟶ℋ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→x⋅ihT⁡y=S⁡x⋅ihy↔T⁡y⋅ihx=y⋅ihS⁡x
43 eqcom ⊢T⁡y⋅ihx=y⋅ihS⁡x↔y⋅ihS⁡x=T⁡y⋅ihx
44 42 43 bitrdi ⊢S:ℋ⟶ℋ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→x⋅ihT⁡y=S⁡x⋅ihy↔y⋅ihS⁡x=T⁡y⋅ihx
45 44 ralbidva ⊢S:ℋ⟶ℋ∧T:ℋ⟶ℋ∧x∈ℋ→∀y∈ℋx⋅ihT⁡y=S⁡x⋅ihy↔∀y∈ℋy⋅ihS⁡x=T⁡y⋅ihx
46 45 ralbidva ⊢S:ℋ⟶ℋ∧T:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=S⁡x⋅ihy↔∀x∈ℋ∀y∈ℋy⋅ihS⁡x=T⁡y⋅ihx
47 21 46 bitr4id ⊢S:ℋ⟶ℋ∧T:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋx⋅ihS⁡y=T⁡x⋅ihy↔∀x∈ℋ∀y∈ℋx⋅ihT⁡y=S⁡x⋅ihy