Metamath Proof Explorer


Theorem mapdcnvordN

Description: Ordering property of the converse of the map defined by df-mapd . (Contributed by NM, 13-Mar-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdcnvord.h 𝐻 = ( LHyp ‘ 𝐾 )
mapdcnvord.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdcnvord.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
mapdcnvord.x ( 𝜑𝑋 ∈ ran 𝑀 )
mapdcnvord.y ( 𝜑𝑌 ∈ ran 𝑀 )
Assertion mapdcnvordN ( 𝜑 → ( ( 𝑀𝑋 ) ⊆ ( 𝑀𝑌 ) ↔ 𝑋𝑌 ) )

Proof

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 ( 𝜑 → ( ( 𝑀𝑋 ) ⊆ ( 𝑀𝑌 ) ↔ 𝑋𝑌 ) )