Step |
Hyp |
Ref |
Expression |
1 |
|
mapdcnvcl.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
mapdcnvcl.m |
⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
mapdcnvcl.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
mapdcnvcl.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑈 ) |
5 |
|
mapdcnvcl.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
6 |
|
mapdcl.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑆 ) |
7 |
|
mapdsord.x |
⊢ ( 𝜑 → 𝑌 ∈ 𝑆 ) |
8 |
1 3 4 2 5 6 7
|
mapdord |
⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) ) |
9 |
1 3 4 2 5 6 7
|
mapd11 |
⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) = ( 𝑀 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) ) |
10 |
9
|
necon3bid |
⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ≠ ( 𝑀 ‘ 𝑌 ) ↔ 𝑋 ≠ 𝑌 ) ) |
11 |
8 10
|
anbi12d |
⊢ ( 𝜑 → ( ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ 𝑌 ) ∧ ( 𝑀 ‘ 𝑋 ) ≠ ( 𝑀 ‘ 𝑌 ) ) ↔ ( 𝑋 ⊆ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) ) |
12 |
|
df-pss |
⊢ ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑌 ) ↔ ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ 𝑌 ) ∧ ( 𝑀 ‘ 𝑋 ) ≠ ( 𝑀 ‘ 𝑌 ) ) ) |
13 |
|
df-pss |
⊢ ( 𝑋 ⊊ 𝑌 ↔ ( 𝑋 ⊆ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) |
14 |
11 12 13
|
3bitr4g |
⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑌 ) ↔ 𝑋 ⊊ 𝑌 ) ) |