cdlemd5

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 30-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	cdlemd5	$⊢ (((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \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		fveq2	$⊢ R = P \to F (R) = F (P)$
7		fveq2	$⊢ R = P \to G (R) = G (P)$
8	6 7	eqeq12d	$⊢ R = P \to (F (R) = G (R) \leftrightarrow F (P) = G (P))$
9		simpll1	$⊢ (((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land R \neq P) \to ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A)$
10		simpl21	$⊢ ((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
11	10	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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land R \neq P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
12		simpl22	$⊢ ((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
13	12	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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land R \neq P) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
14		simp23	$⊢ (((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \to P \neq Q$
15	14	ad2antrr	$⊢ (((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land R \neq P) \to P \neq Q$
16		simplr	$⊢ (((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land R \neq P) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
17		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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land R \neq P) \to R \neq P$
18	15 16 17	3jca	$⊢ (((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land R \neq P) \to (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)$
19		simpll3	$⊢ (((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land R \neq P) \to (F (P) = G (P) \land F (Q) = G (Q))$
20	1 2 3 4 5	cdlemd4	$⊢ (((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (R) = G (R)$
21	9 11 13 18 19 20	syl131anc	$⊢ (((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land R \neq P) \to F (R) = G (R)$
22		simpl3l	$⊢ ((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to F (P) = G (P)$
23	8 21 22	pm2.61ne	$⊢ ((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to F (R) = G (R)$
24		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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A)$
25		simpl21	$⊢ ((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
26		simpl22	$⊢ ((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
27		simpl23	$⊢ ((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq Q$
28		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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
29	27 28	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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
30		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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (F (P) = G (P) \land F (Q) = G (Q))$
31	1 2 3 4 5	cdlemd2	$⊢ (((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (R) = G (R)$
32	24 25 26 29 30 31	syl131anc	$⊢ ((((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to F (R) = G (R)$
33	23 32	pm2.61dan	$⊢ (((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 (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \neq Q) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (R) = G (R)$

Metamath Proof Explorer

Theorem cdlemd5

Proof