cdlemg2fvlem

	Ref	Expression
Hypotheses	cdlemg2.b	$⊢ B = {Base}_{K}$
	cdlemg2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg2.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg2.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg2.a	$⊢ A = Atoms (K)$
	cdlemg2.h	$⊢ H = LHyp (K)$
	cdlemg2.t	$⊢ T = LTrn (K) (W)$
	cdlemg2ex.u	$⊢ U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W$
	cdlemg2ex.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemg2ex.e	$⊢ E = (p \underset{˙}{\lor} q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemg2ex.g	$⊢ G = (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	cdlemg2fvlem	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to F (X) = F (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$

Proof

Step	Hyp	Ref	Expression
1		cdlemg2.b	$⊢ B = {Base}_{K}$
2		cdlemg2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemg2.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemg2.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemg2.a	$⊢ A = Atoms (K)$
6		cdlemg2.h	$⊢ H = LHyp (K)$
7		cdlemg2.t	$⊢ T = LTrn (K) (W)$
8		cdlemg2ex.u	$⊢ U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W$
9		cdlemg2ex.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W))$
10		cdlemg2ex.e	$⊢ E = (p \underset{˙}{\lor} q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
11		cdlemg2ex.g	$⊢ G = (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))$
12		simp1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (K \in HL \land W \in H)$
13		simp3l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to F \in T$
14		simp2r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
15		simp2l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
16		simp3r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
17	15 16	jca	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((P \in A \land \neg P \underset{˙}{\leq} W) \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)$
18		fveq1	$⊢ F = G \to F (X) = G (X)$
19		fveq1	$⊢ F = G \to F (P) = G (P)$
20	19	oveq1d	$⊢ F = G \to F (P) \underset{˙}{\lor} (X \underset{˙}{\land} W) = G (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$
21	18 20	eqeq12d	$⊢ F = G \to (F (X) = F (P) \underset{˙}{\lor} (X \underset{˙}{\land} W) \leftrightarrow G (X) = G (P) \underset{˙}{\lor} (X \underset{˙}{\land} W))$
22	1 2 3 4 5 6 8 9 10 11	cdleme48fvg	$⊢ (((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 (X \in B \land \neg X \underset{˙}{\leq} W) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to G (X) = G (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$
23	22	3expb	$⊢ (((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 ((X \in B \land \neg X \underset{˙}{\leq} W) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to G (X) = G (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$
24	1 2 3 4 5 6 7 8 9 10 11 21 23	cdlemg2ce	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((X \in B \land \neg X \underset{˙}{\leq} W) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to F (X) = F (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$
25	12 13 14 17 24	syl112anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to F (X) = F (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem cdlemg2fvlem

Proof