trlval2

Description: The value of the trace of a lattice translation, given any atom P not under the fiducial co-atom W . Note: this requires only the weaker assumption K e. Lat ; we use K e. HL for convenience. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	trlval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	trlval2.j	$⊢ \underset{˙}{\lor} = join (K)$
	trlval2.m	$⊢ \underset{˙}{\land} = meet (K)$
	trlval2.a	$⊢ A = Atoms (K)$
	trlval2.h	$⊢ H = LHyp (K)$
	trlval2.t	$⊢ T = LTrn (K) (W)$
	trlval2.r	$⊢ R = trL (K) (W)$
Assertion	trlval2	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W$

Proof

Step	Hyp	Ref	Expression
1		trlval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		trlval2.j	$⊢ \underset{˙}{\lor} = join (K)$
3		trlval2.m	$⊢ \underset{˙}{\land} = meet (K)$
4		trlval2.a	$⊢ A = Atoms (K)$
5		trlval2.h	$⊢ H = LHyp (K)$
6		trlval2.t	$⊢ T = LTrn (K) (W)$
7		trlval2.r	$⊢ R = trL (K) (W)$
8		hllat	$⊢ K \in HL \to K \in Lat$
9	8	anim1i	$⊢ (K \in HL \land W \in H) \to (K \in Lat \land W \in H)$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 1 2 3 4 5 6 7	trlval	$⊢ ((K \in Lat \land W \in H) \land F \in T) \to R (F) = (ι x \in {Base}_{K} \| \forall q \in A (\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W))$
12	11	3adant3	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (F) = (ι x \in {Base}_{K} \| \forall q \in A (\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W))$
13		simp1l	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in Lat$
14		simp3l	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \in A$
15	10 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
16	14 15	syl	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \in {Base}_{K}$
17	10 5 6	ltrncl	$⊢ ((K \in Lat \land W \in H) \land F \in T \land P \in {Base}_{K}) \to F (P) \in {Base}_{K}$
18	16 17	syld3an3	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \in {Base}_{K}$
19	10 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land F (P) \in {Base}_{K}) \to P \underset{˙}{\lor} F (P) \in {Base}_{K}$
20	13 16 18 19	syl3anc	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} F (P) \in {Base}_{K}$
21		simp1r	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in H$
22	10 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
23	21 22	syl	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in {Base}_{K}$
24	10 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} F (P) \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W \in {Base}_{K}$
25	13 20 23 24	syl3anc	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W \in {Base}_{K}$
26		simpl3l	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land x \in {Base}_{K}) \to P \in A$
27		simpl3r	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land x \in {Base}_{K}) \to \neg P \underset{˙}{\leq} W$
28		breq1	$⊢ q = P \to (q \underset{˙}{\leq} W \leftrightarrow P \underset{˙}{\leq} W)$
29	28	notbid	$⊢ q = P \to (\neg q \underset{˙}{\leq} W \leftrightarrow \neg P \underset{˙}{\leq} W)$
30		id	$⊢ q = P \to q = P$
31		fveq2	$⊢ q = P \to F (q) = F (P)$
32	30 31	oveq12d	$⊢ q = P \to q \underset{˙}{\lor} F (q) = P \underset{˙}{\lor} F (P)$
33	32	oveq1d	$⊢ q = P \to (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W$
34	33	eqeq2d	$⊢ q = P \to (x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W \leftrightarrow x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W)$
35	29 34	imbi12d	$⊢ q = P \to ((\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W) \leftrightarrow (\neg P \underset{˙}{\leq} W \to x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W))$
36	35	rspcv	$⊢ P \in A \to (\forall q \in A (\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W) \to (\neg P \underset{˙}{\leq} W \to x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W))$
37	36	com23	$⊢ P \in A \to (\neg P \underset{˙}{\leq} W \to (\forall q \in A (\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W) \to x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W))$
38	26 27 37	sylc	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land x \in {Base}_{K}) \to (\forall q \in A (\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W) \to x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W)$
39		simp11	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land \neg q \underset{˙}{\leq} W \land q \in A) \to (K \in Lat \land W \in H)$
40		simp12	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land \neg q \underset{˙}{\leq} W \land q \in A) \to F \in T$
41		simp13l	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land \neg q \underset{˙}{\leq} W \land q \in A) \to P \in A$
42		simp13r	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land \neg q \underset{˙}{\leq} W \land q \in A) \to \neg P \underset{˙}{\leq} W$
43		simp3	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land \neg q \underset{˙}{\leq} W \land q \in A) \to q \in A$
44		simp2	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land \neg q \underset{˙}{\leq} W \land q \in A) \to \neg q \underset{˙}{\leq} W$
45	1 2 3 4 5 6	ltrnu	$⊢ (((K \in Lat \land W \in H) \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (q \in A \land \neg q \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W$
46	39 40 41 42 43 44 45	syl222anc	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land \neg q \underset{˙}{\leq} W \land q \in A) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W$
47		eqeq2	$⊢ (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W \to (x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W \leftrightarrow x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W)$
48	47	biimpd	$⊢ (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W \to (x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W)$
49	46 48	syl	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land \neg q \underset{˙}{\leq} W \land q \in A) \to (x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W)$
50	49	3exp	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (\neg q \underset{˙}{\leq} W \to (q \in A \to (x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W)))$
51	50	com24	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W \to (q \in A \to (\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W)))$
52	51	ralrimdv	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W \to \forall q \in A (\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W))$
53	52	adantr	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land x \in {Base}_{K}) \to (x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W \to \forall q \in A (\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W))$
54	38 53	impbid	$⊢ (((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land x \in {Base}_{K}) \to (\forall q \in A (\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W) \leftrightarrow x = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W)$
55	25 54	riota5	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (ι x \in {Base}_{K} \| \forall q \in A (\neg q \underset{˙}{\leq} W \to x = (q \underset{˙}{\lor} F (q)) \underset{˙}{\land} W)) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W$
56	12 55	eqtrd	$⊢ ((K \in Lat \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W$
57	9 56	syl3an1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem trlval2

Proof