Theorem adjsymt 9759

Description: Symmetry property of an adjoint.

Assertion

Ref	Expression
adjsymt	|- ((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)))

Distinct variable groups:   x,y,S   x,T,y

Proof of Theorem adjsymt

Step	Hyp	Ref	Expression
1		ax-his1 8949	. . . . . . . . . . . 12 |- (((T` y) e. H~ /\ x e. H~) -> ((T` y) .ih x) = (*` (x .ih (T` y))))
2		ffvelrn 3814	. . . . . . . . . . . 12 |- ((T:H~-->H~ /\ y e. H~) -> (T` y) e. H~)
3	1, 2	sylan 448	. . . . . . . . . . 11 |- (((T:H~-->H~ /\ y e. H~) /\ x e. H~) -> ((T` y) .ih x) = (*` (x .ih (T` y))))
4	3	adantrl 394	. . . . . . . . . 10 |- (((T:H~-->H~ /\ y e. H~) /\ (S:H~-->H~ /\ x e. H~)) -> ((T` y) .ih x) = (*` (x .ih (T` y))))
5		ax-his1 8949	. . . . . . . . . . . 12 |- ((y e. H~ /\ (S` x) e. H~) -> (y .ih (S` x)) = (*` ((S` x) .ih y)))
6		ffvelrn 3814	. . . . . . . . . . . 12 |- ((S:H~-->H~ /\ x e. H~) -> (S` x) e. H~)
7	5, 6	sylan2 451	. . . . . . . . . . 11 |- ((y e. H~ /\ (S:H~-->H~ /\ x e. H~)) -> (y .ih (S` x)) = (*` ((S` x) .ih y)))
8	7	adantll 392	. . . . . . . . . 10 |- (((T:H~-->H~ /\ y e. H~) /\ (S:H~-->H~ /\ x e. H~)) -> (y .ih (S` x)) = (*` ((S` x) .ih y)))
9	4, 8	eqeq12d 1489	. . . . . . . . 9 |- (((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))))
10	9	ancoms 436	. . . . . . . 8 |- (((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))))
11		cj11t 6830	. . . . . . . . 9 |- (((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)))
12		hiclt 8947	. . . . . . . . . . 11 |- ((x e. H~ /\ (T` y) e. H~) -> (x .ih (T` y)) e. CC)
13	12, 2	sylan2 451	. . . . . . . . . 10 |- ((x e. H~ /\ (T:H~-->H~ /\ y e. H~)) -> (x .ih (T` y)) e. CC)
14	13	adantll 392	. . . . . . . . 9 |- (((S:H~-->H~ /\ x e. H~) /\ (T:H~-->H~ /\ y e. H~)) -> (x .ih (T` y)) e. CC)
15		hiclt 8947	. . . . . . . . . . 11 |- (((S` x) e. H~ /\ y e. H~) -> ((S` x) .ih y) e. CC)
16	15, 6	sylan 448	. . . . . . . . . 10 |- (((S:H~-->H~ /\ x e. H~) /\ y e. H~) -> ((S` x) .ih y) e. CC)
17	16	adantrl 394	. . . . . . . . 9 |- (((S:H~-->H~ /\ x e. H~) /\ (T:H~-->H~ /\ y e. H~)) -> ((S` x) .ih y) e. CC)
18	11, 14, 17	sylanc 471	. . . . . . . 8 |- (((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)))
19	10, 18	bitr2d 529	. . . . . . 7 |- (((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))))
20	19	an4s 508	. . . . . 6 |- (((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))))
21	20	anassrs 441	. . . . 5 |- ((((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))))
22		eqcom 1477	. . . . 5 |- (((T` y) .ih x) = (y .ih (S` x)) <-> (y .ih (S` x)) = ((T` y) .ih x))
23	21, 22	syl6bb 536	. . . 4 |- ((((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)))
24	23	ralbidva 1659	. . 3 |- (((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)))
25	24	ralbidva 1659	. 2 |- ((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)))
26		ralcom 1774	. . . 4 |- (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))
27		fveq2 3724	. . . . . . . 8 |- (z = y -> (S` z) = (S` y))
28	27	opreq2d 3976	. . . . . . 7 |- (z = y -> (x .ih (S` z)) = (x .ih (S` y)))
29		opreq2 3969	. . . . . . 7 |- (z = y -> ((T` x) .ih z) = ((T` x) .ih y))
30	28, 29	eqeq12d 1489	. . . . . 6 |- (z = y -> ((x .ih (S` z)) = ((T` x) .ih z) <-> (x .ih (S` y)) = ((T` x) .ih y)))
31	30	ralbidv 1663	. . . . 5 |- (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)))
32	31	cbvralv 1800	. . . 4 |- (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))
33	26, 32	bitr4 176	. . 3 |- (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))
34		opreq1 3968	. . . . . 6 |- (x = y -> (x .ih (S` z)) = (y .ih (S` z)))
35		fveq2 3724	. . . . . . 7 |- (x = y -> (T` x) = (T` y))
36	35	opreq1d 3975	. . . . . 6 |- (x = y -> ((T` x) .ih z) = ((T` y) .ih z))
37	34, 36	eqeq12d 1489	. . . . 5 |- (x = y -> ((x .ih (S` z)) = ((T` x) .ih z) <-> (y .ih (S` z)) = ((T` y) .ih z)))
38	37	cbvralv 1800	. . . 4 |- (A.x e. H~ (x .ih (S` z)) = ((T` x) .ih z) <-> A.y e. H~ (y .ih (S` z)) = ((T` y) .ih z))
39	38	ralbii 1667	. . 3 |- (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))
40		fveq2 3724	. . . . . . 7 |- (z = x -> (S` z) = (S` x))
41	40	opreq2d 3976	. . . . . 6 |- (z = x -> (y .ih (S` z)) = (y .ih (S` x)))
42		opreq2 3969	. . . . . 6 |- (z = x -> ((T` y) .ih z) = ((T` y) .ih x))
43	41, 42	eqeq12d 1489	. . . . 5 |- (z = x -> ((y .ih (S` z)) = ((T` y) .ih z) <-> (y .ih (S` x)) = ((T` y) .ih x)))
44	43	ralbidv 1663	. . . 4 |- (z =