Step | Hyp | Ref
| Expression |
1 | | phnv 27053 |
. . . . 5
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) |
2 | | ajval.1 |
. . . . . 6
⊢ 𝑋 = (BaseSet‘𝑈) |
3 | | ajval.2 |
. . . . . 6
⊢ 𝑌 = (BaseSet‘𝑊) |
4 | | ajval.3 |
. . . . . 6
⊢ 𝑃 =
(·𝑖OLD‘𝑈) |
5 | | ajval.4 |
. . . . . 6
⊢ 𝑄 =
(·𝑖OLD‘𝑊) |
6 | | ajval.5 |
. . . . . 6
⊢ 𝐴 = (𝑈adj𝑊) |
7 | 2, 3, 4, 5, 6 | ajfval 27048 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐴 = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) |
8 | 1, 7 | sylan 487 |
. . . 4
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ NrmCVec)
→ 𝐴 = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) |
9 | 8 | fveq1d 6105 |
. . 3
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ NrmCVec)
→ (𝐴‘𝑇) = ({〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}‘𝑇)) |
10 | 9 | 3adant3 1074 |
. 2
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ NrmCVec
∧ 𝑇:𝑋⟶𝑌) → (𝐴‘𝑇) = ({〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}‘𝑇)) |
11 | | fvex 6113 |
. . . . . . 7
⊢
(BaseSet‘𝑈)
∈ V |
12 | 2, 11 | eqeltri 2684 |
. . . . . 6
⊢ 𝑋 ∈ V |
13 | | fex 6394 |
. . . . . 6
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝑋 ∈ V) → 𝑇 ∈ V) |
14 | 12, 13 | mpan2 703 |
. . . . 5
⊢ (𝑇:𝑋⟶𝑌 → 𝑇 ∈ V) |
15 | | eqid 2610 |
. . . . . 6
⊢
{〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))} = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))} |
16 | | feq1 5939 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (𝑡:𝑋⟶𝑌 ↔ 𝑇:𝑋⟶𝑌)) |
17 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → (𝑡‘𝑥) = (𝑇‘𝑥)) |
18 | 17 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → ((𝑡‘𝑥)𝑄𝑦) = ((𝑇‘𝑥)𝑄𝑦)) |
19 | 18 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)) ↔ ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))) |
20 | 19 | 2ralbidv 2972 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))) |
21 | 16, 20 | 3anbi13d 1393 |
. . . . . 6
⊢ (𝑡 = 𝑇 → ((𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))) ↔ (𝑇:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |
22 | 15, 21 | fvopab5 6217 |
. . . . 5
⊢ (𝑇 ∈ V → ({〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}‘𝑇) = (℩𝑠(𝑇:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |
23 | 14, 22 | syl 17 |
. . . 4
⊢ (𝑇:𝑋⟶𝑌 → ({〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}‘𝑇) = (℩𝑠(𝑇:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |
24 | | 3anass 1035 |
. . . . . 6
⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))) ↔ (𝑇:𝑋⟶𝑌 ∧ (𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |
25 | 24 | baib 942 |
. . . . 5
⊢ (𝑇:𝑋⟶𝑌 → ((𝑇:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))) ↔ (𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |
26 | 25 | iotabidv 5789 |
. . . 4
⊢ (𝑇:𝑋⟶𝑌 → (℩𝑠(𝑇:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))) = (℩𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |
27 | 23, 26 | eqtrd 2644 |
. . 3
⊢ (𝑇:𝑋⟶𝑌 → ({〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}‘𝑇) = (℩𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |
28 | 27 | 3ad2ant3 1077 |
. 2
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ NrmCVec
∧ 𝑇:𝑋⟶𝑌) → ({〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}‘𝑇) = (℩𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |
29 | 10, 28 | eqtrd 2644 |
1
⊢ ((𝑈 ∈ CPreHilOLD
∧ 𝑊 ∈ NrmCVec
∧ 𝑇:𝑋⟶𝑌) → (𝐴‘𝑇) = (℩𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |