Metamath Proof Explorer

Theorem cdlemg11a

Description: TODO: FIX COMMENT. (Contributed by NM, 4-May-2013)

		Ref	Expression
	Hypotheses	cdlemg8.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		cdlemg8.j	$⊢ \underset{˙}{\lor} = join (K)$
		cdlemg8.m	$⊢ \underset{˙}{\land} = meet (K)$
		cdlemg8.a	$⊢ A = Atoms (K)$
		cdlemg8.h	$⊢ H = LHyp (K)$
		cdlemg8.t	$⊢ T = LTrn (K) (W)$
	Assertion	cdlemg11a	$⊢ ((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 (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \to F (G (P)) \neq P$

Proof

Step	Hyp	Ref	Expression
1		cdlemg8.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg8.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg8.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg8.a	$⊢ A = Atoms (K)$
5		cdlemg8.h	$⊢ H = LHyp (K)$
6		cdlemg8.t	$⊢ T = LTrn (K) (W)$
7		simp33	$⊢ ((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 (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \to F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q$
8		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 F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \land F (G (P)) = P) \to F (G (P)) = P$
9		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 F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \land F (G (P)) = P) \to (K \in HL \land W \in H)$
10		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 (F \in T \land G \in T \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \land F (G (P)) = P) \to ((P \in A \land \neg P \underset{˙}{\leq} W) \land (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 F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \land F (G (P)) = P) \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 F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \land F (G (P)) = P) \to G \in T$
13	1 4 5 6	cdlemg6	$⊢ ((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 (G (P)) = P)) \to F (G (Q)) = Q$
14	9 10 11 12 8 13	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 F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \land F (G (P)) = P) \to F (G (Q)) = Q$
15	8 14	oveq12d	$⊢ (((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 (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \land F (G (P)) = P) \to F (G (P)) \underset{˙}{\lor} F (G (Q)) = P \underset{˙}{\lor} Q$
16	15	ex	$⊢ ((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 (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \to (F (G (P)) = P \to F (G (P)) \underset{˙}{\lor} F (G (Q)) = P \underset{˙}{\lor} Q)$
17	16	necon3d	$⊢ ((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 (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \to (F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \to F (G (P)) \neq P)$
18	7 17	mpd	$⊢ ((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 (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q)) \to F (G (P)) \neq P$