dochexmidlem6

	Ref	Expression
Hypotheses	dochexmidlem1.h	$⊢ H = LHyp (K)$
	dochexmidlem1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochexmidlem1.u	$⊢ U = DVecH (K) (W)$
	dochexmidlem1.v	$⊢ V = {Base}_{U}$
	dochexmidlem1.s	$⊢ S = LSubSp (U)$
	dochexmidlem1.n	$⊢ N = LSpan (U)$
	dochexmidlem1.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dochexmidlem1.a	$⊢ A = LSAtoms (U)$
	dochexmidlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
	dochexmidlem1.x	$⊢ φ \to X \in S$
	dochexmidlem6.pp	$⊢ φ \to p \in A$
	dochexmidlem6.z	$⊢ \underset{˙}{0} = 0_{U}$
	dochexmidlem6.m	$⊢ M = X \underset{˙}{\oplus} p$
	dochexmidlem6.xn	$⊢ φ \to X \neq \{\underset{˙}{0}\}$
	dochexmidlem6.c	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
	dochexmidlem6.pl	$⊢ φ \to \neg p \subseteq X \underset{˙}{\oplus} \underset{˙}{⊥} (X)$
Assertion	dochexmidlem6	$⊢ φ \to M = X$

Proof

Step	Hyp	Ref	Expression
1		dochexmidlem1.h	$⊢ H = LHyp (K)$
2		dochexmidlem1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochexmidlem1.u	$⊢ U = DVecH (K) (W)$
4		dochexmidlem1.v	$⊢ V = {Base}_{U}$
5		dochexmidlem1.s	$⊢ S = LSubSp (U)$
6		dochexmidlem1.n	$⊢ N = LSpan (U)$
7		dochexmidlem1.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
8		dochexmidlem1.a	$⊢ A = LSAtoms (U)$
9		dochexmidlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
10		dochexmidlem1.x	$⊢ φ \to X \in S$
11		dochexmidlem6.pp	$⊢ φ \to p \in A$
12		dochexmidlem6.z	$⊢ \underset{˙}{0} = 0_{U}$
13		dochexmidlem6.m	$⊢ M = X \underset{˙}{\oplus} p$
14		dochexmidlem6.xn	$⊢ φ \to X \neq \{\underset{˙}{0}\}$
15		dochexmidlem6.c	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
16		dochexmidlem6.pl	$⊢ φ \to \neg p \subseteq X \underset{˙}{\oplus} \underset{˙}{⊥} (X)$
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14 16	dochexmidlem5	$⊢ φ \to \underset{˙}{⊥} (X) \cap M = \{\underset{˙}{0}\}$
18	17	fveq2d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap M) = \underset{˙}{⊥} (\{\underset{˙}{0}\})$
19	1 3 2 4 12	doch0	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} (\{\underset{˙}{0}\}) = V$
20	9 19	syl	$⊢ φ \to \underset{˙}{⊥} (\{\underset{˙}{0}\}) = V$
21	18 20	eqtrd	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap M) = V$
22	21	ineq1d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap M) \cap M = V \cap M$
23		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
24	4 5	lssss	$⊢ X \in S \to X \subseteq V$
25	10 24	syl	$⊢ φ \to X \subseteq V$
26	1 3 4 2	dochssv	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \subseteq V$
27	9 25 26	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) \subseteq V$
28	1 23 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)$
29	9 27 28	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)$
30	15 29	eqeltrrd	$⊢ φ \to X \in ran DIsoH (K) (W)$
31	1 23 3 7 8 9 30 11	dihsmatrn	$⊢ φ \to X \underset{˙}{\oplus} p \in ran DIsoH (K) (W)$
32	13 31	eqeltrid	$⊢ φ \to M \in ran DIsoH (K) (W)$
33	1 3 23 5	dihrnlss	$⊢ ((K \in HL \land W \in H) \land M \in ran DIsoH (K) (W)) \to M \in S$
34	9 32 33	syl2anc	$⊢ φ \to M \in S$
35	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
36	5 8 35 11	lsatlssel	$⊢ φ \to p \in S$
37	5 7	lsmcl	$⊢ (U \in LMod \land X \in S \land p \in S) \to X \underset{˙}{\oplus} p \in S$
38	35 10 36 37	syl3anc	$⊢ φ \to X \underset{˙}{\oplus} p \in S$
39	4 5	lssss	$⊢ X \underset{˙}{\oplus} p \in S \to X \underset{˙}{\oplus} p \subseteq V$
40	38 39	syl	$⊢ φ \to X \underset{˙}{\oplus} p \subseteq V$
41	13 40	eqsstrid	$⊢ φ \to M \subseteq V$
42	1 23 3 4 2 9 41	dochoccl	$⊢ φ \to (M \in ran DIsoH (K) (W) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (M)) = M)$
43	32 42	mpbid	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (M)) = M$
44	5	lsssssubg	$⊢ U \in LMod \to S \subseteq SubGrp (U)$
45	35 44	syl	$⊢ φ \to S \subseteq SubGrp (U)$
46	45 10	sseldd	$⊢ φ \to X \in SubGrp (U)$
47	45 36	sseldd	$⊢ φ \to p \in SubGrp (U)$
48	7	lsmub1	$⊢ (X \in SubGrp (U) \land p \in SubGrp (U)) \to X \subseteq X \underset{˙}{\oplus} p$
49	46 47 48	syl2anc	$⊢ φ \to X \subseteq X \underset{˙}{\oplus} p$
50	49 13	sseqtrrdi	$⊢ φ \to X \subseteq M$
51	1 3 5 2 9 10 34 43 50	dihoml4	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap M) \cap M = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
52		sseqin2	$⊢ M \subseteq V \leftrightarrow V \cap M = M$
53	41 52	sylib	$⊢ φ \to V \cap M = M$
54	22 51 53	3eqtr3rd	$⊢ φ \to M = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
55	54 15	eqtrd	$⊢ φ \to M = X$

Metamath Proof Explorer

Theorem dochexmidlem6

Proof