cdleme22e

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 4th line on p. 115. F , N , O represent f(z), f_z(s), f_z(t) respectively. When t \/ v = p \/ q, f_z(s) <_ f_z(t) \/ v. (Contributed by NM, 6-Dec-2012)

	Ref	Expression
Hypotheses	cdleme22.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme22.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme22.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme22.a	$⊢ A = Atoms (K)$
	cdleme22.h	$⊢ H = LHyp (K)$
	cdleme22e.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme22e.f	$⊢ F = (z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W))$
	cdleme22e.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} z) \underset{˙}{\land} W))$
	cdleme22e.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W))$
Assertion	cdleme22e	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to N \underset{˙}{\leq} (O \underset{˙}{\lor} V)$

Proof

Step	Hyp	Ref	Expression
1		cdleme22.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme22.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme22.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme22.a	$⊢ A = Atoms (K)$
5		cdleme22.h	$⊢ H = LHyp (K)$
6		cdleme22e.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme22e.f	$⊢ F = (z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W))$
8		cdleme22e.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} z) \underset{˙}{\land} W))$
9		cdleme22e.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W))$
10		simp1l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to K \in HL$
11	10	hllatd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to K \in Lat$
12		simp21l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \in A$
13		simp22l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to Q \in A$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15	14 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
16	10 12 13 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
17		simp1r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to W \in H$
18		simp33l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to z \in A$
19	1 2 3 4 5 6 7 14	cdleme1b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land z \in A)) \to F \in {Base}_{K}$
20	10 17 12 13 18 19	syl23anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to F \in {Base}_{K}$
21		simp23l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to S \in A$
22	14 2 4	hlatjcl	$⊢ (K \in HL \land S \in A \land z \in A) \to S \underset{˙}{\lor} z \in {Base}_{K}$
23	10 21 18 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to S \underset{˙}{\lor} z \in {Base}_{K}$
24	14 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
25	17 24	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to W \in {Base}_{K}$
26	14 3	latmcl	$⊢ (K \in Lat \land S \underset{˙}{\lor} z \in {Base}_{K} \land W \in {Base}_{K}) \to (S \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K}$
27	11 23 25 26	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (S \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K}$
28	14 2	latjcl	$⊢ (K \in Lat \land F \in {Base}_{K} \land (S \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K}) \to F \underset{˙}{\lor} ((S \underset{˙}{\lor} z) \underset{˙}{\land} W) \in {Base}_{K}$
29	11 20 27 28	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to F \underset{˙}{\lor} ((S \underset{˙}{\lor} z) \underset{˙}{\land} W) \in {Base}_{K}$
30	14 1 3	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land F \underset{˙}{\lor} ((S \underset{˙}{\lor} z) \underset{˙}{\land} W) \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} z) \underset{˙}{\land} W))) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
31	11 16 29 30	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} z) \underset{˙}{\land} W))) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
32	8 31	eqbrtrid	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to N \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
33		simp1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
34		simp21	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
35		simp23r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to T \in A$
36		simp31	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (V \in A \land V \underset{˙}{\leq} W)$
37		simp32l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \neq Q$
38		simp32r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q$
39	1 2 3 4 5 6	cdleme22a	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land T \in A) \land ((V \in A \land V \underset{˙}{\leq} W) \land P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q)) \to V = U$
40	33 34 13 35 36 37 38 39	syl133anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to V = U$
41	40	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to O \underset{˙}{\lor} V = O \underset{˙}{\lor} U$
42	9	oveq1i	$⊢ O \underset{˙}{\lor} U = ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W))) \underset{˙}{\lor} U$
43		simp21r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to \neg P \underset{˙}{\leq} W$
44	1 2 3 4 5 6	cdleme0a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \to U \in A$
45	10 17 12 43 13 37 44	syl222anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to U \in A$
46	14 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land z \in A) \to T \underset{˙}{\lor} z \in {Base}_{K}$
47	10 35 18 46	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to T \underset{˙}{\lor} z \in {Base}_{K}$
48	14 3	latmcl	$⊢ (K \in Lat \land T \underset{˙}{\lor} z \in {Base}_{K} \land W \in {Base}_{K}) \to (T \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K}$
49	11 47 25 48	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (T \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K}$
50	14 2	latjcl	$⊢ (K \in Lat \land F \in {Base}_{K} \land (T \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K}) \to F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W) \in {Base}_{K}$
51	11 20 49 50	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W) \in {Base}_{K}$
52	1 2 3 4 5 6	cdlemeulpq	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A)) \to U \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
53	10 17 12 13 52	syl22anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to U \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
54	14 1 2 3 4	atmod2i1	$⊢ (K \in HL \land (U \in A \land P \underset{˙}{\lor} Q \in {Base}_{K} \land F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W) \in {Base}_{K}) \land U \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W))) \underset{˙}{\lor} U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U)$
55	10 45 16 51 53 54	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W))) \underset{˙}{\lor} U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U)$
56	42 55	syl5req	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U) = O \underset{˙}{\lor} U$
57	41 56	eqtr4d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to O \underset{˙}{\lor} V = (P \underset{˙}{\lor} Q) \underset{˙}{\land} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U)$
58	40	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to T \underset{˙}{\lor} V = T \underset{˙}{\lor} U$
59	38 58	eqtr3d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} Q = T \underset{˙}{\lor} U$
60	14 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
61	10 35 45 60	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to T \underset{˙}{\lor} U \in {Base}_{K}$
62	14 4	atbase	$⊢ z \in A \to z \in {Base}_{K}$
63	18 62	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to z \in {Base}_{K}$
64	14 1 2	latlej1	$⊢ (K \in Lat \land T \underset{˙}{\lor} U \in {Base}_{K} \land z \in {Base}_{K}) \to (T \underset{˙}{\lor} U) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} z)$
65	11 61 63 64	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (T \underset{˙}{\lor} U) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} z)$
66	2 4	hlatj32	$⊢ (K \in HL \land (T \in A \land U \in A \land z \in A)) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} z = (T \underset{˙}{\lor} z) \underset{˙}{\lor} U$
67	10 35 45 18 66	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} z = (T \underset{˙}{\lor} z) \underset{˙}{\lor} U$
68	14 4	atbase	$⊢ U \in A \to U \in {Base}_{K}$
69	45 68	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to U \in {Base}_{K}$
70	14 2	latj32	$⊢ (K \in Lat \land (z \in {Base}_{K} \land U \in {Base}_{K} \land (T \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K})) \to (z \underset{˙}{\lor} U) \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W) = (z \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U$
71	11 63 69 49 70	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (z \underset{˙}{\lor} U) \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W) = (z \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U$
72	14 2	latj32	$⊢ (K \in Lat \land (F \in {Base}_{K} \land (T \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K} \land U \in {Base}_{K})) \to (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U = (F \underset{˙}{\lor} U) \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)$
73	11 20 49 69 72	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U = (F \underset{˙}{\lor} U) \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)$
74	14 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land z \in A) \to P \underset{˙}{\lor} z \in {Base}_{K}$
75	10 12 18 74	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} z \in {Base}_{K}$
76	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land z \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} z)$
77	10 12 18 76	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} z)$
78	14 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (P \in A \land P \underset{˙}{\lor} z \in {Base}_{K} \land W \in {Base}_{K}) \land P \underset{˙}{\leq} (P \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W) = (P \underset{˙}{\lor} z) \underset{˙}{\land} (P \underset{˙}{\lor} W)$
79	10 12 75 25 77 78	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W) = (P \underset{˙}{\lor} z) \underset{˙}{\land} (P \underset{˙}{\lor} W)$
80		eqid	$⊢ 1. (K) = 1. (K)$
81	1 2 80 4 5	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} W = 1. (K)$
82	10 17 34 81	syl21anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} W = 1. (K)$
83	82	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} z) \underset{˙}{\land} (P \underset{˙}{\lor} W) = (P \underset{˙}{\lor} z) \underset{˙}{\land} 1. (K)$
84		hlol	$⊢ K \in HL \to K \in OL$
85	10 84	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to K \in OL$
86	14 3 80	olm11	$⊢ (K \in OL \land P \underset{˙}{\lor} z \in {Base}_{K}) \to (P \underset{˙}{\lor} z) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} z$
87	85 75 86	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} z) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} z$
88	79 83 87	3eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W) = P \underset{˙}{\lor} z$
89	88	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} Q = (P \underset{˙}{\lor} z) \underset{˙}{\lor} Q$
90	6	oveq2i	$⊢ Q \underset{˙}{\lor} U = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
91	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land Q \in A) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
92	10 12 13 91	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
93	14 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (Q \in A \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \land Q \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} W)$
94	10 13 16 25 92 93	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} W)$
95	90 94	syl5eq	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to Q \underset{˙}{\lor} U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} W)$
96		simp22	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
97	1 2 80 4 5	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to Q \underset{˙}{\lor} W = 1. (K)$
98	10 17 96 97	syl21anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to Q \underset{˙}{\lor} W = 1. (K)$
99	98	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (Q \underset{˙}{\lor} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K)$
100	14 3 80	olm11	$⊢ (K \in OL \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} Q$
101	85 16 100	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} Q$
102	95 99 101	3eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to Q \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$
103	102	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (Q \underset{˙}{\lor} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)$
104	14 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
105	12 104	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \in {Base}_{K}$
106	14 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} z \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K}$
107	11 75 25 106	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K}$
108	14 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
109	13 108	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to Q \in {Base}_{K}$
110	14 2	latj32	$⊢ (K \in Lat \land (P \in {Base}_{K} \land (P \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K} \land Q \in {Base}_{K})) \to (P \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} Q = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)$
111	11 105 107 109 110	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} Q = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)$
112	103 111	eqtr4d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (Q \underset{˙}{\lor} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W) = (P \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} Q$
113	2 4	hlatj32	$⊢ (K \in HL \land (P \in A \land Q \in A \land z \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} z = (P \underset{˙}{\lor} z) \underset{˙}{\lor} Q$
114	10 12 13 18 113	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} z = (P \underset{˙}{\lor} z) \underset{˙}{\lor} Q$
115	89 112 114	3eqtr4rd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} z = (Q \underset{˙}{\lor} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)$
116	14 2	latj32	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land U \in {Base}_{K} \land (P \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K})) \to (Q \underset{˙}{\lor} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W) = (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U$
117	11 109 69 107 116	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (Q \underset{˙}{\lor} U) \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W) = (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U$
118	115 117	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} z = (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U$
119	118	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (z \underset{˙}{\lor} U) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z) = (z \underset{˙}{\lor} U) \underset{˙}{\land} ((Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U)$
120	14 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land z \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} z \in {Base}_{K}$
121	11 16 63 120	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} z \in {Base}_{K}$
122	14 1 2	latlej2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land z \in {Base}_{K}) \to z \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)$
123	11 16 63 122	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to z \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)$
124	14 1 2 3 4	atmod1i1	$⊢ (K \in HL \land (z \in A \land U \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} z \in {Base}_{K}) \land z \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)) \to z \underset{˙}{\lor} (U \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)) = (z \underset{˙}{\lor} U) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)$
125	10 18 69 121 123 124	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to z \underset{˙}{\lor} (U \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)) = (z \underset{˙}{\lor} U) \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)$
126	7	oveq1i	$⊢ F \underset{˙}{\lor} U = ((z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W))) \underset{˙}{\lor} U$
127	14 2 4	hlatjcl	$⊢ (K \in HL \land z \in A \land U \in A) \to z \underset{˙}{\lor} U \in {Base}_{K}$
128	10 18 45 127	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to z \underset{˙}{\lor} U \in {Base}_{K}$
129	14 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land (P \underset{˙}{\lor} z) \underset{˙}{\land} W \in {Base}_{K}) \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W) \in {Base}_{K}$
130	11 109 107 129	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W) \in {Base}_{K}$
131	1 2 4	hlatlej2	$⊢ (K \in HL \land z \in A \land U \in A) \to U \underset{˙}{\leq} (z \underset{˙}{\lor} U)$
132	10 18 45 131	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to U \underset{˙}{\leq} (z \underset{˙}{\lor} U)$
133	14 1 2 3 4	atmod2i1	$⊢ (K \in HL \land (U \in A \land z \underset{˙}{\lor} U \in {Base}_{K} \land Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W) \in {Base}_{K}) \land U \underset{˙}{\leq} (z \underset{˙}{\lor} U)) \to ((z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W))) \underset{˙}{\lor} U = (z \underset{˙}{\lor} U) \underset{˙}{\land} ((Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U)$
134	10 45 128 130 132 133	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to ((z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W))) \underset{˙}{\lor} U = (z \underset{˙}{\lor} U) \underset{˙}{\land} ((Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U)$
135	126 134	syl5eq	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to F \underset{˙}{\lor} U = (z \underset{˙}{\lor} U) \underset{˙}{\land} ((Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U)$
136	119 125 135	3eqtr4rd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to F \underset{˙}{\lor} U = z \underset{˙}{\lor} (U \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z))$
137	14 1 2	latlej1	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land z \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)$
138	11 16 63 137	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)$
139	14 1 11 69 16 121 53 138	lattrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to U \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)$
140	14 1 3	latleeqm1	$⊢ (K \in Lat \land U \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} z \in {Base}_{K}) \to (U \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z) \leftrightarrow U \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z) = U)$
141	11 69 121 140	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (U \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z) \leftrightarrow U \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z) = U)$
142	139 141	mpbid	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to U \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z) = U$
143	142	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to z \underset{˙}{\lor} (U \underset{˙}{\land} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} z)) = z \underset{˙}{\lor} U$
144	136 143	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to F \underset{˙}{\lor} U = z \underset{˙}{\lor} U$
145	144	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (F \underset{˙}{\lor} U) \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W) = (z \underset{˙}{\lor} U) \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)$
146	73 145	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U = (z \underset{˙}{\lor} U) \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)$
147	1 2 4	hlatlej2	$⊢ (K \in HL \land T \in A \land z \in A) \to z \underset{˙}{\leq} (T \underset{˙}{\lor} z)$
148	10 35 18 147	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to z \underset{˙}{\leq} (T \underset{˙}{\lor} z)$
149	14 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (z \in A \land T \underset{˙}{\lor} z \in {Base}_{K} \land W \in {Base}_{K}) \land z \underset{˙}{\leq} (T \underset{˙}{\lor} z)) \to z \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W) = (T \underset{˙}{\lor} z) \underset{˙}{\land} (z \underset{˙}{\lor} W)$
150	10 18 47 25 148 149	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to z \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W) = (T \underset{˙}{\lor} z) \underset{˙}{\land} (z \underset{˙}{\lor} W)$
151		simp33	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (z \in A \land \neg z \underset{˙}{\leq} W)$
152	1 2 80 4 5	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (z \in A \land \neg z \underset{˙}{\leq} W)) \to z \underset{˙}{\lor} W = 1. (K)$
153	10 17 151 152	syl21anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to z \underset{˙}{\lor} W = 1. (K)$
154	153	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (T \underset{˙}{\lor} z) \underset{˙}{\land} (z \underset{˙}{\lor} W) = (T \underset{˙}{\lor} z) \underset{˙}{\land} 1. (K)$
155	150 154	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to z \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W) = (T \underset{˙}{\lor} z) \underset{˙}{\land} 1. (K)$
156	14 3 80	olm11	$⊢ (K \in OL \land T \underset{˙}{\lor} z \in {Base}_{K}) \to (T \underset{˙}{\lor} z) \underset{˙}{\land} 1. (K) = T \underset{˙}{\lor} z$
157	85 47 156	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (T \underset{˙}{\lor} z) \underset{˙}{\land} 1. (K) = T \underset{˙}{\lor} z$
158	155 157	eqtr2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to T \underset{˙}{\lor} z = z \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)$
159	158	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (T \underset{˙}{\lor} z) \underset{˙}{\lor} U = (z \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U$
160	71 146 159	3eqtr4rd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (T \underset{˙}{\lor} z) \underset{˙}{\lor} U = (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U$
161	67 160	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} z = (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U$
162	65 161	breqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (T \underset{˙}{\lor} U) \underset{˙}{\leq} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U)$
163	59 162	eqbrtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U)$
164	14 2	latjcl	$⊢ (K \in Lat \land F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W) \in {Base}_{K} \land U \in {Base}_{K}) \to (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U \in {Base}_{K}$
165	11 51 69 164	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U \in {Base}_{K}$
166	14 1 3	latleeqm1	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land (F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\land} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U) = P \underset{˙}{\lor} Q)$
167	11 16 165 166	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\land} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U) = P \underset{˙}{\lor} Q)$
168	163 167	mpbid	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} ((F \underset{˙}{\lor} ((T \underset{˙}{\lor} z) \underset{˙}{\land} W)) \underset{˙}{\lor} U) = P \underset{˙}{\lor} Q$
169	57 168	eqtr2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} Q = O \underset{˙}{\lor} V$
170	32 169	breqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land T \in A)) \land ((V \in A \land V \underset{˙}{\leq} W) \land (P \neq Q \land T \underset{˙}{\lor} V = P \underset{˙}{\lor} Q) \land (z \in A \land \neg z \underset{˙}{\leq} W))) \to N \underset{˙}{\leq} (O \underset{˙}{\lor} V)$

Metamath Proof Explorer

Theorem cdleme22e

Proof