cdlemd6

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 31-May-2012)

	Ref	Expression
Hypotheses	cdlemd4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemd4.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemd4.a	$⊢ A = Atoms (K)$
	cdlemd4.h	$⊢ H = LHyp (K)$
	cdlemd4.t	$⊢ T = LTrn (K) (W)$
Assertion	cdlemd6	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to F (Q) = G (Q)$

Proof

Step	Hyp	Ref	Expression
1		cdlemd4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemd4.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemd4.a	$⊢ A = Atoms (K)$
4		cdlemd4.h	$⊢ H = LHyp (K)$
5		cdlemd4.t	$⊢ T = LTrn (K) (W)$
6		simp3	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to F (P) = G (P)$
7	6	oveq2d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to P \underset{˙}{\lor} F (P) = P \underset{˙}{\lor} G (P)$
8	7	oveq1d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to (P \underset{˙}{\lor} F (P)) meet (K) W = (P \underset{˙}{\lor} G (P)) meet (K) W$
9		simp1l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to (K \in HL \land W \in H)$
10		simp1rl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to F \in T$
11		simp21	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
12		eqid	$⊢ meet (K) = meet (K)$
13		eqid	$⊢ trL (K) (W) = trL (K) (W)$
14	1 2 12 3 4 5 13	trlval2	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to trL (K) (W) (F) = (P \underset{˙}{\lor} F (P)) meet (K) W$
15	9 10 11 14	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to trL (K) (W) (F) = (P \underset{˙}{\lor} F (P)) meet (K) W$
16		simp1rr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to G \in T$
17	1 2 12 3 4 5 13	trlval2	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to trL (K) (W) (G) = (P \underset{˙}{\lor} G (P)) meet (K) W$
18	9 16 11 17	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to trL (K) (W) (G) = (P \underset{˙}{\lor} G (P)) meet (K) W$
19	8 15 18	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to trL (K) (W) (F) = trL (K) (W) (G)$
20	19	oveq2d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to Q \underset{˙}{\lor} trL (K) (W) (F) = Q \underset{˙}{\lor} trL (K) (W) (G)$
21	6	oveq1d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) meet (K) W) = G (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) meet (K) W)$
22	20 21	oveq12d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to (Q \underset{˙}{\lor} trL (K) (W) (F)) meet (K) (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) meet (K) W)) = (Q \underset{˙}{\lor} trL (K) (W) (G)) meet (K) (G (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) meet (K) W))$
23		simp22	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
24		simp23	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
25	1 2 12 3 4 5 13	cdlemc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to F (Q) = (Q \underset{˙}{\lor} trL (K) (W) (F)) meet (K) (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) meet (K) W))$
26	9 10 11 23 24 25	syl131anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to F (Q) = (Q \underset{˙}{\lor} trL (K) (W) (F)) meet (K) (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) meet (K) W))$
27		oveq2	$⊢ F (P) = G (P) \to P \underset{˙}{\lor} F (P) = P \underset{˙}{\lor} G (P)$
28	27	breq2d	$⊢ F (P) = G (P) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \leftrightarrow Q \underset{˙}{\leq} (P \underset{˙}{\lor} G (P)))$
29	28	notbid	$⊢ F (P) = G (P) \to (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \leftrightarrow \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} G (P)))$
30	29	biimpd	$⊢ F (P) = G (P) \to (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} G (P)))$
31	6 24 30	sylc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} G (P))$
32	1 2 12 3 4 5 13	cdlemc	$⊢ ((K \in HL \land W \in H) \land (G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} G (P))) \to G (Q) = (Q \underset{˙}{\lor} trL (K) (W) (G)) meet (K) (G (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) meet (K) W))$
33	9 16 11 23 31 32	syl131anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to G (Q) = (Q \underset{˙}{\lor} trL (K) (W) (G)) meet (K) (G (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) meet (K) W))$
34	22 26 33	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \land F (P) = G (P)) \to F (Q) = G (Q)$

Metamath Proof Explorer

Theorem cdlemd6

Proof