| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ajfval.5 | . 2
⊢ 𝐴 = (𝑈adj𝑊) | 
| 2 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑢 = 𝑈 → (BaseSet‘𝑢) = (BaseSet‘𝑈)) | 
| 3 |  | ajfval.1 | . . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) | 
| 4 | 2, 3 | eqtr4di 2795 | . . . . . 6
⊢ (𝑢 = 𝑈 → (BaseSet‘𝑢) = 𝑋) | 
| 5 | 4 | feq2d 6722 | . . . . 5
⊢ (𝑢 = 𝑈 → (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ↔ 𝑡:𝑋⟶(BaseSet‘𝑤))) | 
| 6 | 4 | feq3d 6723 | . . . . 5
⊢ (𝑢 = 𝑈 → (𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ↔ 𝑠:(BaseSet‘𝑤)⟶𝑋)) | 
| 7 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑢 = 𝑈 →
(·𝑖OLD‘𝑢) =
(·𝑖OLD‘𝑈)) | 
| 8 |  | ajfval.3 | . . . . . . . . . 10
⊢ 𝑃 =
(·𝑖OLD‘𝑈) | 
| 9 | 7, 8 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝑢 = 𝑈 →
(·𝑖OLD‘𝑢) = 𝑃) | 
| 10 | 9 | oveqd 7448 | . . . . . . . 8
⊢ (𝑢 = 𝑈 → (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) = (𝑥𝑃(𝑠‘𝑦))) | 
| 11 | 10 | eqeq2d 2748 | . . . . . . 7
⊢ (𝑢 = 𝑈 → (((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) ↔ ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)))) | 
| 12 | 11 | ralbidv 3178 | . . . . . 6
⊢ (𝑢 = 𝑈 → (∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) ↔ ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)))) | 
| 13 | 4, 12 | raleqbidv 3346 | . . . . 5
⊢ (𝑢 = 𝑈 → (∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)))) | 
| 14 | 5, 6, 13 | 3anbi123d 1438 | . . . 4
⊢ (𝑢 = 𝑈 → ((𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦))))) | 
| 15 | 14 | opabbidv 5209 | . . 3
⊢ (𝑢 = 𝑈 → {〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))} = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) | 
| 16 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑤 = 𝑊 → (BaseSet‘𝑤) = (BaseSet‘𝑊)) | 
| 17 |  | ajfval.2 | . . . . . . 7
⊢ 𝑌 = (BaseSet‘𝑊) | 
| 18 | 16, 17 | eqtr4di 2795 | . . . . . 6
⊢ (𝑤 = 𝑊 → (BaseSet‘𝑤) = 𝑌) | 
| 19 | 18 | feq3d 6723 | . . . . 5
⊢ (𝑤 = 𝑊 → (𝑡:𝑋⟶(BaseSet‘𝑤) ↔ 𝑡:𝑋⟶𝑌)) | 
| 20 | 18 | feq2d 6722 | . . . . 5
⊢ (𝑤 = 𝑊 → (𝑠:(BaseSet‘𝑤)⟶𝑋 ↔ 𝑠:𝑌⟶𝑋)) | 
| 21 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 →
(·𝑖OLD‘𝑤) =
(·𝑖OLD‘𝑊)) | 
| 22 |  | ajfval.4 | . . . . . . . . . 10
⊢ 𝑄 =
(·𝑖OLD‘𝑊) | 
| 23 | 21, 22 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝑤 = 𝑊 →
(·𝑖OLD‘𝑤) = 𝑄) | 
| 24 | 23 | oveqd 7448 | . . . . . . . 8
⊢ (𝑤 = 𝑊 → ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = ((𝑡‘𝑥)𝑄𝑦)) | 
| 25 | 24 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑤 = 𝑊 → (((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)) ↔ ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))) | 
| 26 | 18, 25 | raleqbidv 3346 | . . . . . 6
⊢ (𝑤 = 𝑊 → (∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)) ↔ ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))) | 
| 27 | 26 | ralbidv 3178 | . . . . 5
⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))) | 
| 28 | 19, 20, 27 | 3anbi123d 1438 | . . . 4
⊢ (𝑤 = 𝑊 → ((𝑡:𝑋⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦))) ↔ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) | 
| 29 | 28 | opabbidv 5209 | . . 3
⊢ (𝑤 = 𝑊 → {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥𝑃(𝑠‘𝑦)))} = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) | 
| 30 |  | df-aj 30769 | . . 3
⊢ adj =
(𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦
{〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}) | 
| 31 |  | ovex 7464 | . . . . 5
⊢ (𝑌 ↑m 𝑋) ∈ V | 
| 32 |  | ovex 7464 | . . . . 5
⊢ (𝑋 ↑m 𝑌) ∈ V | 
| 33 | 31, 32 | xpex 7773 | . . . 4
⊢ ((𝑌 ↑m 𝑋) × (𝑋 ↑m 𝑌)) ∈ V | 
| 34 | 17 | fvexi 6920 | . . . . . . . . . 10
⊢ 𝑌 ∈ V | 
| 35 | 3 | fvexi 6920 | . . . . . . . . . 10
⊢ 𝑋 ∈ V | 
| 36 | 34, 35 | elmap 8911 | . . . . . . . . 9
⊢ (𝑡 ∈ (𝑌 ↑m 𝑋) ↔ 𝑡:𝑋⟶𝑌) | 
| 37 | 35, 34 | elmap 8911 | . . . . . . . . 9
⊢ (𝑠 ∈ (𝑋 ↑m 𝑌) ↔ 𝑠:𝑌⟶𝑋) | 
| 38 | 36, 37 | anbi12i 628 | . . . . . . . 8
⊢ ((𝑡 ∈ (𝑌 ↑m 𝑋) ∧ 𝑠 ∈ (𝑋 ↑m 𝑌)) ↔ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋)) | 
| 39 | 38 | biimpri 228 | . . . . . . 7
⊢ ((𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋) → (𝑡 ∈ (𝑌 ↑m 𝑋) ∧ 𝑠 ∈ (𝑋 ↑m 𝑌))) | 
| 40 | 39 | 3adant3 1133 | . . . . . 6
⊢ ((𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))) → (𝑡 ∈ (𝑌 ↑m 𝑋) ∧ 𝑠 ∈ (𝑋 ↑m 𝑌))) | 
| 41 | 40 | ssopab2i 5555 | . . . . 5
⊢
{〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))} ⊆ {〈𝑡, 𝑠〉 ∣ (𝑡 ∈ (𝑌 ↑m 𝑋) ∧ 𝑠 ∈ (𝑋 ↑m 𝑌))} | 
| 42 |  | df-xp 5691 | . . . . 5
⊢ ((𝑌 ↑m 𝑋) × (𝑋 ↑m 𝑌)) = {〈𝑡, 𝑠〉 ∣ (𝑡 ∈ (𝑌 ↑m 𝑋) ∧ 𝑠 ∈ (𝑋 ↑m 𝑌))} | 
| 43 | 41, 42 | sseqtrri 4033 | . . . 4
⊢
{〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))} ⊆ ((𝑌 ↑m 𝑋) × (𝑋 ↑m 𝑌)) | 
| 44 | 33, 43 | ssexi 5322 | . . 3
⊢
{〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))} ∈ V | 
| 45 | 15, 29, 30, 44 | ovmpo 7593 | . 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑈adj𝑊) = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) | 
| 46 | 1, 45 | eqtrid 2789 | 1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐴 = {〈𝑡, 𝑠〉 ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) |