Metamath Proof Explorer

Theorem 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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ) → ⟨ 𝑓 , 𝑂 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) )