cdlemd7

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 1-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	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 (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (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		simp1	$⊢ (((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 (F (P) = G (P) \land \neg Q \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)$
7		simp2l	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
8		simp2r	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
9		simp11l	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to K \in HL$
10	9	hllatd	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to K \in Lat$
11		simp2rl	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to Q \in A$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13	12 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
14	11 13	syl	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to Q \in {Base}_{K}$
15		simp2ll	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to P \in A$
16	12 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
17	15 16	syl	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to P \in {Base}_{K}$
18		simp11	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to (K \in HL \land W \in H)$
19		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 (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to F \in T$
20	12 4 5	ltrncl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in {Base}_{K}) \to F (P) \in {Base}_{K}$
21	18 19 17 20	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 (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to F (P) \in {Base}_{K}$
22		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 (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
23	12 1 2	latnlej1l	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land P \in {Base}_{K} \land F (P) \in {Base}_{K}) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to Q \neq P$
24	23	necomd	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land P \in {Base}_{K} \land F (P) \in {Base}_{K}) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to P \neq Q$
25	10 14 17 21 22 24	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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to P \neq Q$
26		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 (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to F (P) = G (P)$
27		simp12	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to (F \in T \land G \in T)$
28	1 2 3 4 5	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)$
29	18 27 7 8 22 26 28	syl231anc	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to F (Q) = G (Q)$
30	1 2 3 4 5	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)$
31	6 7 8 25 26 29 30	syl132anc	$⊢ (((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 (F (P) = G (P) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)))) \to F (R) = G (R)$

Metamath Proof Explorer

Theorem cdlemd7

Proof