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 : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( ( T ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( S ` x ) .ih y ) ) )

Proof

Step Hyp Ref Expression
1 ralcom 
 |-  ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( ( T ` x ) .ih y ) <-> A. y e. ~H A. x e. ~H ( 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 -> ( A. x e. ~H ( x .ih ( S ` z ) ) = ( ( T ` x ) .ih z ) <-> A. x e. ~H ( x .ih ( S ` y ) ) = ( ( T ` x ) .ih y ) ) )
7 6 cbvralvw 
 |-  ( A. z e. ~H A. x e. ~H ( x .ih ( S ` z ) ) = ( ( T ` x ) .ih z ) <-> A. y e. ~H A. x e. ~H ( x .ih ( S ` y ) ) = ( ( T ` x ) .ih y ) )
8 1 7 bitr4i 
 |-  ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( ( T ` x ) .ih y ) <-> A. z e. ~H A. x e. ~H ( 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 
 |-  ( A. x e. ~H ( x .ih ( S ` z ) ) = ( ( T ` x ) .ih z ) <-> A. y e. ~H ( y .ih ( S ` z ) ) = ( ( T ` y ) .ih z ) )
14 13 ralbii 
 |-  ( A. z e. ~H A. x e. ~H ( x .ih ( S ` z ) ) = ( ( T ` x ) .ih z ) <-> A. z e. ~H A. y e. ~H ( 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 -> ( A. y e. ~H ( y .ih ( S ` z ) ) = ( ( T ` y ) .ih z ) <-> A. y e. ~H ( y .ih ( S ` x ) ) = ( ( T ` y ) .ih x ) ) )
20 19 cbvralvw 
 |-  ( A. z e. ~H A. y e. ~H ( y .ih ( S ` z ) ) = ( ( T ` y ) .ih z ) <-> A. x e. ~H A. y e. ~H ( y .ih ( S ` x ) ) = ( ( T ` y ) .ih x ) )
21 8 14 20 3bitri 
 |-  ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( ( T ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( y .ih ( S ` x ) ) = ( ( T ` y ) .ih x ) )
22 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( T ` y ) e. ~H )
23 ax-his1 
 |-  ( ( ( T ` y ) e. ~H /\ x e. ~H ) -> ( ( T ` y ) .ih x ) = ( * ` ( x .ih ( T ` y ) ) ) )
24 22 23 sylan 
 |-  ( ( ( T : ~H --> ~H /\ y e. ~H ) /\ x e. ~H ) -> ( ( T ` y ) .ih x ) = ( * ` ( x .ih ( T ` y ) ) ) )
25 24 adantrl 
 |-  ( ( ( T : ~H --> ~H /\ y e. ~H ) /\ ( S : ~H --> ~H /\ x e. ~H ) ) -> ( ( T ` y ) .ih x ) = ( * ` ( x .ih ( T ` y ) ) ) )
26 ffvelcdm 
 |-  ( ( S : ~H --> ~H /\ x e. ~H ) -> ( S ` x ) e. ~H )
27 ax-his1 
 |-  ( ( y e. ~H /\ ( S ` x ) e. ~H ) -> ( y .ih ( S ` x ) ) = ( * ` ( ( S ` x ) .ih y ) ) )
28 26 27 sylan2 
 |-  ( ( y e. ~H /\ ( S : ~H --> ~H /\ x e. ~H ) ) -> ( y .ih ( S ` x ) ) = ( * ` ( ( S ` x ) .ih y ) ) )
