djajN

Description: Transfer lattice join to DVecA partial vector space closed subspace join. Part of Lemma M of Crawley p. 120 line 29, with closed subspace join rather than subspace sum. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	djaj.k	$⊢ \underset{˙}{\lor} = join (K)$
	djaj.h	$⊢ H = LHyp (K)$
	djaj.i	$⊢ I = DIsoA (K) (W)$
	djaj.j	$⊢ J = vA (K) (W)$
Assertion	djajN	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (X \underset{˙}{\lor} Y) = I (X) J I (Y)$

Proof

Step	Hyp	Ref	Expression
1		djaj.k	$⊢ \underset{˙}{\lor} = join (K)$
2		djaj.h	$⊢ H = LHyp (K)$
3		djaj.i	$⊢ I = DIsoA (K) (W)$
4		djaj.j	$⊢ J = vA (K) (W)$
5		hllat	$⊢ K \in HL \to K \in Lat$
6	5	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to K \in Lat$
7		hlop	$⊢ K \in HL \to K \in OP$
8	7	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to K \in OP$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 2 3	diadmclN	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to X \in {Base}_{K}$
11	10	adantrr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to X \in {Base}_{K}$
12		eqid	$⊢ oc (K) = oc (K)$
13	9 12	opoccl	$⊢ (K \in OP \land X \in {Base}_{K}) \to oc (K) (X) \in {Base}_{K}$
14	8 11 13	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (X) \in {Base}_{K}$
15	9 2	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
16	15	ad2antlr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to W \in {Base}_{K}$
17	9 12	opoccl	$⊢ (K \in OP \land W \in {Base}_{K}) \to oc (K) (W) \in {Base}_{K}$
18	8 16 17	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (W) \in {Base}_{K}$
19	9 1	latjcl	$⊢ (K \in Lat \land oc (K) (X) \in {Base}_{K} \land oc (K) (W) \in {Base}_{K}) \to oc (K) (X) \underset{˙}{\lor} oc (K) (W) \in {Base}_{K}$
20	6 14 18 19	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (X) \underset{˙}{\lor} oc (K) (W) \in {Base}_{K}$
21		eqid	$⊢ meet (K) = meet (K)$
22	9 21	latmcl	$⊢ (K \in Lat \land oc (K) (X) \underset{˙}{\lor} oc (K) (W) \in {Base}_{K} \land W \in {Base}_{K}) \to (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K}$
23	6 20 16 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K}$
24	9 2 3	diadmclN	$⊢ ((K \in HL \land W \in H) \land Y \in dom I) \to Y \in {Base}_{K}$
25	24	adantrl	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to Y \in {Base}_{K}$
26	9 12	opoccl	$⊢ (K \in OP \land Y \in {Base}_{K}) \to oc (K) (Y) \in {Base}_{K}$
27	8 25 26	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (Y) \in {Base}_{K}$
28	9 1	latjcl	$⊢ (K \in Lat \land oc (K) (Y) \in {Base}_{K} \land oc (K) (W) \in {Base}_{K}) \to oc (K) (Y) \underset{˙}{\lor} oc (K) (W) \in {Base}_{K}$
29	6 27 18 28	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (Y) \underset{˙}{\lor} oc (K) (W) \in {Base}_{K}$
30	9 21	latmcl	$⊢ (K \in Lat \land oc (K) (Y) \underset{˙}{\lor} oc (K) (W) \in {Base}_{K} \land W \in {Base}_{K}) \to (oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K}$
31	6 29 16 30	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K}$
32	9 21	latmcl	$⊢ (K \in Lat \land (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K} \land (oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K}) \to ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \in {Base}_{K}$
33	6 23 31 32	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \in {Base}_{K}$
34		eqid	$⊢ \leq_{K} = \leq_{K}$
35	9 34 21	latmle2	$⊢ (K \in Lat \land (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K} \land (oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K}) \to (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \leq_{K} ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)$
36	6 23 31 35	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \leq_{K} ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)$
37	9 34 21	latmle2	$⊢ (K \in Lat \land oc (K) (Y) \underset{˙}{\lor} oc (K) (W) \in {Base}_{K} \land W \in {Base}_{K}) \to ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \leq_{K} W$
38	6 29 16 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \leq_{K} W$
39	9 34 6 33 31 16 36 38	lattrd	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \leq_{K} W$
40	9 34 2 3	diaeldm	$⊢ (K \in HL \land W \in H) \to (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \in dom I \leftrightarrow (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \in {Base}_{K} \land (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \leq_{K} W))$
41	40	adantr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \in dom I \leftrightarrow (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \in {Base}_{K} \land (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \leq_{K} W))$
42	33 39 41	mpbir2and	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \in dom I$
43		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
44		eqid	$⊢ ocA (K) (W) = ocA (K) (W)$
45	1 21 12 2 43 3 44	diaocN	$⊢ ((K \in HL \land W \in H) \land ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \in dom I) \to I ((oc (K) (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \underset{˙}{\lor} oc (K) (W)) meet (K) W) = ocA (K) (W) (I (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)))$
46	42 45	syldan	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I ((oc (K) (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \underset{˙}{\lor} oc (K) (W)) meet (K) W) = ocA (K) (W) (I (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)))$
47		hloml	$⊢ K \in HL \to K \in OML$
48	47	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to K \in OML$
49	9 1	latjcl	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to X \underset{˙}{\lor} Y \in {Base}_{K}$
50	6 11 25 49	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to X \underset{˙}{\lor} Y \in {Base}_{K}$
51	34 2 3	diadmleN	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to X \leq_{K} W$
52	51	adantrr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to X \leq_{K} W$
53	34 2 3	diadmleN	$⊢ ((K \in HL \land W \in H) \land Y \in dom I) \to Y \leq_{K} W$
54	53	adantrl	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to Y \leq_{K} W$
55	9 34 1	latjle12	$⊢ (K \in Lat \land (X \in {Base}_{K} \land Y \in {Base}_{K} \land W \in {Base}_{K})) \to ((X \leq_{K} W \land Y \leq_{K} W) \leftrightarrow (X \underset{˙}{\lor} Y) \leq_{K} W)$
56	6 11 25 16 55	syl13anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((X \leq_{K} W \land Y \leq_{K} W) \leftrightarrow (X \underset{˙}{\lor} Y) \leq_{K} W)$
57	52 54 56	mpbi2and	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (X \underset{˙}{\lor} Y) \leq_{K} W$
58	9 34 1 21 12	omlspjN	$⊢ (K \in OML \land (X \underset{˙}{\lor} Y \in {Base}_{K} \land W \in {Base}_{K}) \land (X \underset{˙}{\lor} Y) \leq_{K} W) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W = X \underset{˙}{\lor} Y$
59	48 50 16 57 58	syl121anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W = X \underset{˙}{\lor} Y$
60	9 1	latjidm	$⊢ (K \in Lat \land oc (K) (W) \in {Base}_{K}) \to oc (K) (W) \underset{˙}{\lor} oc (K) (W) = oc (K) (W)$
61	6 18 60	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (W) \underset{˙}{\lor} oc (K) (W) = oc (K) (W)$
62	61	oveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} (oc (K) (W) \underset{˙}{\lor} oc (K) (W)) = (X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)$
63	9 1	latjass	$⊢ (K \in Lat \land (X \underset{˙}{\lor} Y \in {Base}_{K} \land oc (K) (W) \in {Base}_{K} \land oc (K) (W) \in {Base}_{K})) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)) \underset{˙}{\lor} oc (K) (W) = (X \underset{˙}{\lor} Y) \underset{˙}{\lor} (oc (K) (W) \underset{˙}{\lor} oc (K) (W))$
64	6 50 18 18 63	syl13anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)) \underset{˙}{\lor} oc (K) (W) = (X \underset{˙}{\lor} Y) \underset{˙}{\lor} (oc (K) (W) \underset{˙}{\lor} oc (K) (W))$
65		hlol	$⊢ K \in HL \to K \in OL$
66	65	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to K \in OL$
67	9 1 21 12	oldmm2	$⊢ (K \in OL \land X \underset{˙}{\lor} Y \in {Base}_{K} \land W \in {Base}_{K}) \to oc (K) (oc (K) (X \underset{˙}{\lor} Y) meet (K) W) = (X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)$
68	66 50 16 67	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (oc (K) (X \underset{˙}{\lor} Y) meet (K) W) = (X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)$
69	9 1 21 12	oldmj1	$⊢ (K \in OL \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to oc (K) (X \underset{˙}{\lor} Y) = oc (K) (X) meet (K) oc (K) (Y)$
70	66 11 25 69	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (X \underset{˙}{\lor} Y) = oc (K) (X) meet (K) oc (K) (Y)$
71	9 34 21	latleeqm1	$⊢ (K \in Lat \land X \in {Base}_{K} \land W \in {Base}_{K}) \to (X \leq_{K} W \leftrightarrow X meet (K) W = X)$
72	6 11 16 71	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (X \leq_{K} W \leftrightarrow X meet (K) W = X)$
73	52 72	mpbid	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to X meet (K) W = X$
74	73	fveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (X meet (K) W) = oc (K) (X)$
75	9 1 21 12	oldmm1	$⊢ (K \in OL \land X \in {Base}_{K} \land W \in {Base}_{K}) \to oc (K) (X meet (K) W) = oc (K) (X) \underset{˙}{\lor} oc (K) (W)$
76	66 11 16 75	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (X meet (K) W) = oc (K) (X) \underset{˙}{\lor} oc (K) (W)$
77	74 76	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (X) = oc (K) (X) \underset{˙}{\lor} oc (K) (W)$
78	9 34 21	latleeqm1	$⊢ (K \in Lat \land Y \in {Base}_{K} \land W \in {Base}_{K}) \to (Y \leq_{K} W \leftrightarrow Y meet (K) W = Y)$
79	6 25 16 78	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (Y \leq_{K} W \leftrightarrow Y meet (K) W = Y)$
80	54 79	mpbid	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to Y meet (K) W = Y$
81	80	fveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (Y meet (K) W) = oc (K) (Y)$
82	9 1 21 12	oldmm1	$⊢ (K \in OL \land Y \in {Base}_{K} \land W \in {Base}_{K}) \to oc (K) (Y meet (K) W) = oc (K) (Y) \underset{˙}{\lor} oc (K) (W)$
83	66 25 16 82	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (Y meet (K) W) = oc (K) (Y) \underset{˙}{\lor} oc (K) (W)$
84	81 83	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (Y) = oc (K) (Y) \underset{˙}{\lor} oc (K) (W)$
85	77 84	oveq12d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (X) meet (K) oc (K) (Y) = (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) (oc (K) (Y) \underset{˙}{\lor} oc (K) (W))$
86	70 85	eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (X \underset{˙}{\lor} Y) = (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) (oc (K) (Y) \underset{˙}{\lor} oc (K) (W))$
87	86	oveq1d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (X \underset{˙}{\lor} Y) meet (K) W = ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) (oc (K) (Y) \underset{˙}{\lor} oc (K) (W))) meet (K) W$
88	9 21	latmmdir	$⊢ (K \in OL \land (oc (K) (X) \underset{˙}{\lor} oc (K) (W) \in {Base}_{K} \land oc (K) (Y) \underset{˙}{\lor} oc (K) (W) \in {Base}_{K} \land W \in {Base}_{K})) \to ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) (oc (K) (Y) \underset{˙}{\lor} oc (K) (W))) meet (K) W = ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)$
89	66 20 29 16 88	syl13anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) (oc (K) (Y) \underset{˙}{\lor} oc (K) (W))) meet (K) W = ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)$
90	87 89	eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (X \underset{˙}{\lor} Y) meet (K) W = ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)$
91	90	fveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to oc (K) (oc (K) (X \underset{˙}{\lor} Y) meet (K) W) = oc (K) (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W))$
92	68 91	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W) = oc (K) (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W))$
93	92	oveq1d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)) \underset{˙}{\lor} oc (K) (W) = oc (K) (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \underset{˙}{\lor} oc (K) (W)$
94	64 93	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} (oc (K) (W) \underset{˙}{\lor} oc (K) (W)) = oc (K) (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \underset{˙}{\lor} oc (K) (W)$
95	62 94	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W) = oc (K) (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \underset{˙}{\lor} oc (K) (W)$
96	95	oveq1d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W = (oc (K) (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \underset{˙}{\lor} oc (K) (W)) meet (K) W$
97	59 96	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to X \underset{˙}{\lor} Y = (oc (K) (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \underset{˙}{\lor} oc (K) (W)) meet (K) W$
98	97	fveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (X \underset{˙}{\lor} Y) = I ((oc (K) (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) \underset{˙}{\lor} oc (K) (W)) meet (K) W)$
99		simpl	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (K \in HL \land W \in H)$
100	2 3	diaclN	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to I (X) \in ran I$
101	100	adantrr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (X) \in ran I$
102	2 43 3	diaelrnN	$⊢ ((K \in HL \land W \in H) \land I (X) \in ran I) \to I (X) \subseteq LTrn (K) (W)$
103	101 102	syldan	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (X) \subseteq LTrn (K) (W)$
104	2 3	diaclN	$⊢ ((K \in HL \land W \in H) \land Y \in dom I) \to I (Y) \in ran I$
105	104	adantrl	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (Y) \in ran I$
106	2 43 3	diaelrnN	$⊢ ((K \in HL \land W \in H) \land I (Y) \in ran I) \to I (Y) \subseteq LTrn (K) (W)$
107	105 106	syldan	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (Y) \subseteq LTrn (K) (W)$
108	2 43 3 44 4	djavalN	$⊢ ((K \in HL \land W \in H) \land (I (X) \subseteq LTrn (K) (W) \land I (Y) \subseteq LTrn (K) (W))) \to I (X) J I (Y) = ocA (K) (W) (ocA (K) (W) (I (X)) \cap ocA (K) (W) (I (Y)))$
109	99 103 107 108	syl12anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (X) J I (Y) = ocA (K) (W) (ocA (K) (W) (I (X)) \cap ocA (K) (W) (I (Y)))$
110	9 34 21	latmle2	$⊢ (K \in Lat \land oc (K) (X) \underset{˙}{\lor} oc (K) (W) \in {Base}_{K} \land W \in {Base}_{K}) \to ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \leq_{K} W$
111	6 20 16 110	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \leq_{K} W$
112	9 34 2 3	diaeldm	$⊢ (K \in HL \land W \in H) \to ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in dom I \leftrightarrow ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K} \land ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \leq_{K} W))$
113	112	adantr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in dom I \leftrightarrow ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K} \land ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \leq_{K} W))$
114	23 111 113	mpbir2and	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in dom I$
115	9 34 2 3	diaeldm	$⊢ (K \in HL \land W \in H) \to ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in dom I \leftrightarrow ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K} \land ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \leq_{K} W))$
116	115	adantr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in dom I \leftrightarrow ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in {Base}_{K} \land ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \leq_{K} W))$
117	31 38 116	mpbir2and	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in dom I$
118	21 2 3	diameetN	$⊢ ((K \in HL \land W \in H) \land ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in dom I \land (oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W \in dom I)) \to I (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) = I ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \cap I ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)$
119	99 114 117 118	syl12anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) = I ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \cap I ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)$
120	1 21 12 2 43 3 44	diaocN	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to I ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) = ocA (K) (W) (I (X))$
121	120	adantrr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) = ocA (K) (W) (I (X))$
122	1 21 12 2 43 3 44	diaocN	$⊢ ((K \in HL \land W \in H) \land Y \in dom I) \to I ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) = ocA (K) (W) (I (Y))$
123	122	adantrl	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) = ocA (K) (W) (I (Y))$
124	121 123	ineq12d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I ((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) \cap I ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W) = ocA (K) (W) (I (X)) \cap ocA (K) (W) (I (Y))$
125	119 124	eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)) = ocA (K) (W) (I (X)) \cap ocA (K) (W) (I (Y))$
126	125	fveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ocA (K) (W) (I (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W))) = ocA (K) (W) (ocA (K) (W) (I (X)) \cap ocA (K) (W) (I (Y)))$
127	109 126	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (X) J I (Y) = ocA (K) (W) (I (((oc (K) (X) \underset{˙}{\lor} oc (K) (W)) meet (K) W) meet (K) ((oc (K) (Y) \underset{˙}{\lor} oc (K) (W)) meet (K) W)))$
128	46 98 127	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (X \underset{˙}{\lor} Y) = I (X) J I (Y)$

Metamath Proof Explorer

Theorem djajN

Proof