cdlemk2

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 22-Jun-2013)

	Ref	Expression
Hypotheses	cdlemk.b	$⊢ B = {Base}_{K}$
	cdlemk.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemk.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemk.a	$⊢ A = Atoms (K)$
	cdlemk.h	$⊢ H = LHyp (K)$
	cdlemk.t	$⊢ T = LTrn (K) (W)$
	cdlemk.r	$⊢ R = trL (K) (W)$
Assertion	cdlemk2	$⊢ ((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)) \to G (P) \underset{˙}{\lor} R (G \circ F^{-1}) = F (P) \underset{˙}{\lor} R (G \circ F^{-1})$

Proof

Step	Hyp	Ref	Expression
1		cdlemk.b	$⊢ B = {Base}_{K}$
2		cdlemk.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemk.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemk.a	$⊢ A = Atoms (K)$
5		cdlemk.h	$⊢ H = LHyp (K)$
6		cdlemk.t	$⊢ T = LTrn (K) (W)$
7		cdlemk.r	$⊢ R = trL (K) (W)$
8		simp1	$⊢ ((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)) \to (K \in HL \land W \in H)$
9		simp2r	$⊢ ((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)) \to G \in T$
10		simp2l	$⊢ ((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)) \to F \in T$
11	5 6	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
12	8 10 11	syl2anc	$⊢ ((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)) \to F^{-1} \in T$
13	5 6	ltrnco	$⊢ ((K \in HL \land W \in H) \land G \in T \land F^{-1} \in T) \to G \circ F^{-1} \in T$
14	8 9 12 13	syl3anc	$⊢ ((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)) \to G \circ F^{-1} \in T$
15	2 4 5 6	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)$
16	15	3adant2r	$⊢ ((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)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
17	2 3 4 5 6 7	trljat3	$⊢ ((K \in HL \land W \in H) \land G \circ F^{-1} \in T \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} R (G \circ F^{-1}) = (G \circ F^{-1}) (F (P)) \underset{˙}{\lor} R (G \circ F^{-1})$
18	8 14 16 17	syl3anc	$⊢ ((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)) \to F (P) \underset{˙}{\lor} R (G \circ F^{-1}) = (G \circ F^{-1}) (F (P)) \underset{˙}{\lor} R (G \circ F^{-1})$
19		simp3l	$⊢ ((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)) \to P \in A$
20	2 4 5 6	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (G \circ F^{-1} \in T \land F \in T) \land P \in A) \to ((G \circ F^{-1}) \circ F) (P) = (G \circ F^{-1}) (F (P))$
21	8 14 10 19 20	syl121anc	$⊢ ((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)) \to ((G \circ F^{-1}) \circ F) (P) = (G \circ F^{-1}) (F (P))$
22		coass	$⊢ (G \circ F^{-1}) \circ F = G \circ (F^{-1} \circ F)$
23	1 5 6	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
24	8 10 23	syl2anc	$⊢ ((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)) \to F : B \underset{1-1 onto}{⟶} B$
25		f1ococnv1	$⊢ F : B \underset{1-1 onto}{⟶} B \to F^{-1} \circ F = {I ↾}_{B}$
26	24 25	syl	$⊢ ((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)) \to F^{-1} \circ F = {I ↾}_{B}$
27	26	coeq2d	$⊢ ((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)) \to G \circ (F^{-1} \circ F) = G \circ ({I ↾}_{B})$
28	1 5 6	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : B \underset{1-1 onto}{⟶} B$
29	8 9 28	syl2anc	$⊢ ((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)) \to G : B \underset{1-1 onto}{⟶} B$
30		f1of	$⊢ G : B \underset{1-1 onto}{⟶} B \to G : B ⟶ B$
31		fcoi1	$⊢ G : B ⟶ B \to G \circ ({I ↾}_{B}) = G$
32	29 30 31	3syl	$⊢ ((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)) \to G \circ ({I ↾}_{B}) = G$
33	27 32	eqtrd	$⊢ ((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)) \to G \circ (F^{-1} \circ F) = G$
34	22 33	syl5eq	$⊢ ((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)) \to (G \circ F^{-1}) \circ F = G$
35	34	fveq1d	$⊢ ((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)) \to ((G \circ F^{-1}) \circ F) (P) = G (P)$
36	21 35	eqtr3d	$⊢ ((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)) \to (G \circ F^{-1}) (F (P)) = G (P)$
37	36	oveq1d	$⊢ ((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)) \to (G \circ F^{-1}) (F (P)) \underset{˙}{\lor} R (G \circ F^{-1}) = G (P) \underset{˙}{\lor} R (G \circ F^{-1})$
38	18 37	eqtr2d	$⊢ ((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)) \to G (P) \underset{˙}{\lor} R (G \circ F^{-1}) = F (P) \underset{˙}{\lor} R (G \circ F^{-1})$

Metamath Proof Explorer

Theorem cdlemk2

Proof