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