cdlemk8

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 26-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)$
	cdlemk.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	cdlemk8	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G (P) \underset{˙}{\lor} X (P) = G (P) \underset{˙}{\lor} R (X \circ G^{-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		cdlemk.m	$⊢ \underset{˙}{\land} = meet (K)$
9		coass	$⊢ (X \circ G^{-1}) \circ G = X \circ (G^{-1} \circ G)$
10		simp1	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
11		simp2l	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \in T$
12	1 5 6	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : B \underset{1-1 onto}{⟶} B$
13	10 11 12	syl2anc	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G : B \underset{1-1 onto}{⟶} B$
14		f1ococnv1	$⊢ G : B \underset{1-1 onto}{⟶} B \to G^{-1} \circ G = {I ↾}_{B}$
15	13 14	syl	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G^{-1} \circ G = {I ↾}_{B}$
16	15	coeq2d	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \circ (G^{-1} \circ G) = X \circ ({I ↾}_{B})$
17		simp2r	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \in T$
18	1 5 6	ltrn1o	$⊢ ((K \in HL \land W \in H) \land X \in T) \to X : B \underset{1-1 onto}{⟶} B$
19	10 17 18	syl2anc	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X : B \underset{1-1 onto}{⟶} B$
20		f1of	$⊢ X : B \underset{1-1 onto}{⟶} B \to X : B ⟶ B$
21		fcoi1	$⊢ X : B ⟶ B \to X \circ ({I ↾}_{B}) = X$
22	19 20 21	3syl	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \circ ({I ↾}_{B}) = X$
23	16 22	eqtrd	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \circ (G^{-1} \circ G) = X$
24	9 23	syl5eq	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (X \circ G^{-1}) \circ G = X$
25	24	fveq1d	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((X \circ G^{-1}) \circ G) (P) = X (P)$
26	5 6	ltrncnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G^{-1} \in T$
27	10 11 26	syl2anc	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G^{-1} \in T$
28	5 6	ltrnco	$⊢ ((K \in HL \land W \in H) \land X \in T \land G^{-1} \in T) \to X \circ G^{-1} \in T$
29	10 17 27 28	syl3anc	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \circ G^{-1} \in T$
30		simp3l	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \in A$
31	2 4 5 6	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (X \circ G^{-1} \in T \land G \in T) \land P \in A) \to ((X \circ G^{-1}) \circ G) (P) = (X \circ G^{-1}) (G (P))$
32	10 29 11 30 31	syl121anc	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((X \circ G^{-1}) \circ G) (P) = (X \circ G^{-1}) (G (P))$
33	25 32	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X (P) = (X \circ G^{-1}) (G (P))$
34	33	oveq2d	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G (P) \underset{˙}{\lor} X (P) = G (P) \underset{˙}{\lor} (X \circ G^{-1}) (G (P))$
35	2 4 5 6	ltrnel	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
36	35	3adant2r	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
37	2 3 4 5 6 7	trljat1	$⊢ ((K \in HL \land W \in H) \land X \circ G^{-1} \in T \land (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)) \to G (P) \underset{˙}{\lor} R (X \circ G^{-1}) = G (P) \underset{˙}{\lor} (X \circ G^{-1}) (G (P))$
38	10 29 36 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G (P) \underset{˙}{\lor} R (X \circ G^{-1}) = G (P) \underset{˙}{\lor} (X \circ G^{-1}) (G (P))$
39	34 38	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G (P) \underset{˙}{\lor} X (P) = G (P) \underset{˙}{\lor} R (X \circ G^{-1})$

Metamath Proof Explorer

Theorem cdlemk8

Proof