cdlemg39

Description: Eliminate =/= conditions from cdlemg38 . TODO: Would this better be done at cdlemg35 ? 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)$
	cdlemg35.r	$⊢ R = trL (K) (W)$
Assertion	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$

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		cdlemg35.r	$⊢ R = trL (K) (W)$
8		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)) \land R (F) = R (G)) \to (K \in HL \land W \in H)$
9		simpl2l	$⊢ (((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)) \land R (F) = R (G)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
10		simpl2r	$⊢ (((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)) \land R (F) = R (G)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
11		simpl31	$⊢ (((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)) \land R (F) = R (G)) \to F \in T$
12		simpl32	$⊢ (((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)) \land R (F) = R (G)) \to G \in T$
13		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)) \land R (F) = R (G)) \to R (F) = R (G)$
14	1 2 3 4 5 6 7	cdlemg15	$⊢ (((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 R (F) = R (G)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
15	8 9 10 11 12 13 14	syl321anc	$⊢ (((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)) \land R (F) = R (G)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
16		simpll1	$⊢ ((((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)) \land R (F) \neq R (G)) \land F (P) = P) \to (K \in HL \land W \in H)$
17		simpll2	$⊢ ((((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)) \land R (F) \neq R (G)) \land F (P) = P) \to ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
18		simpl31	$⊢ (((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)) \land R (F) \neq R (G)) \to F \in T$
19	18	adantr	$⊢ ((((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)) \land R (F) \neq R (G)) \land F (P) = P) \to F \in T$
20		simpl32	$⊢ (((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)) \land R (F) \neq R (G)) \to G \in T$
21	20	adantr	$⊢ ((((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)) \land R (F) \neq R (G)) \land F (P) = P) \to G \in T$
22		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)) \land R (F) \neq R (G)) \land F (P) = P) \to F (P) = P$
23	1 2 3 4 5 6 7	cdlemg14f	$⊢ ((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 F (P) = P)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
24	16 17 19 21 22 23	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)) \land R (F) \neq R (G)) \land F (P) = P) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
25		simpll1	$⊢ ((((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)) \land R (F) \neq R (G)) \land G (P) = P) \to (K \in HL \land W \in H)$
26		simpll2	$⊢ ((((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)) \land R (F) \neq R (G)) \land G (P) = P) \to ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
27	18	adantr	$⊢ ((((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)) \land R (F) \neq R (G)) \land G (P) = P) \to F \in T$
28	20	adantr	$⊢ ((((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)) \land R (F) \neq R (G)) \land G (P) = P) \to G \in T$
29		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)) \land R (F) \neq R (G)) \land G (P) = P) \to G (P) = P$
30	1 2 3 4 5 6 7	cdlemg14g	$⊢ ((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 G (P) = P)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
31	25 26 27 28 29 30	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)) \land R (F) \neq R (G)) \land G (P) = P) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
32		simpll1	$⊢ ((((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)) \land R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to (K \in HL \land W \in H)$
33		simpl2l	$⊢ (((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)) \land R (F) \neq R (G)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
34	33	adantr	$⊢ ((((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)) \land R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
35		simpl2r	$⊢ (((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)) \land R (F) \neq R (G)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
36	35	adantr	$⊢ ((((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)) \land R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
37		simpll3	$⊢ ((((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)) \land R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to (F \in T \land G \in T \land P \neq Q)$
38		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)) \land R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to (F (P) \neq P \land G (P) \neq P)$
39		simplr	$⊢ ((((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)) \land R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to R (F) \neq R (G)$
40	1 2 3 4 5 6 7	cdlemg38	$⊢ (((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) \land ((F (P) \neq P \land G (P) \neq P) \land R (F) \neq R (G))) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
41	32 34 36 37 38 39 40	syl312anc	$⊢ ((((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)) \land R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
42	24 31 41	pm2.61da2ne	$⊢ (((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)) \land R (F) \neq R (G)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
43	15 42	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 \land P \neq Q)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem cdlemg39

Proof