# Metamath Proof Explorer

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 ffvelrn $⊢ 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 ffvelrn $⊢ 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$