This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem adjvalval

Description: Value of the value of the adjoint function. (Contributed by NM, 22-Feb-2006) (Proof shortened by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Assertion adjvalval ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ → adj h ⁡ T ⁡ A = ι w ∈ ℋ | ∀ x ∈ ℋ T ⁡ x ⋅ ih A = x ⋅ ih w

Proof

Step Hyp Ref Expression
1 adjcl ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ → adj h ⁡ T ⁡ A ∈ ℋ
2 eqcom ⊢ T ⁡ x ⋅ ih A = x ⋅ ih w ↔ x ⋅ ih w = T ⁡ x ⋅ ih A
3 adj2 ⊢ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ A ∈ ℋ → T ⁡ x ⋅ ih A = x ⋅ ih adj h ⁡ T ⁡ A
4 3 3com23 ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ x ∈ ℋ → T ⁡ x ⋅ ih A = x ⋅ ih adj h ⁡ T ⁡ A
5 4 3expa ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ x ∈ ℋ → T ⁡ x ⋅ ih A = x ⋅ ih adj h ⁡ T ⁡ A
6 5 eqeq2d ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih w = T ⁡ x ⋅ ih A ↔ x ⋅ ih w = x ⋅ ih adj h ⁡ T ⁡ A
7 2 6 bitrid ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ x ∈ ℋ → T ⁡ x ⋅ ih A = x ⋅ ih w ↔ x ⋅ ih w = x ⋅ ih adj h ⁡ T ⁡ A
8 7 ralbidva ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ → ∀ x ∈ ℋ T ⁡ x ⋅ ih A = x ⋅ ih w ↔ ∀ x ∈ ℋ x ⋅ ih w = x ⋅ ih adj h ⁡ T ⁡ A
9 8 adantr ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ w ∈ ℋ → ∀ x ∈ ℋ T ⁡ x ⋅ ih A = x ⋅ ih w ↔ ∀ x ∈ ℋ x ⋅ ih w = x ⋅ ih adj h ⁡ T ⁡ A
10 simpr ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ w ∈ ℋ → w ∈ ℋ
11 1 adantr ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ w ∈ ℋ → adj h ⁡ T ⁡ A ∈ ℋ
12 hial2eq2 ⊢ w ∈ ℋ ∧ adj h ⁡ T ⁡ A ∈ ℋ → ∀ x ∈ ℋ x ⋅ ih w = x ⋅ ih adj h ⁡ T ⁡ A ↔ w = adj h ⁡ T ⁡ A
13 10 11 12 syl2anc ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ w ∈ ℋ → ∀ x ∈ ℋ x ⋅ ih w = x ⋅ ih adj h ⁡ T ⁡ A ↔ w = adj h ⁡ T ⁡ A
14 9 13 bitrd ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ ∧ w ∈ ℋ → ∀ x ∈ ℋ T ⁡ x ⋅ ih A = x ⋅ ih w ↔ w = adj h ⁡ T ⁡ A
15 1 14 riota5 ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ → ι w ∈ ℋ | ∀ x ∈ ℋ T ⁡ x ⋅ ih A = x ⋅ ih w = adj h ⁡ T ⁡ A
16 15 eqcomd ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ → adj h ⁡ T ⁡ A = ι w ∈ ℋ | ∀ x ∈ ℋ T ⁡ x ⋅ ih A = x ⋅ ih w