cdlemd2

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 29-May-2012)

	Ref	Expression
Hypotheses	cdlemd2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemd2.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemd2.a	$⊢ A = Atoms (K)$
	cdlemd2.h	$⊢ H = LHyp (K)$
	cdlemd2.t	$⊢ T = LTrn (K) (W)$
Assertion	cdlemd2	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (R) = G (R)$

Proof

Step	Hyp	Ref	Expression
1		cdlemd2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemd2.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemd2.a	$⊢ A = Atoms (K)$
4		cdlemd2.h	$⊢ H = LHyp (K)$
5		cdlemd2.t	$⊢ T = LTrn (K) (W)$
6		simp3l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (P) = G (P)$
7		simp11	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to (K \in HL \land W \in H)$
8		simp12l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F \in T$
9		simp11l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to K \in HL$
10	9	hllatd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to K \in Lat$
11		simp21l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to P \in A$
12		simp13	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to R \in A$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R \in {Base}_{K}$
15	9 11 12 14	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to P \underset{˙}{\lor} R \in {Base}_{K}$
16		simp11r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to W \in H$
17	13 4	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
18	16 17	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to W \in {Base}_{K}$
19		eqid	$⊢ meet (K) = meet (K)$
20	13 19	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} R) meet (K) W \in {Base}_{K}$
21	10 15 18 20	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to (P \underset{˙}{\lor} R) meet (K) W \in {Base}_{K}$
22	13 1 19	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} R) meet (K) W) \underset{˙}{\leq} W$
23	10 15 18 22	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to ((P \underset{˙}{\lor} R) meet (K) W) \underset{˙}{\leq} W$
24	13 1 4 5	ltrnval1	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \underset{˙}{\lor} R) meet (K) W \in {Base}_{K} \land ((P \underset{˙}{\lor} R) meet (K) W) \underset{˙}{\leq} W)) \to F ((P \underset{˙}{\lor} R) meet (K) W) = (P \underset{˙}{\lor} R) meet (K) W$
25	7 8 21 23 24	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F ((P \underset{˙}{\lor} R) meet (K) W) = (P \underset{˙}{\lor} R) meet (K) W$
26		simp12r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to G \in T$
27	13 1 4 5	ltrnval1	$⊢ ((K \in HL \land W \in H) \land G \in T \land ((P \underset{˙}{\lor} R) meet (K) W \in {Base}_{K} \land ((P \underset{˙}{\lor} R) meet (K) W) \underset{˙}{\leq} W)) \to G ((P \underset{˙}{\lor} R) meet (K) W) = (P \underset{˙}{\lor} R) meet (K) W$
28	7 26 21 23 27	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to G ((P \underset{˙}{\lor} R) meet (K) W) = (P \underset{˙}{\lor} R) meet (K) W$
29	25 28	eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F ((P \underset{˙}{\lor} R) meet (K) W) = G ((P \underset{˙}{\lor} R) meet (K) W)$
30	6 29	oveq12d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (P) \underset{˙}{\lor} F ((P \underset{˙}{\lor} R) meet (K) W) = G (P) \underset{˙}{\lor} G ((P \underset{˙}{\lor} R) meet (K) W)$
31	13 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
32	11 31	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to P \in {Base}_{K}$
33	13 2 4 5	ltrnj	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in {Base}_{K} \land (P \underset{˙}{\lor} R) meet (K) W \in {Base}_{K})) \to F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) = F (P) \underset{˙}{\lor} F ((P \underset{˙}{\lor} R) meet (K) W)$
34	7 8 32 21 33	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) = F (P) \underset{˙}{\lor} F ((P \underset{˙}{\lor} R) meet (K) W)$
35	13 2 4 5	ltrnj	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in {Base}_{K} \land (P \underset{˙}{\lor} R) meet (K) W \in {Base}_{K})) \to G (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) = G (P) \underset{˙}{\lor} G ((P \underset{˙}{\lor} R) meet (K) W)$
36	7 26 32 21 35	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to G (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) = G (P) \underset{˙}{\lor} G ((P \underset{˙}{\lor} R) meet (K) W)$
37	30 34 36	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) = G (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W))$
38		simp3r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (Q) = G (Q)$
39		simp22l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to Q \in A$
40	13 2 3	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
41	9 39 12 40	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
42	13 19	latmcl	$⊢ (K \in Lat \land Q \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K}) \to (Q \underset{˙}{\lor} R) meet (K) W \in {Base}_{K}$
43	10 41 18 42	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to (Q \underset{˙}{\lor} R) meet (K) W \in {Base}_{K}$
44	13 1 19	latmle2	$⊢ (K \in Lat \land Q \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K}) \to ((Q \underset{˙}{\lor} R) meet (K) W) \underset{˙}{\leq} W$
45	10 41 18 44	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to ((Q \underset{˙}{\lor} R) meet (K) W) \underset{˙}{\leq} W$
46	13 1 4 5	ltrnval1	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((Q \underset{˙}{\lor} R) meet (K) W \in {Base}_{K} \land ((Q \underset{˙}{\lor} R) meet (K) W) \underset{˙}{\leq} W)) \to F ((Q \underset{˙}{\lor} R) meet (K) W) = (Q \underset{˙}{\lor} R) meet (K) W$
47	7 8 43 45 46	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F ((Q \underset{˙}{\lor} R) meet (K) W) = (Q \underset{˙}{\lor} R) meet (K) W$
48	13 1 4 5	ltrnval1	$⊢ ((K \in HL \land W \in H) \land G \in T \land ((Q \underset{˙}{\lor} R) meet (K) W \in {Base}_{K} \land ((Q \underset{˙}{\lor} R) meet (K) W) \underset{˙}{\leq} W)) \to G ((Q \underset{˙}{\lor} R) meet (K) W) = (Q \underset{˙}{\lor} R) meet (K) W$
49	7 26 43 45 48	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to G ((Q \underset{˙}{\lor} R) meet (K) W) = (Q \underset{˙}{\lor} R) meet (K) W$
50	47 49	eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F ((Q \underset{˙}{\lor} R) meet (K) W) = G ((Q \underset{˙}{\lor} R) meet (K) W)$
51	38 50	oveq12d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (Q) \underset{˙}{\lor} F ((Q \underset{˙}{\lor} R) meet (K) W) = G (Q) \underset{˙}{\lor} G ((Q \underset{˙}{\lor} R) meet (K) W)$
52	13 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
53	39 52	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to Q \in {Base}_{K}$
54	13 2 4 5	ltrnj	$⊢ ((K \in HL \land W \in H) \land F \in T \land (Q \in {Base}_{K} \land (Q \underset{˙}{\lor} R) meet (K) W \in {Base}_{K})) \to F (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W)) = F (Q) \underset{˙}{\lor} F ((Q \underset{˙}{\lor} R) meet (K) W)$
55	7 8 53 43 54	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W)) = F (Q) \underset{˙}{\lor} F ((Q \underset{˙}{\lor} R) meet (K) W)$
56	13 2 4 5	ltrnj	$⊢ ((K \in HL \land W \in H) \land G \in T \land (Q \in {Base}_{K} \land (Q \underset{˙}{\lor} R) meet (K) W \in {Base}_{K})) \to G (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W)) = G (Q) \underset{˙}{\lor} G ((Q \underset{˙}{\lor} R) meet (K) W)$
57	7 26 53 43 56	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to G (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W)) = G (Q) \underset{˙}{\lor} G ((Q \underset{˙}{\lor} R) meet (K) W)$
58	51 55 57	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W)) = G (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))$
59	37 58	oveq12d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) F (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W)) = G (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) G (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))$
60	13 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land (P \underset{˙}{\lor} R) meet (K) W \in {Base}_{K}) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W) \in {Base}_{K}$
61	10 32 21 60	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W) \in {Base}_{K}$
62	13 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land (Q \underset{˙}{\lor} R) meet (K) W \in {Base}_{K}) \to Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W) \in {Base}_{K}$
63	10 53 43 62	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W) \in {Base}_{K}$
64	13 19 4 5	ltrnm	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W) \in {Base}_{K} \land Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W) \in {Base}_{K})) \to F ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))) = F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) F (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))$
65	7 8 61 63 64	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))) = F (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) F (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))$
66	13 19 4 5	ltrnm	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W) \in {Base}_{K} \land Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W) \in {Base}_{K})) \to G ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))) = G (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) G (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))$
67	7 26 61 63 66	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to G ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))) = G (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) G (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))$
68	59 65 67	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))) = G ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W)))$
69		simp21	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
70		simp22	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
71		simp23l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to P \neq Q$
72		simp23r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
73	12 71 72	3jca	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to (R \in A \land P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
74	1 2 19 3 4	cdlemd1	$⊢ ((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 (R \in A \land P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R = (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))$
75	7 69 70 73 74	syl13anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to R = (P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W))$
76	75	fveq2d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (R) = F ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W)))$
77	75	fveq2d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to G (R) = G ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} R) meet (K) W)) meet (K) (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} R) meet (K) W)))$
78	68 76 77	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (R) = G (R)$

Metamath Proof Explorer

Theorem cdlemd2

Proof