cdlemk9

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 29-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	cdlemk9	$⊢ ((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)) \underset{˙}{\land} W = 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	1 2 3 4 5 6 7 8	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})$
10	9	oveq1d	$⊢ ((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)) \underset{˙}{\land} W = (G (P) \underset{˙}{\lor} R (X \circ G^{-1})) \underset{˙}{\land} W$
11		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)$
12	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)$
13	12	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)$
14		eqid	$⊢ 0. (K) = 0. (K)$
15	2 8 14 4 5	lhpmat	$⊢ ((K \in HL \land W \in H) \land (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)) \to G (P) \underset{˙}{\land} W = 0. (K)$
16	11 13 15	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 (P) \underset{˙}{\land} W = 0. (K)$
17	16	oveq1d	$⊢ ((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{˙}{\land} W) \underset{˙}{\lor} R (X \circ G^{-1}) = 0. (K) \underset{˙}{\lor} R (X \circ G^{-1})$
18		simp1l	$⊢ ((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$
19		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$
20		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$
21	2 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in A) \to G (P) \in A$
22	11 19 20 21	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) \in A$
23		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$
24	5 6	ltrncnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G^{-1} \in T$
25	11 19 24	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$
26	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$
27	11 23 25 26	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$
28	1 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land X \circ G^{-1} \in T) \to R (X \circ G^{-1}) \in B$
29	11 27 28	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 R (X \circ G^{-1}) \in B$
30		simp1r	$⊢ ((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 W \in H$
31	1 5	lhpbase	$⊢ W \in H \to W \in B$
32	30 31	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 W \in B$
33	2 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land X \circ G^{-1} \in T) \to R (X \circ G^{-1}) \underset{˙}{\leq} W$
34	11 27 33	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 R (X \circ G^{-1}) \underset{˙}{\leq} W$
35	1 2 3 8 4	atmod4i2	$⊢ (K \in HL \land (G (P) \in A \land R (X \circ G^{-1}) \in B \land W \in B) \land R (X \circ G^{-1}) \underset{˙}{\leq} W) \to (G (P) \underset{˙}{\land} W) \underset{˙}{\lor} R (X \circ G^{-1}) = (G (P) \underset{˙}{\lor} R (X \circ G^{-1})) \underset{˙}{\land} W$
36	18 22 29 32 34 35	syl131anc	$⊢ ((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{˙}{\land} W) \underset{˙}{\lor} R (X \circ G^{-1}) = (G (P) \underset{˙}{\lor} R (X \circ G^{-1})) \underset{˙}{\land} W$
37		hlol	$⊢ K \in HL \to K \in OL$
38	18 37	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 K \in OL$
39	1 3 14	olj02	$⊢ (K \in OL \land R (X \circ G^{-1}) \in B) \to 0. (K) \underset{˙}{\lor} R (X \circ G^{-1}) = R (X \circ G^{-1})$
40	38 29 39	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 0. (K) \underset{˙}{\lor} R (X \circ G^{-1}) = R (X \circ G^{-1})$
41	17 36 40	3eqtr3d	$⊢ ((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})) \underset{˙}{\land} W = R (X \circ G^{-1})$
42	10 41	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 (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W = R (X \circ G^{-1})$

Metamath Proof Explorer

Theorem cdlemk9

Proof