Step |
Hyp |
Ref |
Expression |
1 |
|
dibcl.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
dibcl.i |
⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
relxp |
⊢ Rel ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) |
4 |
|
eqid |
⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
1 4 2
|
dibdiadm |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ) |
6 |
5
|
eleq2d |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
7 |
6
|
biimpa |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ) |
8 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
9 |
|
eqid |
⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
10 |
|
eqid |
⊢ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) |
11 |
8 1 9 10 4 2
|
dibval |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) ) |
12 |
7 11
|
syldan |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) ) |
13 |
12
|
releqd |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) ) ) |
14 |
3 13
|
mpbiri |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → Rel ( 𝐼 ‘ 𝑋 ) ) |
15 |
|
rel0 |
⊢ Rel ∅ |
16 |
|
ndmfv |
⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑋 ) = ∅ ) |
17 |
16
|
releqd |
⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel ∅ ) ) |
18 |
15 17
|
mpbiri |
⊢ ( ¬ 𝑋 ∈ dom 𝐼 → Rel ( 𝐼 ‘ 𝑋 ) ) |
19 |
18
|
adantl |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ¬ 𝑋 ∈ dom 𝐼 ) → Rel ( 𝐼 ‘ 𝑋 ) ) |
20 |
14 19
|
pm2.61dan |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) ) |