dia2dimlem1

Description: Lemma for dia2dim . Show properties of the auxiliary atom Q . Part of proof of Lemma M in Crawley p. 121 line 3. (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia2dimlem1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dia2dimlem1.j	$⊢ \underset{˙}{\lor} = join (K)$
	dia2dimlem1.m	$⊢ \underset{˙}{\land} = meet (K)$
	dia2dimlem1.a	$⊢ A = Atoms (K)$
	dia2dimlem1.h	$⊢ H = LHyp (K)$
	dia2dimlem1.t	$⊢ T = LTrn (K) (W)$
	dia2dimlem1.r	$⊢ R = trL (K) (W)$
	dia2dimlem1.q	$⊢ Q = (P \underset{˙}{\lor} U) \underset{˙}{\land} (F (P) \underset{˙}{\lor} V)$
	dia2dimlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
	dia2dimlem1.u	$⊢ φ \to (U \in A \land U \underset{˙}{\leq} W)$
	dia2dimlem1.v	$⊢ φ \to (V \in A \land V \underset{˙}{\leq} W)$
	dia2dimlem1.p	$⊢ φ \to (P \in A \land \neg P \underset{˙}{\leq} W)$
	dia2dimlem1.f	$⊢ φ \to (F \in T \land F (P) \neq P)$
	dia2dimlem1.rf	$⊢ φ \to R (F) \underset{˙}{\leq} (U \underset{˙}{\lor} V)$
	dia2dimlem1.uv	$⊢ φ \to U \neq V$
	dia2dimlem1.ru	$⊢ φ \to R (F) \neq U$
Assertion	dia2dimlem1	$⊢ φ \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dia2dimlem1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dia2dimlem1.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dia2dimlem1.a	$⊢ A = Atoms (K)$
5		dia2dimlem1.h	$⊢ H = LHyp (K)$
6		dia2dimlem1.t	$⊢ T = LTrn (K) (W)$
7		dia2dimlem1.r	$⊢ R = trL (K) (W)$
8		dia2dimlem1.q	$⊢ Q = (P \underset{˙}{\lor} U) \underset{˙}{\land} (F (P) \underset{˙}{\lor} V)$
9		dia2dimlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
10		dia2dimlem1.u	$⊢ φ \to (U \in A \land U \underset{˙}{\leq} W)$
11		dia2dimlem1.v	$⊢ φ \to (V \in A \land V \underset{˙}{\leq} W)$
12		dia2dimlem1.p	$⊢ φ \to (P \in A \land \neg P \underset{˙}{\leq} W)$
13		dia2dimlem1.f	$⊢ φ \to (F \in T \land F (P) \neq P)$
14		dia2dimlem1.rf	$⊢ φ \to R (F) \underset{˙}{\leq} (U \underset{˙}{\lor} V)$
15		dia2dimlem1.uv	$⊢ φ \to U \neq V$
16		dia2dimlem1.ru	$⊢ φ \to R (F) \neq U$
17	9	simpld	$⊢ φ \to K \in HL$
18	12	simpld	$⊢ φ \to P \in A$
19	1 4 5 6 7	trlat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to R (F) \in A$
20	9 12 13 19	syl3anc	$⊢ φ \to R (F) \in A$
21	10	simpld	$⊢ φ \to U \in A$
22	13	simpld	$⊢ φ \to F \in T$
23	1 4 5 6	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
24	9 22 12 23	syl3anc	$⊢ φ \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
25	24	simpld	$⊢ φ \to F (P) \in A$
26	11	simpld	$⊢ φ \to V \in A$
27	12	simprd	$⊢ φ \to \neg P \underset{˙}{\leq} W$
28	1 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \underset{˙}{\leq} W$
29	9 22 28	syl2anc	$⊢ φ \to R (F) \underset{˙}{\leq} W$
30	10	simprd	$⊢ φ \to U \underset{˙}{\leq} W$
31	17	hllatd	$⊢ φ \to K \in Lat$
32		eqid	$⊢ {Base}_{K} = {Base}_{K}$
33	32 4	atbase	$⊢ R (F) \in A \to R (F) \in {Base}_{K}$
34	20 33	syl	$⊢ φ \to R (F) \in {Base}_{K}$
35	32 4	atbase	$⊢ U \in A \to U \in {Base}_{K}$
36	21 35	syl	$⊢ φ \to U \in {Base}_{K}$
37	9	simprd	$⊢ φ \to W \in H$
38	32 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
39	37 38	syl	$⊢ φ \to W \in {Base}_{K}$
40	32 1 2	latjle12	$⊢ (K \in Lat \land (R (F) \in {Base}_{K} \land U \in {Base}_{K} \land W \in {Base}_{K})) \to ((R (F) \underset{˙}{\leq} W \land U \underset{˙}{\leq} W) \leftrightarrow (R (F) \underset{˙}{\lor} U) \underset{˙}{\leq} W)$
41	31 34 36 39 40	syl13anc	$⊢ φ \to ((R (F) \underset{˙}{\leq} W \land U \underset{˙}{\leq} W) \leftrightarrow (R (F) \underset{˙}{\lor} U) \underset{˙}{\leq} W)$
42	29 30 41	mpbi2and	$⊢ φ \to (R (F) \underset{˙}{\lor} U) \underset{˙}{\leq} W$
43	32 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
44	18 43	syl	$⊢ φ \to P \in {Base}_{K}$
45	32 2 4	hlatjcl	$⊢ (K \in HL \land R (F) \in A \land U \in A) \to R (F) \underset{˙}{\lor} U \in {Base}_{K}$
46	17 20 21 45	syl3anc	$⊢ φ \to R (F) \underset{˙}{\lor} U \in {Base}_{K}$
47	32 1	lattr	$⊢ (K \in Lat \land (P \in {Base}_{K} \land R (F) \underset{˙}{\lor} U \in {Base}_{K} \land W \in {Base}_{K})) \to ((P \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U) \land (R (F) \underset{˙}{\lor} U) \underset{˙}{\leq} W) \to P \underset{˙}{\leq} W)$
48	31 44 46 39 47	syl13anc	$⊢ φ \to ((P \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U) \land (R (F) \underset{˙}{\lor} U) \underset{˙}{\leq} W) \to P \underset{˙}{\leq} W)$
49	42 48	mpan2d	$⊢ φ \to (P \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U) \to P \underset{˙}{\leq} W)$
50	27 49	mtod	$⊢ φ \to \neg P \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U)$
51	11	simprd	$⊢ φ \to V \underset{˙}{\leq} W$
52	24	simprd	$⊢ φ \to \neg F (P) \underset{˙}{\leq} W$
53		nbrne2	$⊢ (V \underset{˙}{\leq} W \land \neg F (P) \underset{˙}{\leq} W) \to V \neq F (P)$
54	51 52 53	syl2anc	$⊢ φ \to V \neq F (P)$
55	54	necomd	$⊢ φ \to F (P) \neq V$
56	50 55	jca	$⊢ φ \to (\neg P \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U) \land F (P) \neq V)$
57	31	adantr	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to K \in Lat$
58	44	adantr	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to P \in {Base}_{K}$
59	32 2 4	hlatjcl	$⊢ (K \in HL \land V \in A \land U \in A) \to V \underset{˙}{\lor} U \in {Base}_{K}$
60	17 26 21 59	syl3anc	$⊢ φ \to V \underset{˙}{\lor} U \in {Base}_{K}$
61	60	adantr	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to V \underset{˙}{\lor} U \in {Base}_{K}$
62	39	adantr	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to W \in {Base}_{K}$
63	1 2 4	hlatlej2	$⊢ (K \in HL \land F (P) \in A \land V \in A) \to V \underset{˙}{\leq} (F (P) \underset{˙}{\lor} V)$
64	17 25 26 63	syl3anc	$⊢ φ \to V \underset{˙}{\leq} (F (P) \underset{˙}{\lor} V)$
65	64	adantr	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to V \underset{˙}{\leq} (F (P) \underset{˙}{\lor} V)$
66		simpr	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V$
67	65 66	breqtrrd	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to V \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
68	15	necomd	$⊢ φ \to V \neq U$
69	1 2 4	hlatexch2	$⊢ (K \in HL \land (V \in A \land P \in A \land U \in A) \land V \neq U) \to (V \underset{˙}{\leq} (P \underset{˙}{\lor} U) \to P \underset{˙}{\leq} (V \underset{˙}{\lor} U))$
70	17 26 18 21 68 69	syl131anc	$⊢ φ \to (V \underset{˙}{\leq} (P \underset{˙}{\lor} U) \to P \underset{˙}{\leq} (V \underset{˙}{\lor} U))$
71	70	adantr	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to (V \underset{˙}{\leq} (P \underset{˙}{\lor} U) \to P \underset{˙}{\leq} (V \underset{˙}{\lor} U))$
72	67 71	mpd	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to P \underset{˙}{\leq} (V \underset{˙}{\lor} U)$
73	32 4	atbase	$⊢ V \in A \to V \in {Base}_{K}$
74	26 73	syl	$⊢ φ \to V \in {Base}_{K}$
75	32 1 2	latjle12	$⊢ (K \in Lat \land (V \in {Base}_{K} \land U \in {Base}_{K} \land W \in {Base}_{K})) \to ((V \underset{˙}{\leq} W \land U \underset{˙}{\leq} W) \leftrightarrow (V \underset{˙}{\lor} U) \underset{˙}{\leq} W)$
76	31 74 36 39 75	syl13anc	$⊢ φ \to ((V \underset{˙}{\leq} W \land U \underset{˙}{\leq} W) \leftrightarrow (V \underset{˙}{\lor} U) \underset{˙}{\leq} W)$
77	51 30 76	mpbi2and	$⊢ φ \to (V \underset{˙}{\lor} U) \underset{˙}{\leq} W$
78	77	adantr	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to (V \underset{˙}{\lor} U) \underset{˙}{\leq} W$
79	32 1 57 58 61 62 72 78	lattrd	$⊢ (φ \land P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V) \to P \underset{˙}{\leq} W$
80	79	ex	$⊢ φ \to (P \underset{˙}{\lor} U = F (P) \underset{˙}{\lor} V \to P \underset{˙}{\leq} W)$
81	80	necon3bd	$⊢ φ \to (\neg P \underset{˙}{\leq} W \to P \underset{˙}{\lor} U \neq F (P) \underset{˙}{\lor} V)$
82	27 81	mpd	$⊢ φ \to P \underset{˙}{\lor} U \neq F (P) \underset{˙}{\lor} V$
83	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land F (P) \in A) \to F (P) \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
84	17 18 25 83	syl3anc	$⊢ φ \to F (P) \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
85	1 2 3 4 5 6 7	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$
86	9 22 12 85	syl3anc	$⊢ φ \to R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W$
87	86	oveq2d	$⊢ φ \to P \underset{˙}{\lor} R (F) = P \underset{˙}{\lor} ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W)$
88	32 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land F (P) \in A) \to P \underset{˙}{\lor} F (P) \in {Base}_{K}$
89	17 18 25 88	syl3anc	$⊢ φ \to P \underset{˙}{\lor} F (P) \in {Base}_{K}$
90	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land F (P) \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
91	17 18 25 90	syl3anc	$⊢ φ \to P \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
92	32 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (P \in A \land P \underset{˙}{\lor} F (P) \in {Base}_{K} \land W \in {Base}_{K}) \land P \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (P \underset{˙}{\lor} W)$
93	17 18 89 39 91 92	syl131anc	$⊢ φ \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (P \underset{˙}{\lor} W)$
94		eqid	$⊢ 1. (K) = 1. (K)$
95	1 2 94 4 5	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} W = 1. (K)$
96	9 12 95	syl2anc	$⊢ φ \to P \underset{˙}{\lor} W = 1. (K)$
97	96	oveq2d	$⊢ φ \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (P \underset{˙}{\lor} W) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} 1. (K)$
98		hlol	$⊢ K \in HL \to K \in OL$
99	17 98	syl	$⊢ φ \to K \in OL$
100	32 3 94	olm11	$⊢ (K \in OL \land P \underset{˙}{\lor} F (P) \in {Base}_{K}) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} F (P)$
101	99 89 100	syl2anc	$⊢ φ \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} F (P)$
102	97 101	eqtrd	$⊢ φ \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (P \underset{˙}{\lor} W) = P \underset{˙}{\lor} F (P)$
103	93 102	eqtrd	$⊢ φ \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W) = P \underset{˙}{\lor} F (P)$
104	87 103	eqtrd	$⊢ φ \to P \underset{˙}{\lor} R (F) = P \underset{˙}{\lor} F (P)$
105	84 104	breqtrrd	$⊢ φ \to F (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))$
106	2 4	hlatjcom	$⊢ (K \in HL \land U \in A \land V \in A) \to U \underset{˙}{\lor} V = V \underset{˙}{\lor} U$
107	17 21 26 106	syl3anc	$⊢ φ \to U \underset{˙}{\lor} V = V \underset{˙}{\lor} U$
108	14 107	breqtrd	$⊢ φ \to R (F) \underset{˙}{\leq} (V \underset{˙}{\lor} U)$
109	1 2 4	hlatexch2	$⊢ (K \in HL \land (R (F) \in A \land V \in A \land U \in A) \land R (F) \neq U) \to (R (F) \underset{˙}{\leq} (V \underset{˙}{\lor} U) \to V \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U))$
110	17 20 26 21 16 109	syl131anc	$⊢ φ \to (R (F) \underset{˙}{\leq} (V \underset{˙}{\lor} U) \to V \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U))$
111	108 110	mpd	$⊢ φ \to V \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U)$
112	105 111	jca	$⊢ φ \to (F (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land V \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U))$
113	1 2 3 4	ps-2c	$⊢ ((K \in HL \land P \in A \land R (F) \in A) \land (U \in A \land F (P) \in A \land V \in A) \land ((\neg P \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U) \land F (P) \neq V) \land P \underset{˙}{\lor} U \neq F (P) \underset{˙}{\lor} V \land (F (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land V \underset{˙}{\leq} (R (F) \underset{˙}{\lor} U)))) \to (P \underset{˙}{\lor} U) \underset{˙}{\land} (F (P) \underset{˙}{\lor} V) \in A$
114	17 18 20 21 25 26 56 82 112 113	syl333anc	$⊢ φ \to (P \underset{˙}{\lor} U) \underset{˙}{\land} (F (P) \underset{˙}{\lor} V) \in A$
115	8 114	eqeltrid	$⊢ φ \to Q \in A$
116	32 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land U \in A) \to P \underset{˙}{\lor} U \in {Base}_{K}$
117	17 18 21 116	syl3anc	$⊢ φ \to P \underset{˙}{\lor} U \in {Base}_{K}$
118	32 2 4	hlatjcl	$⊢ (K \in HL \land F (P) \in A \land V \in A) \to F (P) \underset{˙}{\lor} V \in {Base}_{K}$
119	17 25 26 118	syl3anc	$⊢ φ \to F (P) \underset{˙}{\lor} V \in {Base}_{K}$
120	32 1 3	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} U \in {Base}_{K} \land F (P) \underset{˙}{\lor} V \in {Base}_{K}) \to ((P \underset{˙}{\lor} U) \underset{˙}{\land} (F (P) \underset{˙}{\lor} V)) \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
121	31 117 119 120	syl3anc	$⊢ φ \to ((P \underset{˙}{\lor} U) \underset{˙}{\land} (F (P) \underset{˙}{\lor} V)) \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
122	8 121	eqbrtrid	$⊢ φ \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
123	32 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
124	115 123	syl	$⊢ φ \to Q \in {Base}_{K}$
125	32 1 3	latlem12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land P \underset{˙}{\lor} U \in {Base}_{K} \land W \in {Base}_{K})) \to ((Q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \land Q \underset{˙}{\leq} W) \leftrightarrow Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\land} W))$
126	31 124 117 39 125	syl13anc	$⊢ φ \to ((Q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \land Q \underset{˙}{\leq} W) \leftrightarrow Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\land} W))$
127	126	biimpd	$⊢ φ \to ((Q \underset{˙}{\leq} (P \underset{˙}{\lor} U) \land Q \underset{˙}{\leq} W) \to Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\land} W))$
128	122 127	mpand	$⊢ φ \to (Q \underset{˙}{\leq} W \to Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\land} W))$
129	128	imp	$⊢ (φ \land Q \underset{˙}{\leq} W) \to Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\land} W)$
130		eqid	$⊢ 0. (K) = 0. (K)$
131	1 3 130 4 5	lhpmat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\land} W = 0. (K)$
132	9 12 131	syl2anc	$⊢ φ \to P \underset{˙}{\land} W = 0. (K)$
133	132	oveq1d	$⊢ φ \to (P \underset{˙}{\land} W) \underset{˙}{\lor} U = 0. (K) \underset{˙}{\lor} U$
134	32 1 2 3 4	atmod4i1	$⊢ (K \in HL \land (U \in A \land P \in {Base}_{K} \land W \in {Base}_{K}) \land U \underset{˙}{\leq} W) \to (P \underset{˙}{\land} W) \underset{˙}{\lor} U = (P \underset{˙}{\lor} U) \underset{˙}{\land} W$
135	17 21 44 39 30 134	syl131anc	$⊢ φ \to (P \underset{˙}{\land} W) \underset{˙}{\lor} U = (P \underset{˙}{\lor} U) \underset{˙}{\land} W$
136	32 2 130	olj02	$⊢ (K \in OL \land U \in {Base}_{K}) \to 0. (K) \underset{˙}{\lor} U = U$
137	99 36 136	syl2anc	$⊢ φ \to 0. (K) \underset{˙}{\lor} U = U$
138	133 135 137	3eqtr3d	$⊢ φ \to (P \underset{˙}{\lor} U) \underset{˙}{\land} W = U$
139	138	adantr	$⊢ (φ \land Q \underset{˙}{\leq} W) \to (P \underset{˙}{\lor} U) \underset{˙}{\land} W = U$
140	129 139	breqtrd	$⊢ (φ \land Q \underset{˙}{\leq} W) \to Q \underset{˙}{\leq} U$
141		hlatl	$⊢ K \in HL \to K \in AtLat$
142	17 141	syl	$⊢ φ \to K \in AtLat$
143	142	adantr	$⊢ (φ \land Q \underset{˙}{\leq} W) \to K \in AtLat$
144	115	adantr	$⊢ (φ \land Q \underset{˙}{\leq} W) \to Q \in A$
145	21	adantr	$⊢ (φ \land Q \underset{˙}{\leq} W) \to U \in A$
146	1 4	atcmp	$⊢ (K \in AtLat \land Q \in A \land U \in A) \to (Q \underset{˙}{\leq} U \leftrightarrow Q = U)$
147	143 144 145 146	syl3anc	$⊢ (φ \land Q \underset{˙}{\leq} W) \to (Q \underset{˙}{\leq} U \leftrightarrow Q = U)$
148	140 147	mpbid	$⊢ (φ \land Q \underset{˙}{\leq} W) \to Q = U$
149	32 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} U \in {Base}_{K} \land F (P) \underset{˙}{\lor} V \in {Base}_{K}) \to ((P \underset{˙}{\lor} U) \underset{˙}{\land} (F (P) \underset{˙}{\lor} V)) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} V)$
150	31 117 119 149	syl3anc	$⊢ φ \to ((P \underset{˙}{\lor} U) \underset{˙}{\land} (F (P) \underset{˙}{\lor} V)) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} V)$
151	8 150	eqbrtrid	$⊢ φ \to Q \underset{˙}{\leq} (F (P) \underset{˙}{\lor} V)$
152	32 1 3	latlem12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land F (P) \underset{˙}{\lor} V \in {Base}_{K} \land W \in {Base}_{K})) \to ((Q \underset{˙}{\leq} (F (P) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} W) \leftrightarrow Q \underset{˙}{\leq} ((F (P) \underset{˙}{\lor} V) \underset{˙}{\land} W))$
153	31 124 119 39 152	syl13anc	$⊢ φ \to ((Q \underset{˙}{\leq} (F (P) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} W) \leftrightarrow Q \underset{˙}{\leq} ((F (P) \underset{˙}{\lor} V) \underset{˙}{\land} W))$
154	153	biimpd	$⊢ φ \to ((Q \underset{˙}{\leq} (F (P) \underset{˙}{\lor} V) \land Q \underset{˙}{\leq} W) \to Q \underset{˙}{\leq} ((F (P) \underset{˙}{\lor} V) \underset{˙}{\land} W))$
155	151 154	mpand	$⊢ φ \to (Q \underset{˙}{\leq} W \to Q \underset{˙}{\leq} ((F (P) \underset{˙}{\lor} V) \underset{˙}{\land} W))$
156	155	imp	$⊢ (φ \land Q \underset{˙}{\leq} W) \to Q \underset{˙}{\leq} ((F (P) \underset{˙}{\lor} V) \underset{˙}{\land} W)$
157	1 3 130 4 5	lhpmat	$⊢ ((K \in HL \land W \in H) \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\land} W = 0. (K)$
158	9 24 157	syl2anc	$⊢ φ \to F (P) \underset{˙}{\land} W = 0. (K)$
159	158	oveq1d	$⊢ φ \to (F (P) \underset{˙}{\land} W) \underset{˙}{\lor} V = 0. (K) \underset{˙}{\lor} V$
160	32 4	atbase	$⊢ F (P) \in A \to F (P) \in {Base}_{K}$
161	25 160	syl	$⊢ φ \to F (P) \in {Base}_{K}$
162	32 1 2 3 4	atmod4i1	$⊢ (K \in HL \land (V \in A \land F (P) \in {Base}_{K} \land W \in {Base}_{K}) \land V \underset{˙}{\leq} W) \to (F (P) \underset{˙}{\land} W) \underset{˙}{\lor} V = (F (P) \underset{˙}{\lor} V) \underset{˙}{\land} W$
163	17 26 161 39 51 162	syl131anc	$⊢ φ \to (F (P) \underset{˙}{\land} W) \underset{˙}{\lor} V = (F (P) \underset{˙}{\lor} V) \underset{˙}{\land} W$
164	32 2 130	olj02	$⊢ (K \in OL \land V \in {Base}_{K}) \to 0. (K) \underset{˙}{\lor} V = V$
165	99 74 164	syl2anc	$⊢ φ \to 0. (K) \underset{˙}{\lor} V = V$
166	159 163 165	3eqtr3d	$⊢ φ \to (F (P) \underset{˙}{\lor} V) \underset{˙}{\land} W = V$
167	166	adantr	$⊢ (φ \land Q \underset{˙}{\leq} W) \to (F (P) \underset{˙}{\lor} V) \underset{˙}{\land} W = V$
168	156 167	breqtrd	$⊢ (φ \land Q \underset{˙}{\leq} W) \to Q \underset{˙}{\leq} V$
169	26	adantr	$⊢ (φ \land Q \underset{˙}{\leq} W) \to V \in A$
170	1 4	atcmp	$⊢ (K \in AtLat \land Q \in A \land V \in A) \to (Q \underset{˙}{\leq} V \leftrightarrow Q = V)$
171	143 144 169 170	syl3anc	$⊢ (φ \land Q \underset{˙}{\leq} W) \to (Q \underset{˙}{\leq} V \leftrightarrow Q = V)$
172	168 171	mpbid	$⊢ (φ \land Q \underset{˙}{\leq} W) \to Q = V$
173	148 172	eqtr3d	$⊢ (φ \land Q \underset{˙}{\leq} W) \to U = V$
174	173	ex	$⊢ φ \to (Q \underset{˙}{\leq} W \to U = V)$
175	174	necon3ad	$⊢ φ \to (U \neq V \to \neg Q \underset{˙}{\leq} W)$
176	15 175	mpd	$⊢ φ \to \neg Q \underset{˙}{\leq} W$
177	115 176	jca	$⊢ φ \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$

Metamath Proof Explorer

Theorem dia2dimlem1

Proof