cdleme50trn3

Description: Part of proof that F is a translation. P = Q case. TODO: fix comment. (Contributed by NM, 10-Apr-2013)

	Ref	Expression
Hypotheses	cdlemef50.b	$⊢ B = {Base}_{K}$
	cdlemef50.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemef50.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemef50.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemef50.a	$⊢ A = Atoms (K)$
	cdlemef50.h	$⊢ H = LHyp (K)$
	cdlemef50.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdlemef50.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemefs50.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemef50.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = E)), ⦋ s / t ⦌ D) \underset{˙}{\lor} (x \underset{˙}{\land} W))), x))$
Assertion	cdleme50trn3	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \underset{˙}{\lor} F (R)) \underset{˙}{\land} W = U$

Proof

Step	Hyp	Ref	Expression
1		cdlemef50.b	$⊢ B = {Base}_{K}$
2		cdlemef50.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemef50.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemef50.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemef50.a	$⊢ A = Atoms (K)$
6		cdlemef50.h	$⊢ H = LHyp (K)$
7		cdlemef50.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdlemef50.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
9		cdlemefs50.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
10		cdlemef50.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = E)), ⦋ s / t ⦌ D) \underset{˙}{\lor} (x \underset{˙}{\land} W))), x))$
11		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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
12		simprr	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
13		eqid	$⊢ 0. (K) = 0. (K)$
14	2 4 13 5 6	lhpmat	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to R \underset{˙}{\land} W = 0. (K)$
15	11 12 14	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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\land} W = 0. (K)$
16		simprrl	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \in A$
17	1 5	atbase	$⊢ R \in A \to R \in B$
18	16 17	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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \in B$
19		simprl	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P = Q$
20	10	cdleme31id	$⊢ (R \in B \land P = Q) \to F (R) = R$
21	18 19 20	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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to F (R) = R$
22	21	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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} F (R) = R \underset{˙}{\lor} R$
23		simpl1l	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to K \in HL$
24	3 5	hlatjidm	$⊢ (K \in HL \land R \in A) \to R \underset{˙}{\lor} R = R$
25	23 16 24	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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} R = R$
26	22 25	eqtrd	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} F (R) = R$
27	26	oveq1d	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \underset{˙}{\lor} F (R)) \underset{˙}{\land} W = R \underset{˙}{\land} W$
28		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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
29	2 4 13 5 6	lhpmat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\land} W = 0. (K)$
30	11 28 29	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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \underset{˙}{\land} W = 0. (K)$
31	15 27 30	3eqtr4d	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \underset{˙}{\lor} F (R)) \underset{˙}{\land} W = P \underset{˙}{\land} W$
32		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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \in A$
33	3 5	hlatjidm	$⊢ (K \in HL \land P \in A) \to P \underset{˙}{\lor} P = P$
34	23 32 33	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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} P = P$
35	19	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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} P = P \underset{˙}{\lor} Q$
36	34 35	eqtr3d	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P = P \underset{˙}{\lor} Q$
37	36	oveq1d	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \underset{˙}{\land} W = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
38	31 37	eqtrd	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \underset{˙}{\lor} F (R)) \underset{˙}{\land} W = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
39	38 7	eqtr4di	$⊢ (((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 (P = Q \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \underset{˙}{\lor} F (R)) \underset{˙}{\land} W = U$

Metamath Proof Explorer

Theorem cdleme50trn3

Proof