cdlemg40

Description: Eliminate P =/= Q conditions from cdlemg39 . TODO: Fix comment. (Contributed by NM, 31-May-2013)

	Ref	Expression
Hypotheses	cdlemg35.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg35.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg35.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg35.a	$⊢ A = Atoms (K)$
	cdlemg35.h	$⊢ H = LHyp (K)$
	cdlemg35.t	$⊢ T = LTrn (K) (W)$
Assertion	cdlemg40	$⊢ ((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)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$

Proof

Step	Hyp	Ref	Expression
1		cdlemg35.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg35.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg35.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg35.a	$⊢ A = Atoms (K)$
5		cdlemg35.h	$⊢ H = LHyp (K)$
6		cdlemg35.t	$⊢ T = LTrn (K) (W)$
7		id	$⊢ P = Q \to P = Q$
8		2fveq3	$⊢ P = Q \to F (G (P)) = F (G (Q))$
9	7 8	oveq12d	$⊢ P = Q \to P \underset{˙}{\lor} F (G (P)) = Q \underset{˙}{\lor} F (G (Q))$
10	9	oveq1d	$⊢ P = Q \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
11	10	adantl	$⊢ (((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 P = Q) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
12		simpl1	$⊢ (((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 P \neq Q) \to (K \in HL \land W \in H)$
13		simpl2	$⊢ (((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 P \neq Q) \to ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
14		simpl3l	$⊢ (((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 P \neq Q) \to F \in T$
15		simpl3r	$⊢ (((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 P \neq Q) \to G \in T$
16		simpr	$⊢ (((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 P \neq Q) \to P \neq Q$
17		eqid	$⊢ trL (K) (W) = trL (K) (W)$
18	1 2 3 4 5 6 17	cdlemg39	$⊢ ((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 P \neq Q)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
19	12 13 14 15 16 18	syl113anc	$⊢ (((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 P \neq Q) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
20	11 19	pm2.61dane	$⊢ ((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)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem cdlemg40

Proof