dihord2cN

Description: Part of proof after Lemma N of Crawley p. 122. Reverse ordering property. TODO: needed? shorten other proof with it? (Contributed by NM, 3-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihjust.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dihjust.l	⊢ ≤ = ( le ‘ 𝐾 )
	dihjust.j	⊢ ∨ = ( join ‘ 𝐾 )
	dihjust.m	⊢ ∧ = ( meet ‘ 𝐾 )
	dihjust.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dihjust.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihjust.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
	dihjust.J	⊢ 𝐽 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
	dihjust.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dihjust.s	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	dihord2c.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dihord2c.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	dihord2c.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion	dihord2cN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → ⟨ 𝑓 , 𝑂 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihjust.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dihjust.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dihjust.j	⊢ ∨ = ( join ‘ 𝐾 )
4		dihjust.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		dihjust.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		dihjust.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		dihjust.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
8		dihjust.J	⊢ 𝐽 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
9		dihjust.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
10		dihjust.s	⊢ ⊕ = ( LSSum ‘ 𝑈 )
11		dihord2c.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
12		dihord2c.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
13		dihord2c.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
14		simp3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) )
15		eqidd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → 𝑂 = 𝑂 )
16		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → 𝐾 ∈ HL )
18	17	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → 𝐾 ∈ Lat )
19		simp2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → 𝑋 ∈ 𝐵 )
20		simp1r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → 𝑊 ∈ 𝐻 )
21	1 6	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
22	20 21	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → 𝑊 ∈ 𝐵 )
23	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
24	18 19 22 23	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
25	1 2 4	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 )
26	18 19 22 25	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 )
27	1 2 6 11 12 13 7	dibopelval3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑂 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑂 = 𝑂 ) ) )
28	16 24 26 27	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → ( ⟨ 𝑓 , 𝑂 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑂 = 𝑂 ) ) )
29	14 15 28	mpbir2and	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → ⟨ 𝑓 , 𝑂 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) )

Metamath Proof Explorer

Theorem dihord2cN

Proof