cdlemj1

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

	Ref	Expression
Hypotheses	cdlemj.b	$⊢ B = {Base}_{K}$
	cdlemj.h	$⊢ H = LHyp (K)$
	cdlemj.t	$⊢ T = LTrn (K) (W)$
	cdlemj.r	$⊢ R = trL (K) (W)$
	cdlemj.e	$⊢ E = TEndo (K) (W)$
	cdlemj.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemj.a	$⊢ A = Atoms (K)$
Assertion	cdlemj1	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to U (h) (p) = V (h) (p)$

Proof

Step	Hyp	Ref	Expression
1		cdlemj.b	$⊢ B = {Base}_{K}$
2		cdlemj.h	$⊢ H = LHyp (K)$
3		cdlemj.t	$⊢ T = LTrn (K) (W)$
4		cdlemj.r	$⊢ R = trL (K) (W)$
5		cdlemj.e	$⊢ E = TEndo (K) (W)$
6		cdlemj.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
7		cdlemj.a	$⊢ A = Atoms (K)$
8		simp123	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to U (F) = V (F)$
9	8	fveq1d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to U (F) (p) = V (F) (p)$
10	9	oveq1d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to U (F) (p) join (K) R (g \circ F^{-1}) = V (F) (p) join (K) R (g \circ F^{-1})$
11	10	oveq2d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to (p join (K) R (g)) meet (K) (U (F) (p) join (K) R (g \circ F^{-1})) = (p join (K) R (g)) meet (K) (V (F) (p) join (K) R (g \circ F^{-1}))$
12		simp11	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
13		simp131	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to F \in T$
14		simp22	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to g \in T$
15		simp121	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to U \in E$
16		simp33	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to (p \in A \land \neg p \underset{˙}{\leq} W)$
17		simp132	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to F \neq {I ↾}_{B}$
18		simp23	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to g \neq {I ↾}_{B}$
19		simp31	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to R (F) \neq R (g)$
20		eqid	$⊢ join (K) = join (K)$
21		eqid	$⊢ meet (K) = meet (K)$
22		eqid	$⊢ (p join (K) R (g)) meet (K) (U (F) (p) join (K) R (g \circ F^{-1})) = (p join (K) R (g)) meet (K) (U (F) (p) join (K) R (g \circ F^{-1}))$
23	1 6 20 21 7 2 3 4 5 22	cdlemi	$⊢ (((K \in HL \land W \in H) \land F \in T \land g \in T) \land (U \in E \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land g \neq {I ↾}_{B} \land R (F) \neq R (g))) \to U (g) (p) = (p join (K) R (g)) meet (K) (U (F) (p) join (K) R (g \circ F^{-1}))$
24	12 13 14 15 16 17 18 19 23	syl323anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to U (g) (p) = (p join (K) R (g)) meet (K) (U (F) (p) join (K) R (g \circ F^{-1}))$
25		simp122	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to V \in E$
26		eqid	$⊢ (p join (K) R (g)) meet (K) (V (F) (p) join (K) R (g \circ F^{-1})) = (p join (K) R (g)) meet (K) (V (F) (p) join (K) R (g \circ F^{-1}))$
27	1 6 20 21 7 2 3 4 5 26	cdlemi	$⊢ (((K \in HL \land W \in H) \land F \in T \land g \in T) \land (V \in E \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land g \neq {I ↾}_{B} \land R (F) \neq R (g))) \to V (g) (p) = (p join (K) R (g)) meet (K) (V (F) (p) join (K) R (g \circ F^{-1}))$
28	12 13 14 25 16 17 18 19 27	syl323anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to V (g) (p) = (p join (K) R (g)) meet (K) (V (F) (p) join (K) R (g \circ F^{-1}))$
29	11 24 28	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to U (g) (p) = V (g) (p)$
30	29	oveq1d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to U (g) (p) join (K) R (h \circ g^{-1}) = V (g) (p) join (K) R (h \circ g^{-1})$
31	30	oveq2d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to (p join (K) R (h)) meet (K) (U (g) (p) join (K) R (h \circ g^{-1})) = (p join (K) R (h)) meet (K) (V (g) (p) join (K) R (h \circ g^{-1}))$
32		simp133	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to h \in T$
33		simp21	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to h \neq {I ↾}_{B}$
34		simp32	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to R (g) \neq R (h)$
35		eqid	$⊢ (p join (K) R (h)) meet (K) (U (g) (p) join (K) R (h \circ g^{-1})) = (p join (K) R (h)) meet (K) (U (g) (p) join (K) R (h \circ g^{-1}))$
36	1 6 20 21 7 2 3 4 5 35	cdlemi	$⊢ (((K \in HL \land W \in H) \land g \in T \land h \in T) \land (U \in E \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (g \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (g) \neq R (h))) \to U (h) (p) = (p join (K) R (h)) meet (K) (U (g) (p) join (K) R (h \circ g^{-1}))$
37	12 14 32 15 16 18 33 34 36	syl323anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to U (h) (p) = (p join (K) R (h)) meet (K) (U (g) (p) join (K) R (h \circ g^{-1}))$
38		eqid	$⊢ (p join (K) R (h)) meet (K) (V (g) (p) join (K) R (h \circ g^{-1})) = (p join (K) R (h)) meet (K) (V (g) (p) join (K) R (h \circ g^{-1}))$
39	1 6 20 21 7 2 3 4 5 38	cdlemi	$⊢ (((K \in HL \land W \in H) \land g \in T \land h \in T) \land (V \in E \land (p \in A \land \neg p \underset{˙}{\leq} W)) \land (g \neq {I ↾}_{B} \land h \neq {I ↾}_{B} \land R (g) \neq R (h))) \to V (h) (p) = (p join (K) R (h)) meet (K) (V (g) (p) join (K) R (h \circ g^{-1}))$
40	12 14 32 25 16 18 33 34 39	syl323anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to V (h) (p) = (p join (K) R (h)) meet (K) (V (g) (p) join (K) R (h \circ g^{-1}))$
41	31 37 40	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in A \land \neg p \underset{˙}{\leq} W))) \to U (h) (p) = V (h) (p)$

Metamath Proof Explorer

Theorem cdlemj1

Proof