cdlemn11pre

Description: Part of proof of Lemma N of Crawley p. 121 line 37. TODO: combine cdlemn11a , cdlemn11b , cdlemn11c , cdlemn11pre into one? (Contributed by NM, 27-Feb-2014)

	Ref	Expression
Hypotheses	cdlemn11a.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdlemn11a.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemn11a.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemn11a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemn11a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemn11a.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
	cdlemn11a.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	cdlemn11a.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemn11a.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	cdlemn11a.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	cdlemn11a.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
	cdlemn11a.J	⊢ 𝐽 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
	cdlemn11a.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	cdlemn11a.d	⊢ + = ( +_g ‘ 𝑈 )
	cdlemn11a.s	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	cdlemn11a.f	⊢ 𝐹 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑄 )
	cdlemn11a.g	⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑁 )
Assertion	cdlemn11pre	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemn11a.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdlemn11a.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdlemn11a.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdlemn11a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdlemn11a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdlemn11a.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
7		cdlemn11a.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
8		cdlemn11a.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
9		cdlemn11a.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
10		cdlemn11a.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
11		cdlemn11a.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
12		cdlemn11a.J	⊢ 𝐽 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
13		cdlemn11a.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
14		cdlemn11a.d	⊢ + = ( +_g ‘ 𝑈 )
15		cdlemn11a.s	⊢ ⊕ = ( LSSum ‘ 𝑈 )
16		cdlemn11a.f	⊢ 𝐹 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑄 )
17		cdlemn11a.g	⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑁 )
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	cdlemn11c	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ∃ 𝑦 ∈ ( 𝐽 ‘ 𝑄 ) ∃ 𝑧 ∈ ( 𝐼 ‘ 𝑋 ) ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) )
19		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
20		simp21	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
21	2 4 5 6 8 10 12 16	dicelval3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑦 ∈ ( 𝐽 ‘ 𝑄 ) ↔ ∃ 𝑠 ∈ 𝐸 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ) )
22	19 20 21	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑦 ∈ ( 𝐽 ‘ 𝑄 ) ↔ ∃ 𝑠 ∈ 𝐸 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ) )
23		simp23	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) )
24	1 2 5 8 9 7 11	dibelval3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝑧 ∈ ( 𝐼 ‘ 𝑋 ) ↔ ∃ 𝑔 ∈ 𝑇 ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) )
25	19 23 24	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑧 ∈ ( 𝐼 ‘ 𝑋 ) ↔ ∃ 𝑔 ∈ 𝑇 ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) )
26	22 25	anbi12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑦 ∈ ( 𝐽 ‘ 𝑄 ) ∧ 𝑧 ∈ ( 𝐼 ‘ 𝑋 ) ) ↔ ( ∃ 𝑠 ∈ 𝐸 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ ∃ 𝑔 ∈ 𝑇 ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) ) )
27		reeanv	⊢ ( ∃ 𝑠 ∈ 𝐸 ∃ 𝑔 ∈ 𝑇 ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) ↔ ( ∃ 𝑠 ∈ 𝐸 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ ∃ 𝑔 ∈ 𝑇 ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) )
28		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) ∧ ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
29		simpl21	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) ∧ ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
30		simpl22	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) ∧ ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) )
31		simpl23	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) ∧ ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) )
32		simpr1r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) ∧ ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → 𝑔 ∈ 𝑇 )
33		simpr1l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) ∧ ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → 𝑠 ∈ 𝐸 )
34		simpr3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) ∧ ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) )
35	1 2 4 5 6 7 8 10 13 14 16 17	cdlemn9	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑔 ‘ 𝑄 ) = 𝑁 )
36	28 29 30 33 32 34 35	syl123anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) ∧ ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑔 ‘ 𝑄 ) = 𝑁 )
37		simpr2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) ∧ ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 )
38	1 2 3 4 5 8 9	cdlemn10	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑔 ‘ 𝑄 ) = 𝑁 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) )
39	28 29 30 31 32 36 37 38	syl133anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) ∧ ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ∧ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) )
40	39	3exp2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) ) )
41		oveq12	⊢ ( ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( 𝑦 + 𝑧 ) = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) )
42	41	eqeq2d	⊢ ( ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) ↔ ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) ) )
43	42	imbi1d	⊢ ( ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ↔ ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) )
44	43	imbi2d	⊢ ( ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) ↔ ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) ) )
45	44	biimprd	⊢ ( ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) → ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) ) )
46	45	com23	⊢ ( ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) ) )
47	46	impr	⊢ ( ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) → ( ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) )
48	47	com12	⊢ ( ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ + ⟨ 𝑔 , 𝑂 ⟩ ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) → ( ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) )
49	40 48	syl6	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) ) )
50	49	rexlimdvv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( ∃ 𝑠 ∈ 𝐸 ∃ 𝑔 ∈ 𝑇 ( 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) )
51	27 50	biimtrrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ∃ 𝑠 ∈ 𝐸 𝑦 = ⟨ ( 𝑠 ‘ 𝐹 ) , 𝑠 ⟩ ∧ ∃ 𝑔 ∈ 𝑇 ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) ) → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) )
52	26 51	sylbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑦 ∈ ( 𝐽 ‘ 𝑄 ) ∧ 𝑧 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) ) )
53	52	rexlimdvv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → ( ∃ 𝑦 ∈ ( 𝐽 ‘ 𝑄 ) ∃ 𝑧 ∈ ( 𝐼 ‘ 𝑋 ) ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( 𝑦 + 𝑧 ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) ) )
54	18 53	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐽 ‘ 𝑁 ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑁 ≤ ( 𝑄 ∨ 𝑋 ) )

Metamath Proof Explorer

Theorem cdlemn11pre

Proof