Step |
Hyp |
Ref |
Expression |
1 |
|
mapdcnvord.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
mapdcnvord.m |
⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
mapdcnvord.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
4 |
|
mapdcnvord.x |
⊢ ( 𝜑 → 𝑋 ∈ ran 𝑀 ) |
5 |
|
mapdcnvord.y |
⊢ ( 𝜑 → 𝑌 ∈ ran 𝑀 ) |
6 |
|
eqid |
⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
7 |
|
eqid |
⊢ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) |
8 |
1 2 6 7 3 4
|
mapdcnvcl |
⊢ ( 𝜑 → ( ◡ 𝑀 ‘ 𝑋 ) ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
9 |
1 2 6 7 3 5
|
mapdcnvcl |
⊢ ( 𝜑 → ( ◡ 𝑀 ‘ 𝑌 ) ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
10 |
1 6 7 2 3 8 9
|
mapdord |
⊢ ( 𝜑 → ( ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑋 ) ) ⊆ ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑌 ) ) ↔ ( ◡ 𝑀 ‘ 𝑋 ) ⊆ ( ◡ 𝑀 ‘ 𝑌 ) ) ) |
11 |
1 2 3 4
|
mapdcnvid2 |
⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑋 ) ) = 𝑋 ) |
12 |
1 2 3 5
|
mapdcnvid2 |
⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑌 ) ) = 𝑌 ) |
13 |
11 12
|
sseq12d |
⊢ ( 𝜑 → ( ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑋 ) ) ⊆ ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑌 ) ) ↔ 𝑋 ⊆ 𝑌 ) ) |
14 |
10 13
|
bitr3d |
⊢ ( 𝜑 → ( ( ◡ 𝑀 ‘ 𝑋 ) ⊆ ( ◡ 𝑀 ‘ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) ) |