cdlemg11aq

Description: TODO: FIX COMMENT. TODO: can proof using this be restructured to use cdlemg11a ? (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	cdlemg11aq	$⊢ ((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 (Q)) \neq Q$

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		simp1	$⊢ ((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 (K \in HL \land W \in H)$
8		simp2r	$⊢ ((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 (Q \in A \land \neg Q \underset{˙}{\leq} W)$
9		simp2l	$⊢ ((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 (P \in A \land \neg P \underset{˙}{\leq} W)$
10		simp31	$⊢ ((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 \in T$
11		simp32	$⊢ ((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 G \in T$
12		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$
13		simp1l	$⊢ ((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 K \in HL$
14		simp2ll	$⊢ ((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 P \in A$
15	1 4 5 6	ltrncoat	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to F (G (P)) \in A$
16	7 10 11 14 15	syl121anc	$⊢ ((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)) \in A$
17		simp2rl	$⊢ ((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 Q \in A$
18	1 4 5 6	ltrncoat	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land Q \in A) \to F (G (Q)) \in A$
19	7 10 11 17 18	syl121anc	$⊢ ((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 (Q)) \in A$
20	2 4	hlatjcom	$⊢ (K \in HL \land F (G (P)) \in A \land F (G (Q)) \in A) \to F (G (P)) \underset{˙}{\lor} F (G (Q)) = F (G (Q)) \underset{˙}{\lor} F (G (P))$
21	13 16 19 20	syl3anc	$⊢ ((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)) = F (G (Q)) \underset{˙}{\lor} F (G (P))$
22	2 4	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
23	13 14 17 22	syl3anc	$⊢ ((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 P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
24	12 21 23	3netr3d	$⊢ ((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 (Q)) \underset{˙}{\lor} F (G (P)) \neq Q \underset{˙}{\lor} P$
25	1 2 3 4 5 6	cdlemg11a	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land F (G (Q)) \underset{˙}{\lor} F (G (P)) \neq Q \underset{˙}{\lor} P)) \to F (G (Q)) \neq Q$
26	7 8 9 10 11 24 25	syl123anc	$⊢ ((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 (Q)) \neq Q$

Metamath Proof Explorer

Theorem cdlemg11aq

Proof