dihmeetlem13N

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihmeetlem13.b	$⊢ B = {Base}_{K}$
	dihmeetlem13.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihmeetlem13.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihmeetlem13.a	$⊢ A = Atoms (K)$
	dihmeetlem13.h	$⊢ H = LHyp (K)$
	dihmeetlem13.p	$⊢ P = oc (K) (W)$
	dihmeetlem13.t	$⊢ T = LTrn (K) (W)$
	dihmeetlem13.e	$⊢ E = TEndo (K) (W)$
	dihmeetlem13.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	dihmeetlem13.i	$⊢ I = DIsoH (K) (W)$
	dihmeetlem13.u	$⊢ U = DVecH (K) (W)$
	dihmeetlem13.z	$⊢ \underset{˙}{0} = 0_{U}$
	dihmeetlem13.f	$⊢ F = (ι h \in T \| h (P) = Q)$
	dihmeetlem13.g	$⊢ G = (ι h \in T \| h (P) = R)$
Assertion	dihmeetlem13N	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to I (Q) \cap I (R) = \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem13.b	$⊢ B = {Base}_{K}$
2		dihmeetlem13.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetlem13.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dihmeetlem13.a	$⊢ A = Atoms (K)$
5		dihmeetlem13.h	$⊢ H = LHyp (K)$
6		dihmeetlem13.p	$⊢ P = oc (K) (W)$
7		dihmeetlem13.t	$⊢ T = LTrn (K) (W)$
8		dihmeetlem13.e	$⊢ E = TEndo (K) (W)$
9		dihmeetlem13.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
10		dihmeetlem13.i	$⊢ I = DIsoH (K) (W)$
11		dihmeetlem13.u	$⊢ U = DVecH (K) (W)$
12		dihmeetlem13.z	$⊢ \underset{˙}{0} = 0_{U}$
13		dihmeetlem13.f	$⊢ F = (ι h \in T \| h (P) = Q)$
14		dihmeetlem13.g	$⊢ G = (ι h \in T \| h (P) = R)$
15	5 10	dihvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (Q)$
16	15	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to Rel I (Q)$
17		relin1	$⊢ Rel I (Q) \to Rel (I (Q) \cap I (R))$
18	16 17	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to Rel (I (Q) \cap I (R))$
19		elin	$⊢ ⟨f, s⟩ \in (I (Q) \cap I (R)) \leftrightarrow (⟨f, s⟩ \in I (Q) \land ⟨f, s⟩ \in I (R))$
20		simp1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to (K \in HL \land W \in H)$
21		simp2l	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
22		vex	$⊢ f \in V$
23		vex	$⊢ s \in V$
24	2 4 5 6 7 8 10 13 22 23	dihopelvalcqat	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in I (Q) \leftrightarrow (f = s (F) \land s \in E))$
25	20 21 24	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to (⟨f, s⟩ \in I (Q) \leftrightarrow (f = s (F) \land s \in E))$
26		simp2r	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
27	2 4 5 6 7 8 10 14 22 23	dihopelvalcqat	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in I (R) \leftrightarrow (f = s (G) \land s \in E))$
28	20 26 27	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to (⟨f, s⟩ \in I (R) \leftrightarrow (f = s (G) \land s \in E))$
29	25 28	anbi12d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to ((⟨f, s⟩ \in I (Q) \land ⟨f, s⟩ \in I (R)) \leftrightarrow ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)))$
30	19 29	bitrid	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to (⟨f, s⟩ \in (I (Q) \cap I (R)) \leftrightarrow ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)))$
31		simprll	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to f = s (F)$
32		simpl3	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to Q \neq R$
33		fveq1	$⊢ F = G \to F (P) = G (P)$
34		simpl1	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to (K \in HL \land W \in H)$
35	2 4 5 6	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
36	34 35	syl	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
37		simpl2l	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
38	2 4 5 7 13	ltrniotaval	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F (P) = Q$
39	34 36 37 38	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to F (P) = Q$
40		simpl2r	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
41	2 4 5 7 14	ltrniotaval	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to G (P) = R$
42	34 36 40 41	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to G (P) = R$
43	39 42	eqeq12d	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to (F (P) = G (P) \leftrightarrow Q = R)$
44	33 43	imbitrid	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to (F = G \to Q = R)$
45	44	necon3d	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to (Q \neq R \to F \neq G)$
46	32 45	mpd	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to F \neq G$
47		simp2ll	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to f = s (F)$
48		simp2rl	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to f = s (G)$
49	47 48	eqtr3d	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to s (F) = s (G)$
50		simp11	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to (K \in HL \land W \in H)$
51		simp2rr	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to s \in E$
52		simp3	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to s \neq O$
53	50 35	syl	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
54		simp12l	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
55	2 4 5 7 13	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F \in T$
56	50 53 54 55	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to F \in T$
57		simp12r	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
58	2 4 5 7 14	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to G \in T$
59	50 53 57 58	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to G \in T$
60	1 5 7 8 9	tendospcanN	$⊢ ((K \in HL \land W \in H) \land (s \in E \land s \neq O) \land (F \in T \land G \in T)) \to (s (F) = s (G) \leftrightarrow F = G)$
61	50 51 52 56 59 60	syl122anc	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to (s (F) = s (G) \leftrightarrow F = G)$
62	49 61	mpbid	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \land s \neq O) \to F = G$
63	62	3expia	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to (s \neq O \to F = G)$
64	63	necon1d	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to (F \neq G \to s = O)$
65	46 64	mpd	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to s = O$
66	65	fveq1d	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to s (F) = O (F)$
67	34 36 37 55	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to F \in T$
68	9 1	tendo02	$⊢ F \in T \to O (F) = {I ↾}_{B}$
69	67 68	syl	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to O (F) = {I ↾}_{B}$
70	31 66 69	3eqtrd	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to f = {I ↾}_{B}$
71	70 65	jca	$⊢ (((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \land ((f = s (F) \land s \in E) \land (f = s (G) \land s \in E))) \to (f = {I ↾}_{B} \land s = O)$
72	71	ex	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to (((f = s (F) \land s \in E) \land (f = s (G) \land s \in E)) \to (f = {I ↾}_{B} \land s = O))$
73	30 72	sylbid	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to (⟨f, s⟩ \in (I (Q) \cap I (R)) \to (f = {I ↾}_{B} \land s = O))$
74		opex	$⊢ ⟨f, s⟩ \in V$
75	74	elsn	$⊢ ⟨f, s⟩ \in \{⟨{I ↾}_{B}, O⟩\} \leftrightarrow ⟨f, s⟩ = ⟨{I ↾}_{B}, O⟩$
76	22 23	opth	$⊢ ⟨f, s⟩ = ⟨{I ↾}_{B}, O⟩ \leftrightarrow (f = {I ↾}_{B} \land s = O)$
77	75 76	bitr2i	$⊢ (f = {I ↾}_{B} \land s = O) \leftrightarrow ⟨f, s⟩ \in \{⟨{I ↾}_{B}, O⟩\}$
78	1 5 7 11 12 9	dvh0g	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} = ⟨{I ↾}_{B}, O⟩$
79	78	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to \underset{˙}{0} = ⟨{I ↾}_{B}, O⟩$
80	79	sneqd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to \{\underset{˙}{0}\} = \{⟨{I ↾}_{B}, O⟩\}$
81	80	eleq2d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to (⟨f, s⟩ \in \{\underset{˙}{0}\} \leftrightarrow ⟨f, s⟩ \in \{⟨{I ↾}_{B}, O⟩\})$
82	77 81	bitr4id	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to ((f = {I ↾}_{B} \land s = O) \leftrightarrow ⟨f, s⟩ \in \{\underset{˙}{0}\})$
83	73 82	sylibd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to (⟨f, s⟩ \in (I (Q) \cap I (R)) \to ⟨f, s⟩ \in \{\underset{˙}{0}\})$
84	18 83	relssdv	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to I (Q) \cap I (R) \subseteq \{\underset{˙}{0}\}$
85	5 11 20	dvhlmod	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to U \in LMod$
86		simp2ll	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to Q \in A$
87	1 4	atbase	$⊢ Q \in A \to Q \in B$
88	86 87	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to Q \in B$
89		eqid	$⊢ LSubSp (U) = LSubSp (U)$
90	1 5 10 11 89	dihlss	$⊢ ((K \in HL \land W \in H) \land Q \in B) \to I (Q) \in LSubSp (U)$
91	20 88 90	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to I (Q) \in LSubSp (U)$
92		simp2rl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to R \in A$
93	1 4	atbase	$⊢ R \in A \to R \in B$
94	92 93	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to R \in B$
95	1 5 10 11 89	dihlss	$⊢ ((K \in HL \land W \in H) \land R \in B) \to I (R) \in LSubSp (U)$
96	20 94 95	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to I (R) \in LSubSp (U)$
97	89	lssincl	$⊢ (U \in LMod \land I (Q) \in LSubSp (U) \land I (R) \in LSubSp (U)) \to I (Q) \cap I (R) \in LSubSp (U)$
98	85 91 96 97	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to I (Q) \cap I (R) \in LSubSp (U)$
99	12 89	lss0ss	$⊢ (U \in LMod \land I (Q) \cap I (R) \in LSubSp (U)) \to \{\underset{˙}{0}\} \subseteq I (Q) \cap I (R)$
100	85 98 99	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to \{\underset{˙}{0}\} \subseteq I (Q) \cap I (R)$
101	84 100	eqssd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land Q \neq R) \to I (Q) \cap I (R) = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem dihmeetlem13N

Proof