cdlemn3

Description: Part of proof of Lemma N of Crawley p. 121 line 31. (Contributed by NM, 21-Feb-2014)

	Ref	Expression
Hypotheses	cdlemn3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemn3.a	$⊢ A = Atoms (K)$
	cdlemn3.p	$⊢ P = oc (K) (W)$
	cdlemn3.h	$⊢ H = LHyp (K)$
	cdlemn3.t	$⊢ T = LTrn (K) (W)$
	cdlemn3.f	$⊢ F = (ι h \in T \| h (P) = Q)$
	cdlemn3.g	$⊢ G = (ι h \in T \| h (P) = R)$
	cdlemn3.j	$⊢ J = (ι h \in T \| h (Q) = R)$
Assertion	cdlemn3	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to J \circ F = G$

Proof

Step	Hyp	Ref	Expression
1		cdlemn3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemn3.a	$⊢ A = Atoms (K)$
3		cdlemn3.p	$⊢ P = oc (K) (W)$
4		cdlemn3.h	$⊢ H = LHyp (K)$
5		cdlemn3.t	$⊢ T = LTrn (K) (W)$
6		cdlemn3.f	$⊢ F = (ι h \in T \| h (P) = Q)$
7		cdlemn3.g	$⊢ G = (ι h \in T \| h (P) = R)$
8		cdlemn3.j	$⊢ J = (ι h \in T \| h (Q) = R)$
9		simp1	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
10	1 2 4 3	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
11	10	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
12		simp2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
13	1 2 4 5 6	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F \in T$
14	9 11 12 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to F \in T$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 4 5	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
17	9 14 16	syl2anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
18		f1of	$⊢ F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to F : {Base}_{K} ⟶ {Base}_{K}$
19	17 18	syl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to F : {Base}_{K} ⟶ {Base}_{K}$
20	11	simpld	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to P \in A$
21	15 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
22	20 21	syl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to P \in {Base}_{K}$
23		fvco3	$⊢ (F : {Base}_{K} ⟶ {Base}_{K} \land P \in {Base}_{K}) \to (J \circ F) (P) = J (F (P))$
24	19 22 23	syl2anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to (J \circ F) (P) = J (F (P))$
25	1 2 4 5 6	ltrniotaval	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F (P) = Q$
26	9 11 12 25	syl3anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to F (P) = Q$
27	26	fveq2d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to J (F (P)) = J (Q)$
28	1 2 4 5 8	ltrniotaval	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to J (Q) = R$
29	24 27 28	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to (J \circ F) (P) = R$
30	1 2 4 5 7	ltrniotaval	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to G (P) = R$
31	11 30	syld3an2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to G (P) = R$
32	29 31	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to (J \circ F) (P) = G (P)$
33	1 2 4 5 8	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to J \in T$
34	4 5	ltrnco	$⊢ ((K \in HL \land W \in H) \land J \in T \land F \in T) \to J \circ F \in T$
35	9 33 14 34	syl3anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to J \circ F \in T$
36	1 2 4 5 7	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to G \in T$
37	11 36	syld3an2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to G \in T$
38	1 2 4 5	ltrneq3	$⊢ ((K \in HL \land W \in H) \land (J \circ F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((J \circ F) (P) = G (P) \leftrightarrow J \circ F = G)$
39	9 35 37 11 38	syl121anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to ((J \circ F) (P) = G (P) \leftrightarrow J \circ F = G)$
40	32 39	mpbid	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to J \circ F = G$

Metamath Proof Explorer

Theorem cdlemn3

Proof