29 28 adantll 
 |-  ( ( ( T : ~H --> ~H /\ y e. ~H ) /\ ( S : ~H --> ~H /\ x e. ~H ) ) -> ( y .ih ( S ` x ) ) = ( * ` ( ( S ` x ) .ih y ) ) )
30 25 29 eqeq12d 
 |-  ( ( ( T : ~H --> ~H /\ y e. ~H ) /\ ( S : ~H --> ~H /\ x e. ~H ) ) -> ( ( ( T ` y ) .ih x ) = ( y .ih ( S ` x ) ) <-> ( * ` ( x .ih ( T ` y ) ) ) = ( * ` ( ( S ` x ) .ih y ) ) ) )
31 30 ancoms 
 |-  ( ( ( S : ~H --> ~H /\ x e. ~H ) /\ ( T : ~H --> ~H /\ y e. ~H ) ) -> ( ( ( T ` y ) .ih x ) = ( y .ih ( S ` x ) ) <-> ( * ` ( x .ih ( T ` y ) ) ) = ( * ` ( ( S ` x ) .ih y ) ) ) )
32 hicl 
 |-  ( ( x e. ~H /\ ( T ` y ) e. ~H ) -> ( x .ih ( T ` y ) ) e. CC )
33 22 32 sylan2 
 |-  ( ( x e. ~H /\ ( T : ~H --> ~H /\ y e. ~H ) ) -> ( x .ih ( T ` y ) ) e. CC )
34 33 adantll 
 |-  ( ( ( S : ~H --> ~H /\ x e. ~H ) /\ ( T : ~H --> ~H /\ y e. ~H ) ) -> ( x .ih ( T ` y ) ) e. CC )
35 hicl 
 |-  ( ( ( S ` x ) e. ~H /\ y e. ~H ) -> ( ( S ` x ) .ih y ) e. CC )
36 26 35 sylan 
 |-  ( ( ( S : ~H --> ~H /\ x e. ~H ) /\ y e. ~H ) -> ( ( S ` x ) .ih y ) e. CC )
37 36 adantrl 
 |-  ( ( ( S : ~H --> ~H /\ x e. ~H ) /\ ( T : ~H --> ~H /\ y e. ~H ) ) -> ( ( S ` x ) .ih y ) e. CC )
38 cj11 
 |-  ( ( ( x .ih ( T ` y ) ) e. CC /\ ( ( S ` x ) .ih y ) e. CC ) -> ( ( * ` ( x .ih ( T ` y ) ) ) = ( * ` ( ( S ` x ) .ih y ) ) <-> ( x .ih ( T ` y ) ) = ( ( S ` x ) .ih y ) ) )
39 34 37 38 syl2anc 
 |-  ( ( ( S : ~H --> ~H /\ x e. ~H ) /\ ( T : ~H --> ~H /\ y e. ~H ) ) -> ( ( * ` ( x .ih ( T ` y ) ) ) = ( * ` ( ( S ` x ) .ih y ) ) <-> ( x .ih ( T ` y ) ) = ( ( S ` x ) .ih y ) ) )
40 31 39 bitr2d 
 |-  ( ( ( S : ~H --> ~H /\ x e. ~H ) /\ ( T : ~H --> ~H /\ y e. ~H ) ) -> ( ( x .ih ( T ` y ) ) = ( ( S ` x ) .ih y ) <-> ( ( T ` y ) .ih x ) = ( y .ih ( S ` x ) ) ) )
41 40 an4s 
 |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( x .ih ( T ` y ) ) = ( ( S ` x ) .ih y ) <-> ( ( T ` y ) .ih x ) = ( y .ih ( S ` x ) ) ) )
42 41 anassrs 
 |-  ( ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ x e. ~H ) /\ y e. ~H ) -> ( ( 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 : ~H --> ~H /\ T : ~H --> ~H ) /\ x e. ~H ) /\ y e. ~H ) -> ( ( x .ih ( T ` y ) ) = ( ( S ` x ) .ih y ) <-> ( y .ih ( S ` x ) ) = ( ( T ` y ) .ih x ) ) )
45 44 ralbidva 
 |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( A. y e. ~H ( x .ih ( T ` y ) ) = ( ( S ` x ) .ih y ) <-> A. y e. ~H ( y .ih ( S ` x ) ) = ( ( T ` y ) .ih x ) ) )
46 45 ralbidva 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( S ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( y .ih ( S ` x ) ) = ( ( T ` y ) .ih x ) ) )
47 21 46 bitr4id 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( ( T ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( S ` x ) .ih y ) ) )