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