This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
23 ax-his1 ⊢ ( ( ( 𝑇 ‘ 𝑦 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) )
24 22 23 sylan ⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) )
25 24 adantrl ⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) ) )
26 ffvelcdm ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
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 𝑦 ) ) )