cdleme21k

Description: Eliminate S =/= T condition in cdleme21 . (Contributed by NM, 26-Dec-2012)

	Ref	Expression
Hypotheses	cdleme21.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme21.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme21.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme21.a	$⊢ A = Atoms (K)$
	cdleme21.h	$⊢ H = LHyp (K)$
	cdleme21.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme21.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme21g.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
	cdleme21g.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
	cdleme21g.y	$⊢ Y = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
	cdleme21g.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} D)$
	cdleme21g.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (G \underset{˙}{\lor} Y)$
Assertion	cdleme21k	$⊢ (((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to N = O$

Proof

Step	Hyp	Ref	Expression
1		cdleme21.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme21.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme21.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme21.a	$⊢ A = Atoms (K)$
5		cdleme21.h	$⊢ H = LHyp (K)$
6		cdleme21.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme21.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme21g.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9		cdleme21g.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
10		cdleme21g.y	$⊢ Y = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
11		cdleme21g.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} D)$
12		cdleme21g.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (G \underset{˙}{\lor} Y)$
13		oveq1	$⊢ S = T \to S \underset{˙}{\lor} U = T \underset{˙}{\lor} U$
14		oveq2	$⊢ S = T \to P \underset{˙}{\lor} S = P \underset{˙}{\lor} T$
15	14	oveq1d	$⊢ S = T \to (P \underset{˙}{\lor} S) \underset{˙}{\land} W = (P \underset{˙}{\lor} T) \underset{˙}{\land} W$
16	15	oveq2d	$⊢ S = T \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W)$
17	13 16	oveq12d	$⊢ S = T \to (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
18	17 7 8	3eqtr4g	$⊢ S = T \to F = G$
19		oveq2	$⊢ S = T \to R \underset{˙}{\lor} S = R \underset{˙}{\lor} T$
20	19	oveq1d	$⊢ S = T \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
21	20 9 10	3eqtr4g	$⊢ S = T \to D = Y$
22	18 21	oveq12d	$⊢ S = T \to F \underset{˙}{\lor} D = G \underset{˙}{\lor} Y$
23	22	oveq2d	$⊢ S = T \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} D) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (G \underset{˙}{\lor} Y)$
24	23 11 12	3eqtr4g	$⊢ S = T \to N = O$
25	24	eqeq1d	$⊢ S = T \to (N = O \leftrightarrow O = O)$
26		simpl11	$⊢ ((((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to (K \in HL \land W \in H)$
27		simpl12	$⊢ ((((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
28		simpl13	$⊢ ((((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
29		simpl21	$⊢ ((((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
30		simpl22	$⊢ ((((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
31		simpl23	$⊢ ((((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to (T \in A \land \neg T \underset{˙}{\leq} W)$
32		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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to P \neq Q$
33		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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to S \neq T$
34	32 33	jca	$⊢ ((((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to (P \neq Q \land S \neq T)$
35		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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
36	1 2 3 4 5 6 7 8 9 10 11 12	cdleme21	$⊢ (((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land ((P \neq Q \land S \neq T) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to N = O$
37	26 27 28 29 30 31 34 35 36	syl332anc	$⊢ ((((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \land S \neq T) \to N = O$
38		eqidd	$⊢ (((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to O = O$
39	25 37 38	pm2.61ne	$⊢ (((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 \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to N = O$

Metamath Proof Explorer

Theorem cdleme21k

Proof