cdlemd9

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 2-Jun-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	cdlemd9	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \to F (R) = G (R)$

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		simpl1	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) = P) \to ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A)$
7		simpl2	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) = P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
8		simpl3	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) = P) \to F (P) = G (P)$
9		simpr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) = P) \to F (P) = P$
10	1 2 3 4 5	cdlemd8	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F (P) = G (P) \land F (P) = P)) \to F (R) = G (R)$
11	6 7 8 9 10	syl112anc	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) = P) \to F (R) = G (R)$
12		simpl11	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \to (K \in HL \land W \in H)$
13		simpl2	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
14		simp12l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \to F \in T$
15	14	adantr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \to F \in T$
16	1 3 4 5	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
17	12 15 13 16	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
18		simpr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \to F (P) \neq P$
19	18	necomd	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \to P \neq F (P)$
20	1 2 3 4	cdlemb2	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \land P \neq F (P)) \to \exists s \in A (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))$
21	12 13 17 19 20	syl121anc	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \to \exists s \in A (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))$
22		simp1l1	$⊢ (((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \land s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A)$
23		simp1l2	$⊢ (((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \land s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
24		simp2	$⊢ (((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \land s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to s \in A$
25		simp3l	$⊢ (((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \land s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to \neg s \underset{˙}{\leq} W$
26	24 25	jca	$⊢ (((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \land s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to (s \in A \land \neg s \underset{˙}{\leq} W)$
27		simp1l3	$⊢ (((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \land s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to F (P) = G (P)$
28		simp3r	$⊢ (((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \land s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
29	1 2 3 4 5	cdlemd7	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land (F (P) = G (P) \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to F (R) = G (R)$
30	22 23 26 27 28 29	syl122anc	$⊢ (((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \land s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to F (R) = G (R)$
31	30	rexlimdv3a	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \to (\exists s \in A (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to F (R) = G (R))$
32	21 31	mpd	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land F (P) \neq P) \to F (R) = G (R)$
33	11 32	pm2.61dane	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \to F (R) = G (R)$

Metamath Proof Explorer

Theorem cdlemd9

Proof