cdlemg11b - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdlemg11b		Structured version Visualization version GIF version

Theorem cdlemg11b 41516

Description: TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)

**Hypotheses**
Ref	Expression
cdlemg8.l	⊢ ≤ = (le‘𝐾)
cdlemg8.j	⊢ ∨ = (join‘𝐾)
cdlemg8.m	⊢ ∧ = (meet‘𝐾)
cdlemg8.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemg8.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemg8.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemg10.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
cdlemg11b	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∨ 𝑄) ≠ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)))

**Proof of Theorem cdlemg11b**
Step	Hyp	Ref	Expression
1		simp33 1230	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))
2		simpl1 1210	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3		simpl31 1273	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝐺 ∈ 𝑇)
4		simpl2l 1245	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
5		cdlemg8.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
6		cdlemg8.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
7		cdlemg8.m	. . . . . . 7 ⊢ ∧ = (meet‘𝐾)
8		cdlemg8.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
9		cdlemg8.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
10		cdlemg8.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
11		cdlemg10.r	. . . . . . 7 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
12	5, 6, 7, 8, 9, 10, 11	trlval2 41037	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊))
13	2, 3, 4, 12	syl3anc 1398	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊))
14		eqid 2760	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
15		simpl1l 1243	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝐾 ∈ HL)
16	15	hllatd 40238	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝐾 ∈ Lat)
17		simp2ll 1259	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → 𝑃 ∈ 𝐴)
18	17	adantr 486	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑃 ∈ 𝐴)
19	14, 8	atbase 40163	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
20	18, 19	syl 18	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑃 ∈ (Base‘𝐾))
21	14, 9, 10	ltrncl 40999	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝐺‘𝑃) ∈ (Base‘𝐾))
22	2, 3, 20, 21	syl3anc 1398	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑃) ∈ (Base‘𝐾))
23	14, 6	latjcl 18528	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐺‘𝑃) ∈ (Base‘𝐾)) → (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾))
24	16, 20, 22, 23	syl3anc 1398	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾))
25		simpl1r 1244	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑊 ∈ 𝐻)
26	14, 9	lhpbase 40872	. . . . . . . 8 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
27	25, 26	syl 18	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑊 ∈ (Base‘𝐾))
28	14, 7	latmcl 18529	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ∈ (Base‘𝐾))
29	16, 24, 27, 28	syl3anc 1398	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ∈ (Base‘𝐾))
30		simpl2r 1246	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑄 ∈ 𝐴)
31	14, 8	atbase 40163	. . . . . . . 8 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
32	30, 31	syl 18	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑄 ∈ (Base‘𝐾))
33	14, 6	latjcl 18528	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
34	16, 20, 32, 33	syl3anc 1398	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
35	14, 5, 7	latmle1 18553	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ (𝐺‘𝑃)))
36	16, 24, 27, 35	syl3anc 1398	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ (𝐺‘𝑃)))
37	14, 5, 6	latlej1 18537	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → 𝑃 ≤ (𝑃 ∨ 𝑄))
38	16, 20, 32, 37	syl3anc 1398	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑃 ≤ (𝑃 ∨ 𝑄))
39	14, 9, 10	ltrncl 40999	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑄 ∈ (Base‘𝐾)) → (𝐺‘𝑄) ∈ (Base‘𝐾))
40	2, 3, 32, 39	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑄) ∈ (Base‘𝐾))
41	14, 5, 6	latlej1 18537	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝐺‘𝑃) ∈ (Base‘𝐾) ∧ (𝐺‘𝑄) ∈ (Base‘𝐾)) → (𝐺‘𝑃) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)))
42	16, 22, 40, 41	syl3anc 1398	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑃) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)))
43		simpr 490	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄)))
44	42, 43	breqtrrd 5133	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑃) ≤ (𝑃 ∨ 𝑄))
45	14, 5, 6	latjle12 18539	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ (𝐺‘𝑃) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝑃 ≤ (𝑃 ∨ 𝑄) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ 𝑄)))
46	16, 20, 22, 34, 45	syl13anc 1399	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ≤ (𝑃 ∨ 𝑄) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ 𝑄)))
47	38, 44, 46	mpbi2and 725	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ 𝑄))
48	14, 5, 16, 29, 24, 34, 36, 47	lattrd 18535	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ 𝑄))
49	13, 48	eqbrtrd 5127	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))
50	49	ex 418	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄)) → (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄)))
51	50	necon3bd 2969	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) → (𝑃 ∨ 𝑄) ≠ ((𝐺‘𝑃) ∨ (𝐺‘𝑄))))
52	1, 51	mpd 16	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∨ 𝑄) ≠ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 class class class wbr 5103 ‘cfv 6533 (class class class)co 7414 Basecbs 17302 lecple 17350 joincjn 18400 meetcmee 18401 Latclat 18520 Atomscatm 40137 HLchlt 40224 LHypclh 40858 LTrncltrn 40975 trLctrl 41032

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-map 8829 df-poset 18402 df-lub 18433 df-glb 18434 df-join 18435 df-meet 18436 df-lat 18521 df-ats 40141 df-atl 40172 df-cvlat 40196 df-hlat 40225 df-lhyp 40862 df-laut 40863 df-ldil 40978 df-ltrn 40979 df-trl 41033

This theorem is used by: cdlemg12b 41518

W3C validator