cdlemk21N

Description: Part of proof of Lemma K of Crawley p. 118. Lines 26-27, p. 119 for i=0 and j=1. (Contributed by NM, 5-Jul-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemk1.b	$⊢ B = {Base}_{K}$
	cdlemk1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemk1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemk1.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemk1.a	$⊢ A = Atoms (K)$
	cdlemk1.h	$⊢ H = LHyp (K)$
	cdlemk1.t	$⊢ T = LTrn (K) (W)$
	cdlemk1.r	$⊢ R = trL (K) (W)$
	cdlemk1.s	$⊢ S = (f \in T ⟼ (ι i \in T \| i (P) = (P \underset{˙}{\lor} R (f)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (f \circ F^{-1}))))$
	cdlemk1.o	$⊢ O = S (D)$
	cdlemk1.u	$⊢ U = (e \in T ⟼ (ι j \in T \| j (P) = (P \underset{˙}{\lor} R (e)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (e \circ D^{-1}))))$
Assertion	cdlemk21N	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to S (G) (P) = U (G) (P)$

Proof

Step	Hyp	Ref	Expression
1		cdlemk1.b	$⊢ B = {Base}_{K}$
2		cdlemk1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemk1.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemk1.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemk1.a	$⊢ A = Atoms (K)$
6		cdlemk1.h	$⊢ H = LHyp (K)$
7		cdlemk1.t	$⊢ T = LTrn (K) (W)$
8		cdlemk1.r	$⊢ R = trL (K) (W)$
9		cdlemk1.s	$⊢ S = (f \in T ⟼ (ι i \in T \| i (P) = (P \underset{˙}{\lor} R (f)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (f \circ F^{-1}))))$
10		cdlemk1.o	$⊢ O = S (D)$
11		cdlemk1.u	$⊢ U = (e \in T ⟼ (ι j \in T \| j (P) = (P \underset{˙}{\lor} R (e)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (e \circ D^{-1}))))$
12		simp11	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to (K \in HL \land W \in H)$
13		simp21r	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to G \in T$
14		simp22	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
15	2 3 5 6 7 8	trljat1	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} R (G) = P \underset{˙}{\lor} G (P)$
16	12 13 14 15	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to P \underset{˙}{\lor} R (G) = P \underset{˙}{\lor} G (P)$
17	10	fveq1i	$⊢ O (P) = S (D) (P)$
18	17	a1i	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to O (P) = S (D) (P)$
19		simp13	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to D \in T$
20	6 7 8	trlcocnv	$⊢ ((K \in HL \land W \in H) \land G \in T \land D \in T) \to R (G \circ D^{-1}) = R (D \circ G^{-1})$
21	12 13 19 20	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to R (G \circ D^{-1}) = R (D \circ G^{-1})$
22	18 21	oveq12d	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to O (P) \underset{˙}{\lor} R (G \circ D^{-1}) = S (D) (P) \underset{˙}{\lor} R (D \circ G^{-1})$
23	16 22	oveq12d	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1})) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (S (D) (P) \underset{˙}{\lor} R (D \circ G^{-1}))$
24		simp23	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to R (F) = R (N)$
25		simp12	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to F \in T$
26		simp21l	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to N \in T$
27		simp3r1	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to R (D) \neq R (F)$
28		simp3r2	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to R (G) \neq R (D)$
29	28	necomd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to R (D) \neq R (G)$
30	27 29	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to (R (D) \neq R (F) \land R (D) \neq R (G))$
31		simp3l1	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to F \neq {I ↾}_{B}$
32		simp3l3	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to G \neq {I ↾}_{B}$
33		simp3l2	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to D \neq {I ↾}_{B}$
34	31 32 33	3jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land D \neq {I ↾}_{B})$
35	1 2 3 4 5 6 7 8 9 10 11	cdlemkuv2	$⊢ (((K \in HL \land W \in H) \land R (F) = R (N) \land G \in T) \land (F \in T \land D \in T \land N \in T) \land ((R (D) \neq R (F) \land R (D) \neq R (G)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land D \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to U (G) (P) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))$
36	12 24 13 25 19 26 30 34 14 35	syl333anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to U (G) (P) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))$
37	26 19	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to (N \in T \land D \in T)$
38		simp3r3	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to R (G) \neq R (F)$
39	38 27	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to (R (G) \neq R (F) \land R (D) \neq R (F))$
40	1 2 3 5 6 7 8 4 9	cdlemk12	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land D \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land D \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (D) \neq R (F)) \land R (G) \neq R (D))) \to S (G) (P) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (S (D) (P) \underset{˙}{\lor} R (D \circ G^{-1}))$
41	12 25 13 37 14 24 34 39 28 40	syl333anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to S (G) (P) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (S (D) (P) \underset{˙}{\lor} R (D \circ G^{-1}))$
42	23 36 41	3eqtr4rd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (G) \neq R (F)))) \to S (G) (P) = U (G) (P)$

Metamath Proof Explorer

Theorem cdlemk21N

Proof