cdlemm10N

Description: The image of the map G is the entire one-dimensional subspace ( IV ) . Remark after Lemma M of Crawley p. 121 line 23. (Contributed by NM, 24-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemm10.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemm10.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemm10.a	$⊢ A = Atoms (K)$
	cdlemm10.h	$⊢ H = LHyp (K)$
	cdlemm10.t	$⊢ T = LTrn (K) (W)$
	cdlemm10.r	$⊢ R = trL (K) (W)$
	cdlemm10.i	$⊢ I = DIsoA (K) (W)$
	cdlemm10.c	$⊢ C = \{r \in A \| (r \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg r \underset{˙}{\leq} W)\}$
	cdlemm10.f	$⊢ F = (ι f \in T \| f (P) = s)$
	cdlemm10.g	$⊢ G = (q \in C ⟼ (ι f \in T \| f (P) = q))$
Assertion	cdlemm10N	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to ran G = I (V)$

Proof

Step	Hyp	Ref	Expression
1		cdlemm10.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemm10.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemm10.a	$⊢ A = Atoms (K)$
4		cdlemm10.h	$⊢ H = LHyp (K)$
5		cdlemm10.t	$⊢ T = LTrn (K) (W)$
6		cdlemm10.r	$⊢ R = trL (K) (W)$
7		cdlemm10.i	$⊢ I = DIsoA (K) (W)$
8		cdlemm10.c	$⊢ C = \{r \in A \| (r \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg r \underset{˙}{\leq} W)\}$
9		cdlemm10.f	$⊢ F = (ι f \in T \| f (P) = s)$
10		cdlemm10.g	$⊢ G = (q \in C ⟼ (ι f \in T \| f (P) = q))$
11		riotaex	$⊢ (ι f \in T \| f (P) = q) \in V$
12	11 10	fnmpti	$⊢ G Fn C$
13		fvelrnb	$⊢ G Fn C \to (g \in ran G \leftrightarrow \exists s \in C G (s) = g)$
14	12 13	ax-mp	$⊢ g \in ran G \leftrightarrow \exists s \in C G (s) = g$
15		eqeq2	$⊢ q = s \to (f (P) = q \leftrightarrow f (P) = s)$
16	15	riotabidv	$⊢ q = s \to (ι f \in T \| f (P) = q) = (ι f \in T \| f (P) = s)$
17		riotaex	$⊢ (ι f \in T \| f (P) = s) \in V$
18	16 10 17	fvmpt	$⊢ s \in C \to G (s) = (ι f \in T \| f (P) = s)$
19	18 9	eqtr4di	$⊢ s \in C \to G (s) = F$
20	19	adantl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land s \in C) \to G (s) = F$
21	20	eqeq1d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land s \in C) \to (G (s) = g \leftrightarrow F = g)$
22	21	rexbidva	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (\exists s \in C G (s) = g \leftrightarrow \exists s \in C F = g)$
23		simpl1	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to (K \in HL \land W \in H)$
24		simprl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to g \in T$
25		simpl2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to P \in A$
26	1 3 4 5	ltrnat	$⊢ ((K \in HL \land W \in H) \land g \in T \land P \in A) \to g (P) \in A$
27	23 24 25 26	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to g (P) \in A$
28		eqid	$⊢ {Base}_{K} = {Base}_{K}$
29		simpl1l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to K \in HL$
30	29	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to K \in Lat$
31	28 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
32	25 31	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to P \in {Base}_{K}$
33	28 4 5	ltrncl	$⊢ ((K \in HL \land W \in H) \land g \in T \land P \in {Base}_{K}) \to g (P) \in {Base}_{K}$
34	23 24 32 33	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to g (P) \in {Base}_{K}$
35	28 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land g (P) \in {Base}_{K}) \to P \underset{˙}{\lor} g (P) \in {Base}_{K}$
36	30 32 34 35	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to P \underset{˙}{\lor} g (P) \in {Base}_{K}$
37		simpl3l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to V \in A$
38	28 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land V \in A) \to P \underset{˙}{\lor} V \in {Base}_{K}$
39	29 25 37 38	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to P \underset{˙}{\lor} V \in {Base}_{K}$
40	28 1 2	latlej2	$⊢ (K \in Lat \land P \in {Base}_{K} \land g (P) \in {Base}_{K}) \to g (P) \underset{˙}{\leq} (P \underset{˙}{\lor} g (P))$
41	30 32 34 40	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to g (P) \underset{˙}{\leq} (P \underset{˙}{\lor} g (P))$
42		simpl2	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
43	1 2 3 4 5 6	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)$
44	23 24 42 43	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to P \underset{˙}{\lor} R (g) = P \underset{˙}{\lor} g (P)$
45		simprr	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to R (g) \underset{˙}{\leq} V$
46	28 4 5 6	trlcl	$⊢ ((K \in HL \land W \in H) \land g \in T) \to R (g) \in {Base}_{K}$
47	23 24 46	syl2anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to R (g) \in {Base}_{K}$
48	28 3	atbase	$⊢ V \in A \to V \in {Base}_{K}$
49	37 48	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to V \in {Base}_{K}$
50	28 1 2	latjlej2	$⊢ (K \in Lat \land (R (g) \in {Base}_{K} \land V \in {Base}_{K} \land P \in {Base}_{K})) \to (R (g) \underset{˙}{\leq} V \to (P \underset{˙}{\lor} R (g)) \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
51	30 47 49 32 50	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to (R (g) \underset{˙}{\leq} V \to (P \underset{˙}{\lor} R (g)) \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
52	45 51	mpd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to (P \underset{˙}{\lor} R (g)) \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
53	44 52	eqbrtrrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to (P \underset{˙}{\lor} g (P)) \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
54	28 1 30 34 36 39 41 53	lattrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to g (P) \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
55	1 3 4 5	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)$
56	55	simprd	$⊢ ((K \in HL \land W \in H) \land g \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to \neg g (P) \underset{˙}{\leq} W$
57	23 24 42 56	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to \neg g (P) \underset{˙}{\leq} W$
58	54 57	jca	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to (g (P) \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg g (P) \underset{˙}{\leq} W)$
59		breq1	$⊢ r = g (P) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} V) \leftrightarrow g (P) \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
60		breq1	$⊢ r = g (P) \to (r \underset{˙}{\leq} W \leftrightarrow g (P) \underset{˙}{\leq} W)$
61	60	notbid	$⊢ r = g (P) \to (\neg r \underset{˙}{\leq} W \leftrightarrow \neg g (P) \underset{˙}{\leq} W)$
62	59 61	anbi12d	$⊢ r = g (P) \to ((r \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg r \underset{˙}{\leq} W) \leftrightarrow (g (P) \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg g (P) \underset{˙}{\leq} W))$
63	62 8	elrab2	$⊢ g (P) \in C \leftrightarrow (g (P) \in A \land (g (P) \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg g (P) \underset{˙}{\leq} W))$
64	27 58 63	sylanbrc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to g (P) \in C$
65	1 3 4 5	cdlemeiota	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land g \in T) \to g = (ι f \in T \| f (P) = g (P))$
66	23 42 24 65	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to g = (ι f \in T \| f (P) = g (P))$
67	66	eqcomd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to (ι f \in T \| f (P) = g (P)) = g$
68		eqeq2	$⊢ s = g (P) \to (f (P) = s \leftrightarrow f (P) = g (P))$
69	68	riotabidv	$⊢ s = g (P) \to (ι f \in T \| f (P) = s) = (ι f \in T \| f (P) = g (P))$
70	9 69	syl5eq	$⊢ s = g (P) \to F = (ι f \in T \| f (P) = g (P))$
71	70	eqeq1d	$⊢ s = g (P) \to (F = g \leftrightarrow (ι f \in T \| f (P) = g (P)) = g)$
72	71	rspcev	$⊢ (g (P) \in C \land (ι f \in T \| f (P) = g (P)) = g) \to \exists s \in C F = g$
73	64 67 72	syl2anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (g \in T \land R (g) \underset{˙}{\leq} V)) \to \exists s \in C F = g$
74	73	ex	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to ((g \in T \land R (g) \underset{˙}{\leq} V) \to \exists s \in C F = g)$
75		breq1	$⊢ r = s \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} V) \leftrightarrow s \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
76		breq1	$⊢ r = s \to (r \underset{˙}{\leq} W \leftrightarrow s \underset{˙}{\leq} W)$
77	76	notbid	$⊢ r = s \to (\neg r \underset{˙}{\leq} W \leftrightarrow \neg s \underset{˙}{\leq} W)$
78	75 77	anbi12d	$⊢ r = s \to ((r \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg r \underset{˙}{\leq} W) \leftrightarrow (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))$
79	78 8	elrab2	$⊢ s \in C \leftrightarrow (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))$
80		simpl1	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
81		simpl2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to P \in A$
82		simpl2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to \neg P \underset{˙}{\leq} W$
83		simprl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to s \in A$
84		simprrr	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to \neg s \underset{˙}{\leq} W$
85	1 3 4 5 9	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (s \in A \land \neg s \underset{˙}{\leq} W)) \to F \in T$
86	1 3 4 5 9	ltrniotaval	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (s \in A \land \neg s \underset{˙}{\leq} W)) \to F (P) = s$
87	85 86	jca	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (s \in A \land \neg s \underset{˙}{\leq} W)) \to (F \in T \land F (P) = s)$
88	80 81 82 83 84 87	syl122anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to (F \in T \land F (P) = s)$
89		simp3l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to F \in T$
90		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to (K \in HL \land W \in H)$
91		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
92		eqid	$⊢ meet (K) = meet (K)$
93	1 2 92 3 4 5 6	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)) meet (K) W$
94	90 89 91 93	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to R (F) = (P \underset{˙}{\lor} F (P)) meet (K) W$
95		simp3r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to F (P) = s$
96	95	oveq2d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to P \underset{˙}{\lor} F (P) = P \underset{˙}{\lor} s$
97	96	oveq1d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to (P \underset{˙}{\lor} F (P)) meet (K) W = (P \underset{˙}{\lor} s) meet (K) W$
98	94 97	eqtrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to R (F) = (P \underset{˙}{\lor} s) meet (K) W$
99		simpl1l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to K \in HL$
100		simpl3l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to V \in A$
101	1 2 3	hlatlej1	$⊢ (K \in HL \land P \in A \land V \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
102	99 81 100 101	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
103		simprrl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to s \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
104	99	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to K \in Lat$
105	81 31	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to P \in {Base}_{K}$
106	28 3	atbase	$⊢ s \in A \to s \in {Base}_{K}$
107	106	ad2antrl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to s \in {Base}_{K}$
108	99 81 100 38	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} V \in {Base}_{K}$
109	28 1 2	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land s \in {Base}_{K} \land P \underset{˙}{\lor} V \in {Base}_{K})) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land s \underset{˙}{\leq} (P \underset{˙}{\lor} V)) \leftrightarrow (P \underset{˙}{\lor} s) \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
110	104 105 107 108 109	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land s \underset{˙}{\leq} (P \underset{˙}{\lor} V)) \leftrightarrow (P \underset{˙}{\lor} s) \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
111	102 103 110	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} s) \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
112	28 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land s \in A) \to P \underset{˙}{\lor} s \in {Base}_{K}$
113	99 81 83 112	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} s \in {Base}_{K}$
114		simpl1r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to W \in H$
115	28 4	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
116	114 115	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to W \in {Base}_{K}$
117	28 1 92	latmlem1	$⊢ (K \in Lat \land (P \underset{˙}{\lor} s \in {Base}_{K} \land P \underset{˙}{\lor} V \in {Base}_{K} \land W \in {Base}_{K})) \to ((P \underset{˙}{\lor} s) \underset{˙}{\leq} (P \underset{˙}{\lor} V) \to ((P \underset{˙}{\lor} s) meet (K) W) \underset{˙}{\leq} ((P \underset{˙}{\lor} V) meet (K) W))$
118	104 113 108 116 117	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to ((P \underset{˙}{\lor} s) \underset{˙}{\leq} (P \underset{˙}{\lor} V) \to ((P \underset{˙}{\lor} s) meet (K) W) \underset{˙}{\leq} ((P \underset{˙}{\lor} V) meet (K) W))$
119	111 118	mpd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to ((P \underset{˙}{\lor} s) meet (K) W) \underset{˙}{\leq} ((P \underset{˙}{\lor} V) meet (K) W)$
120	1 2 92 3 4	lhpat4N	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} V) meet (K) W = V$
121	120	adantr	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} V) meet (K) W = V$
122	119 121	breqtrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to ((P \underset{˙}{\lor} s) meet (K) W) \underset{˙}{\leq} V$
123	122	3adant3	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to ((P \underset{˙}{\lor} s) meet (K) W) \underset{˙}{\leq} V$
124	98 123	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to R (F) \underset{˙}{\leq} V$
125	89 124	jca	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W)) \land (F \in T \land F (P) = s)) \to (F \in T \land R (F) \underset{˙}{\leq} V)$
126	88 125	mpd3an3	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land (s \in A \land (s \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land \neg s \underset{˙}{\leq} W))) \to (F \in T \land R (F) \underset{˙}{\leq} V)$
127	79 126	sylan2b	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land s \in C) \to (F \in T \land R (F) \underset{˙}{\leq} V)$
128	127	ex	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (s \in C \to (F \in T \land R (F) \underset{˙}{\leq} V))$
129		eleq1	$⊢ F = g \to (F \in T \leftrightarrow g \in T)$
130		fveq2	$⊢ F = g \to R (F) = R (g)$
131	130	breq1d	$⊢ F = g \to (R (F) \underset{˙}{\leq} V \leftrightarrow R (g) \underset{˙}{\leq} V)$
132	129 131	anbi12d	$⊢ F = g \to ((F \in T \land R (F) \underset{˙}{\leq} V) \leftrightarrow (g \in T \land R (g) \underset{˙}{\leq} V))$
133	132	biimpcd	$⊢ (F \in T \land R (F) \underset{˙}{\leq} V) \to (F = g \to (g \in T \land R (g) \underset{˙}{\leq} V))$
134	128 133	syl6	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (s \in C \to (F = g \to (g \in T \land R (g) \underset{˙}{\leq} V)))$
135	134	rexlimdv	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (\exists s \in C F = g \to (g \in T \land R (g) \underset{˙}{\leq} V))$
136	74 135	impbid	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to ((g \in T \land R (g) \underset{˙}{\leq} V) \leftrightarrow \exists s \in C F = g)$
137	22 136	bitr4d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (\exists s \in C G (s) = g \leftrightarrow (g \in T \land R (g) \underset{˙}{\leq} V))$
138		fveq2	$⊢ f = g \to R (f) = R (g)$
139	138	breq1d	$⊢ f = g \to (R (f) \underset{˙}{\leq} V \leftrightarrow R (g) \underset{˙}{\leq} V)$
140	139	elrab	$⊢ g \in \{f \in T \| R (f) \underset{˙}{\leq} V\} \leftrightarrow (g \in T \land R (g) \underset{˙}{\leq} V)$
141	137 140	bitr4di	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (\exists s \in C G (s) = g \leftrightarrow g \in \{f \in T \| R (f) \underset{˙}{\leq} V\})$
142		simp1l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in HL$
143		simp1r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to W \in H$
144		simp3l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \in A$
145	144 48	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \in {Base}_{K}$
146		simp3r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \underset{˙}{\leq} W$
147	28 1 4 5 6 7	diaval	$⊢ ((K \in HL \land W \in H) \land (V \in {Base}_{K} \land V \underset{˙}{\leq} W)) \to I (V) = \{f \in T \| R (f) \underset{˙}{\leq} V\}$
148	142 143 145 146 147	syl22anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to I (V) = \{f \in T \| R (f) \underset{˙}{\leq} V\}$
149	148	eleq2d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (g \in I (V) \leftrightarrow g \in \{f \in T \| R (f) \underset{˙}{\leq} V\})$
150	141 149	bitr4d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (\exists s \in C G (s) = g \leftrightarrow g \in I (V))$
151	14 150	syl5bb	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (g \in ran G \leftrightarrow g \in I (V))$
152	151	eqrdv	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to ran G = I (V)$

Metamath Proof Explorer

Theorem cdlemm10N

Proof