cdlemd8

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	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)$

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		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) = P)) \to F (P) = P$
7		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 (F (P) = G (P) \land F (P) = P)) \to (K \in HL \land W \in H)$
8		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) \land F (P) = P)) \to F \in T$
9		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) = P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 1 3 4 5	ltrnideq	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F = {I ↾}_{{Base}_{K}} \leftrightarrow F (P) = P)$
12	7 8 9 11	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) = P)) \to (F = {I ↾}_{{Base}_{K}} \leftrightarrow F (P) = P)$
13	6 12	mpbird	$⊢ (((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 = {I ↾}_{{Base}_{K}}$
14	13	fveq1d	$⊢ (((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) = ({I ↾}_{{Base}_{K}}) (R)$
15		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) = P)) \to F (P) = G (P)$
16	15 6	eqtr3d	$⊢ (((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 G (P) = P$
17		simp12r	$⊢ (((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 G \in T$
18	10 1 3 4 5	ltrnideq	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G = {I ↾}_{{Base}_{K}} \leftrightarrow G (P) = P)$
19	7 17 9 18	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) = P)) \to (G = {I ↾}_{{Base}_{K}} \leftrightarrow G (P) = P)$
20	16 19	mpbird	$⊢ (((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 G = {I ↾}_{{Base}_{K}}$
21	20	fveq1d	$⊢ (((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 G (R) = ({I ↾}_{{Base}_{K}}) (R)$
22	14 21	eqtr4d	$⊢ (((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)$

Metamath Proof Explorer

Theorem cdlemd8

Proof