Theorem dihord6a

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014)

	Ref	Expression
Hypotheses	dihord3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dihord3.l	⊢ ≤ = ( le ‘ 𝐾 )
	dihord3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihord3.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dihord6a	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ) → 𝑋 ≤ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		dihord3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dihord3.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dihord3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dihord3.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
6		eqid	⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
7		eqid	⊢ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) )
8		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
9		eqid	⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
10		eqid	⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
11		eqid	⊢ ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
12		eqid	⊢ ( ℩ ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( ℎ ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 ) = ( ℩ ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( ℎ ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑞 )
13	1 2 5 3 6 7 8 9 4 10 11 12	dihord6apre	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ) → 𝑋 ≤ 𝑌 )