Step | Hyp | Ref
| Expression |
1 | | ajfval.5 |
. 2
⊢ 𝐴 = (𝑈adj𝑊) |
2 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → (BaseSet‘𝑢) = (BaseSet‘𝑈)) |
3 | | ajfval.1 |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . 6
⊢ (𝑢 = 𝑈 → (BaseSet‘𝑢) = 𝑋) |
5 | 4 | feq2d 6490 |
. . . . 5
⊢ (𝑢 = 𝑈 → (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ↔ 𝑡:𝑋⟶(BaseSet‘𝑤))) |
6 | 4 | feq3d 6491 |
. . . . 5
⊢ (𝑢 = 𝑈 → (𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ↔ 𝑠:(BaseSet‘𝑤)⟶𝑋)) |
7 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑈 →
(·𝑖OLD‘𝑢) =
(·𝑖OLD‘𝑈)) |
8 | | ajfval.3 |
. . . . . . . . . 10
⊢ 𝑃 =
(·𝑖OLD‘𝑈) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝑢 = 𝑈 →
(·𝑖OLD‘𝑢) = 𝑃) |
10 | 9 | oveqd 7187 |
. . . . . . . 8
⊢ (𝑢 = 𝑈 → (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) = (𝑥𝑃(𝑠‘𝑦))) |
11 | 10 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → (((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) ↔ ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)))) |
12 | 11 | ralbidv 3109 |
. . . . . 6
⊢ (𝑢 = 𝑈 → (∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) ↔ ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)))) |
13 | 4, 12 | raleqbidv 3304 |
. . . . 5
⊢ (𝑢 = 𝑈 → (∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)))) |
14 | 5, 6, 13 | 3anbi123d 1437 |
. . . 4
⊢ (𝑢 = 𝑈 → ((𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |
15 | 14 | opabbidv 5096 |
. . 3
⊢ (𝑢 = 𝑈 → {〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))} = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) |
16 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (BaseSet‘𝑤) = (BaseSet‘𝑊)) |
17 | | ajfval.2 |
. . . . . . 7
⊢ 𝑌 = (BaseSet‘𝑊) |
18 | 16, 17 | eqtr4di 2791 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (BaseSet‘𝑤) = 𝑌) |
19 | 18 | feq3d 6491 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑡:𝑋⟶(BaseSet‘𝑤) ↔ 𝑡:𝑋⟶𝑌)) |
20 | 18 | feq2d 6490 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑠:(BaseSet‘𝑤)⟶𝑋 ↔ 𝑠:𝑌⟶𝑋)) |
21 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 →
(·𝑖OLD‘𝑤) =
(·𝑖OLD‘𝑊)) |
22 | | ajfval.4 |
. . . . . . . . . 10
⊢ 𝑄 =
(·𝑖OLD‘𝑊) |
23 | 21, 22 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 →
(·𝑖OLD‘𝑤) = 𝑄) |
24 | 23 | oveqd 7187 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = ((𝑡‘𝑥)𝑄𝑦)) |
25 | 24 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)) ↔ ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))) |
26 | 18, 25 | raleqbidv 3304 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)) ↔ ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))) |
27 | 26 | ralbidv 3109 |
. . . . 5
⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))) |
28 | 19, 20, 27 | 3anbi123d 1437 |
. . . 4
⊢ (𝑤 = 𝑊 → ((𝑡:𝑋⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦))) ↔ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) |
29 | 28 | opabbidv 5096 |
. . 3
⊢ (𝑤 = 𝑊 → {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)))} = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) |
30 | | df-aj 28685 |
. . 3
⊢ adj =
(𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦
{〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}) |
31 | | ovex 7203 |
. . . . 5
⊢ (𝑌 ↑m 𝑋) ∈ V |
32 | | ovex 7203 |
. . . . 5
⊢ (𝑋 ↑m 𝑌) ∈ V |
33 | 31, 32 | xpex 7494 |
. . . 4
⊢ ((𝑌 ↑m 𝑋) × (𝑋 ↑m 𝑌)) ∈ V |
34 | 17 | fvexi 6688 |
. . . . . . . . . 10
⊢ 𝑌 ∈ V |
35 | 3 | fvexi 6688 |
. . . . . . . . . 10
⊢ 𝑋 ∈ V |
36 | 34, 35 | elmap 8481 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝑌 ↑m 𝑋) ↔ 𝑡:𝑋⟶𝑌) |
37 | 35, 34 | elmap 8481 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝑋 ↑m 𝑌) ↔ 𝑠:𝑌⟶𝑋) |
38 | 36, 37 | anbi12i 630 |
. . . . . . . 8
⊢ ((𝑡 ∈ (𝑌 ↑m 𝑋) ∧ 𝑠 ∈ (𝑋 ↑m 𝑌)) ↔ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋)) |
39 | 38 | biimpri 231 |
. . . . . . 7
⊢ ((𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋) → (𝑡 ∈ (𝑌 ↑m 𝑋) ∧ 𝑠 ∈ (𝑋 ↑m 𝑌))) |
40 | 39 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))) → (𝑡 ∈ (𝑌 ↑m 𝑋) ∧ 𝑠 ∈ (𝑋 ↑m 𝑌))) |
41 | 40 | ssopab2i 5405 |
. . . . 5
⊢
{〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))} ⊆ {〈𝑡, 𝑠〉 ∣ (𝑡 ∈ (𝑌 ↑m 𝑋) ∧ 𝑠 ∈ (𝑋 ↑m 𝑌))} |
42 | | df-xp 5531 |
. . . . 5
⊢ ((𝑌 ↑m 𝑋) × (𝑋 ↑m 𝑌)) = {〈𝑡, 𝑠〉 ∣ (𝑡 ∈ (𝑌 ↑m 𝑋) ∧ 𝑠 ∈ (𝑋 ↑m 𝑌))} |
43 | 41, 42 | sseqtrri 3914 |
. . . 4
⊢
{〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))} ⊆ ((𝑌 ↑m 𝑋) × (𝑋 ↑m 𝑌)) |
44 | 33, 43 | ssexi 5190 |
. . 3
⊢
{〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))} ∈ V |
45 | 15, 29, 30, 44 | ovmpo 7325 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑈adj𝑊) = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) |
46 | 1, 45 | syl5eq 2785 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐴 = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) |