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 ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 ralcom ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) )
2 fveq2 ( 𝑧 = 𝑦 → ( 𝑆𝑧 ) = ( 𝑆𝑦 ) )
3 2 oveq2d ( 𝑧 = 𝑦 → ( 𝑥 ·ih ( 𝑆𝑧 ) ) = ( 𝑥 ·ih ( 𝑆𝑦 ) ) )
4 oveq2 ( 𝑧 = 𝑦 → ( ( 𝑇𝑥 ) ·ih 𝑧 ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) )
5 3 4 eqeq12d ( 𝑧 = 𝑦 → ( ( 𝑥 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑧 ) ↔ ( 𝑥 ·ih ( 𝑆𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) ) )
6 5 ralbidv ( 𝑧 = 𝑦 → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) ) )
7 6 cbvralvw ( ∀ 𝑧 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) )
8 1 7 bitr4i ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑧 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑧 ) )
9 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 ·ih ( 𝑆𝑧 ) ) = ( 𝑦 ·ih ( 𝑆𝑧 ) ) )
10 fveq2 ( 𝑥 = 𝑦 → ( 𝑇𝑥 ) = ( 𝑇𝑦 ) )
11 10 oveq1d ( 𝑥 = 𝑦 → ( ( 𝑇𝑥 ) ·ih 𝑧 ) = ( ( 𝑇𝑦 ) ·ih 𝑧 ) )
12 9 11 eqeq12d ( 𝑥 = 𝑦 → ( ( 𝑥 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑧 ) ↔ ( 𝑦 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑧 ) ) )
13 12 cbvralvw ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑧 ) )
14 13 ralbii ( ∀ 𝑧 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑧 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑧 ) )
15 fveq2 ( 𝑧 = 𝑥 → ( 𝑆𝑧 ) = ( 𝑆𝑥 ) )
16 15 oveq2d ( 𝑧 = 𝑥 → ( 𝑦 ·ih ( 𝑆𝑧 ) ) = ( 𝑦 ·ih ( 𝑆𝑥 ) ) )
17 oveq2 ( 𝑧 = 𝑥 → ( ( 𝑇𝑦 ) ·ih 𝑧 ) = ( ( 𝑇𝑦 ) ·ih 𝑥 ) )
18 16 17 eqeq12d ( 𝑧 = 𝑥 → ( ( 𝑦 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑧 ) ↔ ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑥 ) ) )
19 18 ralbidv ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑧 ) ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑥 ) ) )
20 19 cbvralvw ( ∀ 𝑧 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆𝑧 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑧 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑥 ) )
21 8 14 20 3bitri ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑥 ) )
22 ffvelrn ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇𝑦 ) ∈ ℋ )
23 ax-his1 ( ( ( 𝑇𝑦 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑇𝑦 ) ) ) )
24 22 23 sylan ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑇𝑦 ) ) ) )
25 24 adantrl ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( 𝑇𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑇𝑦 ) ) ) )
26 ffvelrn ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑆𝑥 ) ∈ ℋ )
27 ax-his1 ( ( 𝑦 ∈ ℋ ∧ ( 𝑆𝑥 ) ∈ ℋ ) → ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ∗ ‘ ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) )
28 26 27 sylan2 ( ( 𝑦 ∈ ℋ ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ∗ ‘ ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) )
29 28 adantll ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ∗ ‘ ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) )
30 25 29 eqeq12d ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( ( 𝑇𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆𝑥 ) ) ↔ ( ∗ ‘ ( 𝑥 ·ih ( 𝑇𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) ) )
31 30 ancoms ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑇𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆𝑥 ) ) ↔ ( ∗ ‘ ( 𝑥 ·ih ( 𝑇𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) ) )
32 hicl ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑦 ) ∈ ℋ ) → ( 𝑥 ·ih ( 𝑇𝑦 ) ) ∈ ℂ )
33 22 32 sylan2 ( ( 𝑥 ∈ ℋ ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑇𝑦 ) ) ∈ ℂ )
34 33 adantll ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑇𝑦 ) ) ∈ ℂ )
35 hicl ( ( ( 𝑆𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑆𝑥 ) ·ih 𝑦 ) ∈ ℂ )
36 26 35 sylan ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑆𝑥 ) ·ih 𝑦 ) ∈ ℂ )
37 36 adantrl ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑆𝑥 ) ·ih 𝑦 ) ∈ ℂ )
38 cj11 ( ( ( 𝑥 ·ih ( 𝑇𝑦 ) ) ∈ ℂ ∧ ( ( 𝑆𝑥 ) ·ih 𝑦 ) ∈ ℂ ) → ( ( ∗ ‘ ( 𝑥 ·ih ( 𝑇𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) )
39 34 37 38 syl2anc ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ∗ ‘ ( 𝑥 ·ih ( 𝑇𝑦 ) ) ) = ( ∗ ‘ ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) )
40 31 39 bitr2d ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑆𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑇𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆𝑥 ) ) ) )
41 40 an4s ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑆𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑇𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆𝑥 ) ) ) )
42 41 anassrs ( ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑆𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑇𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆𝑥 ) ) ) )
43 eqcom ( ( ( 𝑇𝑦 ) ·ih 𝑥 ) = ( 𝑦 ·ih ( 𝑆𝑥 ) ) ↔ ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑥 ) )
44 42 43 bitrdi ( ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑆𝑥 ) ·ih 𝑦 ) ↔ ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑥 ) ) )
45 44 ralbidva ( ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑆𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑥 ) ) )
46 45 ralbidva ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑆𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑆𝑥 ) ) = ( ( 𝑇𝑦 ) ·ih 𝑥 ) ) )
47 21 46 bitr4id ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑆𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑆𝑥 ) ·ih 𝑦 ) ) )