dihord2a

Description: Part of proof after Lemma N of Crawley p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014)

	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 ‘ 𝑈 )
Assertion	dihord2a	⊢ ( ( ( ( 𝐾 ∈ 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		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12	6 9 11	dvhlmod	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → 𝑈 ∈ LMod )
13		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
14	13	lsssssubg	⊢ ( 𝑈 ∈ LMod → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
15	12 14	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
16		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
17	2 5 6 9 8 13	diclss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐽 ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) )
18	11 16 17	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝐽 ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) )
19	15 18	sseldd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝐽 ‘ 𝑄 ) ∈ ( SubGrp ‘ 𝑈 ) )
20		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → 𝐾 ∈ HL )
21	20	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → 𝐾 ∈ Lat )
22		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → 𝑋 ∈ 𝐵 )
23		simp11r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → 𝑊 ∈ 𝐻 )
24	1 6	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
25	23 24	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → 𝑊 ∈ 𝐵 )
26	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
27	21 22 25 26	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
28	1 2 4	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 )
29	21 22 25 28	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 )
30	1 2 6 9 7 13	diblss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
31	11 27 29 30	syl12anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
32	15 31	sseldd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
33	10	lsmub1	⊢ ( ( ( 𝐽 ‘ 𝑄 ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ∈ ( SubGrp ‘ 𝑈 ) ) → ( 𝐽 ‘ 𝑄 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )
34	19 32 33	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝐽 ‘ 𝑄 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )
35		simp33	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) )
36	34 35	sstrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝐽 ‘ 𝑄 ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) )
37		simp13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
38		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → 𝑌 ∈ 𝐵 )
39	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 )
40	21 38 25 39	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 )
41	1 2 4	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑊 ) ≤ 𝑊 )
42	21 38 25 41	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝑌 ∧ 𝑊 ) ≤ 𝑊 )
43	40 42	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑊 ) ≤ 𝑊 ) )
44	1 2 3 5 6 7 8 9 10	cdlemn	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( ( 𝑌 ∧ 𝑊 ) ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑊 ) ≤ 𝑊 ) ) ) → ( 𝑄 ≤ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) ↔ ( 𝐽 ‘ 𝑄 ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) )
45	11 37 16 43 44	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → ( 𝑄 ≤ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) ↔ ( 𝐽 ‘ 𝑄 ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) )
46	36 45	mpbird	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) = 𝑌 ∧ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑌 ∧ 𝑊 ) ) ) ) ) → 𝑄 ≤ ( 𝑅 ∨ ( 𝑌 ∧ 𝑊 ) ) )

Metamath Proof Explorer

Theorem dihord2a

Proof