Metamath Proof Explorer


Theorem mapdsord

Description: Strong ordering property of themap defined by df-mapd . (Contributed by NM, 13-Mar-2015)

Ref Expression
Hypotheses mapdcnvcl.h 𝐻 = ( LHyp ‘ 𝐾 )
mapdcnvcl.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdcnvcl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdcnvcl.s 𝑆 = ( LSubSp ‘ 𝑈 )
mapdcnvcl.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
mapdcl.x ( 𝜑𝑋𝑆 )
mapdsord.x ( 𝜑𝑌𝑆 )
Assertion mapdsord ( 𝜑 → ( ( 𝑀𝑋 ) ⊊ ( 𝑀𝑌 ) ↔ 𝑋𝑌 ) )

Proof

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