cdlemg4

	Ref	Expression
Hypotheses	cdlemg4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg4.a	$⊢ A = Atoms (K)$
	cdlemg4.h	$⊢ H = LHyp (K)$
	cdlemg4.t	$⊢ T = LTrn (K) (W)$
	cdlemg4.r	$⊢ R = trL (K) (W)$
	cdlemg4.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg4b.v	$⊢ V = R (G)$
Assertion	cdlemg4	$⊢ ((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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to F (G (Q)) = Q$

Proof

Step	Hyp	Ref	Expression
1		cdlemg4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg4.a	$⊢ A = Atoms (K)$
3		cdlemg4.h	$⊢ H = LHyp (K)$
4		cdlemg4.t	$⊢ T = LTrn (K) (W)$
5		cdlemg4.r	$⊢ R = trL (K) (W)$
6		cdlemg4.j	$⊢ \underset{˙}{\lor} = join (K)$
7		cdlemg4b.v	$⊢ V = R (G)$
8		eqid	$⊢ meet (K) = meet (K)$
9	1 2 3 4 5 6 7 8	cdlemg4g	$⊢ ((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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to F (G (Q)) = (Q \underset{˙}{\lor} V) meet (K) (P \underset{˙}{\lor} Q)$
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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to K \in HL$
11		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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to P \in A$
12		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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to Q \in A$
13	6 2	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
14	10 11 12 13	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
15	14	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to (Q \underset{˙}{\lor} V) meet (K) (P \underset{˙}{\lor} Q) = (Q \underset{˙}{\lor} V) meet (K) (Q \underset{˙}{\lor} P)$
16		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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to (K \in HL \land W \in H)$
17		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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to G \in T$
18		eqid	$⊢ {Base}_{K} = {Base}_{K}$
19	18 3 4 5	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in {Base}_{K}$
20	16 17 19	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to R (G) \in {Base}_{K}$
21	7 20	eqeltrid	$⊢ ((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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to V \in {Base}_{K}$
22		simp32	$⊢ ((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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
23		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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to \neg P \underset{˙}{\leq} W$
24		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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
25	1 6 8 2 3 4 5	trlval2	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (G) = (P \underset{˙}{\lor} G (P)) meet (K) W$
26	16 17 24 25	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to R (G) = (P \underset{˙}{\lor} G (P)) meet (K) W$
27	7 26	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to V = (P \underset{˙}{\lor} G (P)) meet (K) W$
28	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to K \in Lat$
29	1 2 3 4	ltrnel	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
30	16 17 24 29	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
31	30	simpld	$⊢ ((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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to G (P) \in A$
32	18 6 2	hlatjcl	$⊢ (K \in HL \land P \in A \land G (P) \in A) \to P \underset{˙}{\lor} G (P) \in {Base}_{K}$
33	10 11 31 32	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to P \underset{˙}{\lor} G (P) \in {Base}_{K}$
34		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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to W \in H$
35	18 3	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
36	34 35	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to W \in {Base}_{K}$
37	18 1 8	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} G (P) \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} G (P)) meet (K) W) \underset{˙}{\leq} W$
38	28 33 36 37	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to ((P \underset{˙}{\lor} G (P)) meet (K) W) \underset{˙}{\leq} W$
39	27 38	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to V \underset{˙}{\leq} W$
40	18 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
41	11 40	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to P \in {Base}_{K}$
42	18 1	lattr	$⊢ (K \in Lat \land (P \in {Base}_{K} \land V \in {Base}_{K} \land W \in {Base}_{K})) \to ((P \underset{˙}{\leq} V \land V \underset{˙}{\leq} W) \to P \underset{˙}{\leq} W)$
43	28 41 21 36 42	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to ((P \underset{˙}{\leq} V \land V \underset{˙}{\leq} W) \to P \underset{˙}{\leq} W)$
44	39 43	mpan2d	$⊢ ((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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to (P \underset{˙}{\leq} V \to P \underset{˙}{\leq} W)$
45	23 44	mtod	$⊢ ((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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to \neg P \underset{˙}{\leq} V$
46	18 1 6 2	hlexch2	$⊢ (K \in HL \land (P \in A \land Q \in A \land V \in {Base}_{K}) \land \neg P \underset{˙}{\leq} V) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} V) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
47	10 11 12 21 45 46	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} V) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
48	22 47	mtod	$⊢ ((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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} V)$
49	18 1 6 8 2	2llnma1b	$⊢ (K \in HL \land (V \in {Base}_{K} \land Q \in A \land P \in A) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} V)) \to (Q \underset{˙}{\lor} V) meet (K) (Q \underset{˙}{\lor} P) = Q$
50	10 21 12 11 48 49	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to (Q \underset{˙}{\lor} V) meet (K) (Q \underset{˙}{\lor} P) = Q$
51	9 15 50	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 F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to F (G (Q)) = Q$

Metamath Proof Explorer

Theorem cdlemg4

Proof