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 ⋅ ih S ⁡ y = T ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = S ⁡ x ⋅ ih y

Proof

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