cdlemg7aN

Description: TODO: FIX COMMENT. (Contributed by NM, 28-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemg7.b	$⊢ B = {Base}_{K}$
	cdlemg7.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg7.a	$⊢ A = Atoms (K)$
	cdlemg7.h	$⊢ H = LHyp (K)$
	cdlemg7.t	$⊢ T = LTrn (K) (W)$
Assertion	cdlemg7aN	$⊢ ((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 G \in T \land F (G (P)) = P)) \to F (G (X)) = X$

Proof

Step	Hyp	Ref	Expression
1		cdlemg7.b	$⊢ B = {Base}_{K}$
2		cdlemg7.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemg7.a	$⊢ A = Atoms (K)$
4		cdlemg7.h	$⊢ H = LHyp (K)$
5		cdlemg7.t	$⊢ T = LTrn (K) (W)$
6		simp1l	$⊢ ((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 G \in T \land F (G (P)) = P)) \to K \in HL$
7		simp1r	$⊢ ((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 G \in T \land F (G (P)) = P)) \to W \in H$
8		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 G \in T \land F (G (P)) = P)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
9		eqid	$⊢ join (K) = join (K)$
10		eqid	$⊢ meet (K) = meet (K)$
11	1 2 9 10 3 4	lhpmcvr2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)$
12	6 7 8 11	syl21anc	$⊢ ((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 G \in T \land F (G (P)) = P)) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)$
13		simp11	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to (K \in HL \land W \in H)$
14		simp2	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to r \in A$
15		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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to \neg r \underset{˙}{\leq} W$
16	14 15	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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to (r \in A \land \neg r \underset{˙}{\leq} W)$
17		simp12r	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
18		simp131	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F \in T$
19		simp132	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to G \in T$
20		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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to r join (K) (X meet (K) W) = X$
21	1 2 9 10 3 4 5	cdlemg7fvN	$⊢ ((K \in HL \land W \in H) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land r join (K) (X meet (K) W) = X)) \to F (G (X)) = F (G (r)) join (K) (X meet (K) W)$
22	13 16 17 18 19 20 21	syl123anc	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (G (X)) = F (G (r)) join (K) (X meet (K) W)$
23		simp12l	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
24		simp133	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (G (P)) = P$
25	2 3 4 5	cdlemg6	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (r \in A \land \neg r \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land F (G (P)) = P)) \to F (G (r)) = r$
26	13 23 16 18 19 24 25	syl123anc	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (G (r)) = r$
27	26	oveq1d	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (G (r)) join (K) (X meet (K) W) = r join (K) (X meet (K) W)$
28	22 27 20	3eqtrd	$⊢ (((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 G \in T \land F (G (P)) = P)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X)) \to F (G (X)) = X$
29	28	rexlimdv3a	$⊢ ((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 G \in T \land F (G (P)) = P)) \to (\exists r \in A (\neg r \underset{˙}{\leq} W \land r join (K) (X meet (K) W) = X) \to F (G (X)) = X)$
30	12 29	mpd	$⊢ ((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 G \in T \land F (G (P)) = P)) \to F (G (X)) = X$

Metamath Proof Explorer

Theorem cdlemg7aN

Proof