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