dihjat1lem

Description: Subspace sum of a closed subspace and an atom. ( pmapjat1 analog.) TODO: merge into dihjat1 ? (Contributed by NM, 18-Aug-2014)

	Ref	Expression
Hypotheses	dihjat1.h	$⊢ H = LHyp (K)$
	dihjat1.u	$⊢ U = DVecH (K) (W)$
	dihjat1.v	$⊢ V = {Base}_{U}$
	dihjat1.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihjat1.n	$⊢ N = LSpan (U)$
	dihjat1.i	$⊢ I = DIsoH (K) (W)$
	dihjat1.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
	dihjat1.k	$⊢ φ \to (K \in HL \land W \in H)$
	dihjat1.x	$⊢ φ \to X \in ran I$
	dihjat1.o	$⊢ \underset{˙}{0} = 0_{U}$
	dihjat1lem.q	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
Assertion	dihjat1lem	$⊢ φ \to X \underset{˙}{\lor} N (\{T\}) = X \underset{˙}{\oplus} N (\{T\})$

Proof

Step	Hyp	Ref	Expression
1		dihjat1.h	$⊢ H = LHyp (K)$
2		dihjat1.u	$⊢ U = DVecH (K) (W)$
3		dihjat1.v	$⊢ V = {Base}_{U}$
4		dihjat1.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
5		dihjat1.n	$⊢ N = LSpan (U)$
6		dihjat1.i	$⊢ I = DIsoH (K) (W)$
7		dihjat1.j	$⊢ \underset{˙}{\lor} = joinH (K) (W)$
8		dihjat1.k	$⊢ φ \to (K \in HL \land W \in H)$
9		dihjat1.x	$⊢ φ \to X \in ran I$
10		dihjat1.o	$⊢ \underset{˙}{0} = 0_{U}$
11		dihjat1lem.q	$⊢ φ \to T \in (V ∖ \{\underset{˙}{0}\})$
12		simpr	$⊢ (φ \land X = \{\underset{˙}{0}\}) \to X = \{\underset{˙}{0}\}$
13	12	oveq1d	$⊢ (φ \land X = \{\underset{˙}{0}\}) \to X \underset{˙}{\lor} N (\{T\}) = \{\underset{˙}{0}\} \underset{˙}{\lor} N (\{T\})$
14	12	oveq1d	$⊢ (φ \land X = \{\underset{˙}{0}\}) \to X \underset{˙}{\oplus} N (\{T\}) = \{\underset{˙}{0}\} \underset{˙}{\oplus} N (\{T\})$
15		eldifi	$⊢ T \in (V ∖ \{\underset{˙}{0}\}) \to T \in V$
16	11 15	syl	$⊢ φ \to T \in V$
17	1 2 3 5 6	dihlsprn	$⊢ ((K \in HL \land W \in H) \land T \in V) \to N (\{T\}) \in ran I$
18	8 16 17	syl2anc	$⊢ φ \to N (\{T\}) \in ran I$
19	1 2 10 6 7 8 18	djh02	$⊢ φ \to \{\underset{˙}{0}\} \underset{˙}{\lor} N (\{T\}) = N (\{T\})$
20	1 2 8	dvhlmod	$⊢ φ \to U \in LMod$
21		eqid	$⊢ LSubSp (U) = LSubSp (U)$
22	3 21 5	lspsncl	$⊢ (U \in LMod \land T \in V) \to N (\{T\}) \in LSubSp (U)$
23	20 16 22	syl2anc	$⊢ φ \to N (\{T\}) \in LSubSp (U)$
24	21	lsssubg	$⊢ (U \in LMod \land N (\{T\}) \in LSubSp (U)) \to N (\{T\}) \in SubGrp (U)$
25	20 23 24	syl2anc	$⊢ φ \to N (\{T\}) \in SubGrp (U)$
26	10 4	lsm02	$⊢ N (\{T\}) \in SubGrp (U) \to \{\underset{˙}{0}\} \underset{˙}{\oplus} N (\{T\}) = N (\{T\})$
27	25 26	syl	$⊢ φ \to \{\underset{˙}{0}\} \underset{˙}{\oplus} N (\{T\}) = N (\{T\})$
28	19 27	eqtr4d	$⊢ φ \to \{\underset{˙}{0}\} \underset{˙}{\lor} N (\{T\}) = \{\underset{˙}{0}\} \underset{˙}{\oplus} N (\{T\})$
29	28	adantr	$⊢ (φ \land X = \{\underset{˙}{0}\}) \to \{\underset{˙}{0}\} \underset{˙}{\lor} N (\{T\}) = \{\underset{˙}{0}\} \underset{˙}{\oplus} N (\{T\})$
30	14 29	eqtr4d	$⊢ (φ \land X = \{\underset{˙}{0}\}) \to X \underset{˙}{\oplus} N (\{T\}) = \{\underset{˙}{0}\} \underset{˙}{\lor} N (\{T\})$
31	13 30	eqtr4d	$⊢ (φ \land X = \{\underset{˙}{0}\}) \to X \underset{˙}{\lor} N (\{T\}) = X \underset{˙}{\oplus} N (\{T\})$
32	20	adantr	$⊢ (φ \land X \neq \{\underset{˙}{0}\}) \to U \in LMod$
33	1 2 6 3	dihrnss	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to X \subseteq V$
34	8 9 33	syl2anc	$⊢ φ \to X \subseteq V$
35	3 21	lssss	$⊢ N (\{T\}) \in LSubSp (U) \to N (\{T\}) \subseteq V$
36	23 35	syl	$⊢ φ \to N (\{T\}) \subseteq V$
37	1 6 2 3 7	djhcl	$⊢ ((K \in HL \land W \in H) \land (X \subseteq V \land N (\{T\}) \subseteq V)) \to X \underset{˙}{\lor} N (\{T\}) \in ran I$
38	8 34 36 37	syl12anc	$⊢ φ \to X \underset{˙}{\lor} N (\{T\}) \in ran I$
39	1 2 6 3	dihrnss	$⊢ ((K \in HL \land W \in H) \land X \underset{˙}{\lor} N (\{T\}) \in ran I) \to X \underset{˙}{\lor} N (\{T\}) \subseteq V$
40	8 38 39	syl2anc	$⊢ φ \to X \underset{˙}{\lor} N (\{T\}) \subseteq V$
41	40	adantr	$⊢ (φ \land X \neq \{\underset{˙}{0}\}) \to X \underset{˙}{\lor} N (\{T\}) \subseteq V$
42	1 2 6 21	dihrnlss	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to X \in LSubSp (U)$
43	8 9 42	syl2anc	$⊢ φ \to X \in LSubSp (U)$
44	21 4	lsmcl	$⊢ (U \in LMod \land X \in LSubSp (U) \land N (\{T\}) \in LSubSp (U)) \to X \underset{˙}{\oplus} N (\{T\}) \in LSubSp (U)$
45	20 43 23 44	syl3anc	$⊢ φ \to X \underset{˙}{\oplus} N (\{T\}) \in LSubSp (U)$
46	45	adantr	$⊢ (φ \land X \neq \{\underset{˙}{0}\}) \to X \underset{˙}{\oplus} N (\{T\}) \in LSubSp (U)$
47		simplr	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to X \neq \{\underset{˙}{0}\}$
48	8	ad2antrr	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to (K \in HL \land W \in H)$
49	9	ad2antrr	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to X \in ran I$
50		simpr	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to x \in (V ∖ \{\underset{˙}{0}\})$
51	11	ad2antrr	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to T \in (V ∖ \{\underset{˙}{0}\})$
52	1 2 3 10 5 6 7 48 49 50 51	djhcvat42	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to ((X \neq \{\underset{˙}{0}\} \land N (\{x\}) \subseteq X \underset{˙}{\lor} N (\{T\})) \to \exists y \in (V ∖ \{\underset{˙}{0}\}) (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))$
53	47 52	mpand	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to (N (\{x\}) \subseteq X \underset{˙}{\lor} N (\{T\}) \to \exists y \in (V ∖ \{\underset{˙}{0}\}) (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))$
54		simprrl	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to N (\{y\}) \subseteq X$
55	20	ad3antrrr	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to U \in LMod$
56	43	ad3antrrr	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to X \in LSubSp (U)$
57		eldifi	$⊢ y \in (V ∖ \{\underset{˙}{0}\}) \to y \in V$
58	57	ad2antrl	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to y \in V$
59	3 21 5 55 56 58	lspsnel5	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to (y \in X \leftrightarrow N (\{y\}) \subseteq X)$
60	54 59	mpbird	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to y \in X$
61	16	ad3antrrr	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to T \in V$
62	3 5	lspsnid	$⊢ (U \in LMod \land T \in V) \to T \in N (\{T\})$
63	55 61 62	syl2anc	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to T \in N (\{T\})$
64		simprrr	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})$
65		sneq	$⊢ z = T \to \{z\} = \{T\}$
66	65	fveq2d	$⊢ z = T \to N (\{z\}) = N (\{T\})$
67	66	oveq2d	$⊢ z = T \to N (\{y\}) \underset{˙}{\lor} N (\{z\}) = N (\{y\}) \underset{˙}{\lor} N (\{T\})$
68	67	sseq2d	$⊢ z = T \to (N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\}) \leftrightarrow N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\}))$
69	68	rspcev	$⊢ (T \in N (\{T\}) \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})) \to \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\})$
70	63 64 69	syl2anc	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\})$
71	60 70	jca	$⊢ (((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \land (y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})))) \to (y \in X \land \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\}))$
72	71	ex	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to ((y \in (V ∖ \{\underset{˙}{0}\}) \land (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\}))) \to (y \in X \land \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\})))$
73	72	reximdv2	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to (\exists y \in (V ∖ \{\underset{˙}{0}\}) (N (\{y\}) \subseteq X \land N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{T\})) \to \exists y \in X \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\}))$
74	53 73	syld	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to (N (\{x\}) \subseteq X \underset{˙}{\lor} N (\{T\}) \to \exists y \in X \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\}))$
75	74	anim2d	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to ((x \in V \land N (\{x\}) \subseteq X \underset{˙}{\lor} N (\{T\})) \to (x \in V \land \exists y \in X \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\})))$
76	1 2 6 21	dihrnlss	$⊢ ((K \in HL \land W \in H) \land X \underset{˙}{\lor} N (\{T\}) \in ran I) \to X \underset{˙}{\lor} N (\{T\}) \in LSubSp (U)$
77	8 38 76	syl2anc	$⊢ φ \to X \underset{˙}{\lor} N (\{T\}) \in LSubSp (U)$
78	3 21 5 20 77	lspsnel6	$⊢ φ \to (x \in (X \underset{˙}{\lor} N (\{T\})) \leftrightarrow (x \in V \land N (\{x\}) \subseteq X \underset{˙}{\lor} N (\{T\})))$
79	78	ad2antrr	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to (x \in (X \underset{˙}{\lor} N (\{T\})) \leftrightarrow (x \in V \land N (\{x\}) \subseteq X \underset{˙}{\lor} N (\{T\})))$
80	3 21 4 5 20 43 23	lsmelval2	$⊢ φ \to (x \in (X \underset{˙}{\oplus} N (\{T\})) \leftrightarrow (x \in V \land \exists y \in X \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})))$
81	8	ad2antrr	$⊢ ((φ \land y \in X) \land z \in N (\{T\})) \to (K \in HL \land W \in H)$
82	43	ad2antrr	$⊢ ((φ \land y \in X) \land z \in N (\{T\})) \to X \in LSubSp (U)$
83		simplr	$⊢ ((φ \land y \in X) \land z \in N (\{T\})) \to y \in X$
84	3 21	lssel	$⊢ (X \in LSubSp (U) \land y \in X) \to y \in V$
85	82 83 84	syl2anc	$⊢ ((φ \land y \in X) \land z \in N (\{T\})) \to y \in V$
86	23	ad2antrr	$⊢ ((φ \land y \in X) \land z \in N (\{T\})) \to N (\{T\}) \in LSubSp (U)$
87		simpr	$⊢ ((φ \land y \in X) \land z \in N (\{T\})) \to z \in N (\{T\})$
88	3 21	lssel	$⊢ (N (\{T\}) \in LSubSp (U) \land z \in N (\{T\})) \to z \in V$
89	86 87 88	syl2anc	$⊢ ((φ \land y \in X) \land z \in N (\{T\})) \to z \in V$
90	1 2 3 4 5 6 7 81 85 89	djhlsmat	$⊢ ((φ \land y \in X) \land z \in N (\{T\})) \to N (\{y\}) \underset{˙}{\oplus} N (\{z\}) = N (\{y\}) \underset{˙}{\lor} N (\{z\})$
91	90	sseq2d	$⊢ ((φ \land y \in X) \land z \in N (\{T\})) \to (N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\}) \leftrightarrow N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\}))$
92	91	rexbidva	$⊢ (φ \land y \in X) \to (\exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\}) \leftrightarrow \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\}))$
93	92	rexbidva	$⊢ φ \to (\exists y \in X \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\}) \leftrightarrow \exists y \in X \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\}))$
94	93	anbi2d	$⊢ φ \to ((x \in V \land \exists y \in X \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\oplus} N (\{z\})) \leftrightarrow (x \in V \land \exists y \in X \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\})))$
95	80 94	bitrd	$⊢ φ \to (x \in (X \underset{˙}{\oplus} N (\{T\})) \leftrightarrow (x \in V \land \exists y \in X \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\})))$
96	95	ad2antrr	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to (x \in (X \underset{˙}{\oplus} N (\{T\})) \leftrightarrow (x \in V \land \exists y \in X \exists z \in N (\{T\}) N (\{x\}) \subseteq N (\{y\}) \underset{˙}{\lor} N (\{z\})))$
97	75 79 96	3imtr4d	$⊢ ((φ \land X \neq \{\underset{˙}{0}\}) \land x \in (V ∖ \{\underset{˙}{0}\})) \to (x \in (X \underset{˙}{\lor} N (\{T\})) \to x \in (X \underset{˙}{\oplus} N (\{T\})))$
98	10 21 32 41 46 97	lssssr	$⊢ (φ \land X \neq \{\underset{˙}{0}\}) \to X \underset{˙}{\lor} N (\{T\}) \subseteq X \underset{˙}{\oplus} N (\{T\})$
99	1 2 3 4 7 8 34 36	djhsumss	$⊢ φ \to X \underset{˙}{\oplus} N (\{T\}) \subseteq X \underset{˙}{\lor} N (\{T\})$
100	99	adantr	$⊢ (φ \land X \neq \{\underset{˙}{0}\}) \to X \underset{˙}{\oplus} N (\{T\}) \subseteq X \underset{˙}{\lor} N (\{T\})$
101	98 100	eqssd	$⊢ (φ \land X \neq \{\underset{˙}{0}\}) \to X \underset{˙}{\lor} N (\{T\}) = X \underset{˙}{\oplus} N (\{T\})$
102	31 101	pm2.61dane	$⊢ φ \to X \underset{˙}{\lor} N (\{T\}) = X \underset{˙}{\oplus} N (\{T\})$

Metamath Proof Explorer

Theorem dihjat1lem

Proof