Metamath Proof Explorer


Theorem mapdord

Description: Ordering property of the map defined by df-mapd . Property (b) of Baer p. 40. (Contributed by NM, 27-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 mapdord.h 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdord.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdord.s 𝑆 = ( LSubSp ‘ 𝑈 )
4 mapdord.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
5 mapdord.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 mapdord.x ( 𝜑𝑋𝑆 )
7 mapdord.y ( 𝜑𝑌𝑆 )
8 eqid ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
9 eqid ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
10 eqid ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
11 eqid ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
12 eqid ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
13 eqid { 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) ∈ ( LSHyp ‘ 𝑈 ) } = { 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) ∈ ( LSHyp ‘ 𝑈 ) }
14 eqid { 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) } = { 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) }
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 mapdordlem2 ( 𝜑 → ( ( 𝑀𝑋 ) ⊆ ( 𝑀𝑌 ) ↔ 𝑋𝑌 ) )