Theorem cdlemg10bALTN

Description: TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? TODO: Compare this proof to cdlemg2m and pick best, if moved to ltrn* area. (Contributed by NM, 4-May-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemg8.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemg8.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemg8.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemg8.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemg8.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemg8.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion	cdlemg10bALTN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ 𝑄 ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemg8.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemg8.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdlemg8.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdlemg8.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdlemg8.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdlemg8.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		simp11	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
8		simp12	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
9	7 8	jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		3simpc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
11		simp13	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
12		eqid	⊢ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
13	5 6 1 2 4 3 12	cdlemg2k	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ 𝑄 ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
14	9 10 11 13	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ 𝑄 ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
15	14	oveq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ 𝑄 ) ) ∧ 𝑊 ) = ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ 𝑊 ) )
16		simp2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
17	1 4 5 6	ltrnel	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
18	9 11 16 17	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
19		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
20	1 3 19 4 5	lhpmat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
21	9 18 20	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
22	21	oveq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∧ 𝑊 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 0. ‘ 𝐾 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
23		simp2l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
24	1 4 5 6	ltrnat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 )
25	9 11 23 24	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 )
26	7	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
27		simp3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝑄 ∈ 𝐴 )
28		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
29	28 2 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
30	7 23 27 29	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
31	28 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
32	8 31	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
33	28 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
34	26 30 32 33	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
35	28 1 3	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
36	26 30 32 35	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
37	28 1 2 3 4	atmod4i2	⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 ) → ( ( ( 𝐹 ‘ 𝑃 ) ∧ 𝑊 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ 𝑊 ) )
38	7 25 34 32 36 37	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∧ 𝑊 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ 𝑊 ) )
39		hlol	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
40	7 39	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
41	28 2 19	olj02	⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
42	40 34 41	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 0. ‘ 𝐾 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
43	22 38 42	3eqtr3d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
44	15 43	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ 𝑄 ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )