dihjat1

Description: Subspace sum of a closed subspace and an atom. ( pmapjat1 analog.) (Contributed by NM, 1-Oct-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.q	$⊢ φ \to T \in V$
Assertion	dihjat1	$⊢ φ \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.q	$⊢ φ \to T \in V$
11		sneq	$⊢ T = 0_{U} \to \{T\} = \{0_{U}\}$
12	11	fveq2d	$⊢ T = 0_{U} \to N (\{T\}) = N (\{0_{U}\})$
13	1 2 8	dvhlmod	$⊢ φ \to U \in LMod$
14		eqid	$⊢ 0_{U} = 0_{U}$
15	14 5	lspsn0	$⊢ U \in LMod \to N (\{0_{U}\}) = \{0_{U}\}$
16	13 15	syl	$⊢ φ \to N (\{0_{U}\}) = \{0_{U}\}$
17	12 16	sylan9eqr	$⊢ (φ \land T = 0_{U}) \to N (\{T\}) = \{0_{U}\}$
18	17	oveq2d	$⊢ (φ \land T = 0_{U}) \to X \underset{˙}{\lor} N (\{T\}) = X \underset{˙}{\lor} \{0_{U}\}$
19	1 2 14 6 7 8 9	djh01	$⊢ φ \to X \underset{˙}{\lor} \{0_{U}\} = X$
20	19	adantr	$⊢ (φ \land T = 0_{U}) \to X \underset{˙}{\lor} \{0_{U}\} = X$
21	17	oveq2d	$⊢ (φ \land T = 0_{U}) \to X \underset{˙}{\oplus} N (\{T\}) = X \underset{˙}{\oplus} \{0_{U}\}$
22		eqid	$⊢ LSubSp (U) = LSubSp (U)$
23	1 2 6 22	dihrnlss	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to X \in LSubSp (U)$
24	8 9 23	syl2anc	$⊢ φ \to X \in LSubSp (U)$
25	22	lsssubg	$⊢ (U \in LMod \land X \in LSubSp (U)) \to X \in SubGrp (U)$
26	13 24 25	syl2anc	$⊢ φ \to X \in SubGrp (U)$
27	14 4	lsm01	$⊢ X \in SubGrp (U) \to X \underset{˙}{\oplus} \{0_{U}\} = X$
28	26 27	syl	$⊢ φ \to X \underset{˙}{\oplus} \{0_{U}\} = X$
29	28	adantr	$⊢ (φ \land T = 0_{U}) \to X \underset{˙}{\oplus} \{0_{U}\} = X$
30	21 29	eqtr2d	$⊢ (φ \land T = 0_{U}) \to X = X \underset{˙}{\oplus} N (\{T\})$
31	18 20 30	3eqtrd	$⊢ (φ \land T = 0_{U}) \to X \underset{˙}{\lor} N (\{T\}) = X \underset{˙}{\oplus} N (\{T\})$
32	8	adantr	$⊢ (φ \land T \neq 0_{U}) \to (K \in HL \land W \in H)$
33	9	adantr	$⊢ (φ \land T \neq 0_{U}) \to X \in ran I$
34	10	anim1i	$⊢ (φ \land T \neq 0_{U}) \to (T \in V \land T \neq 0_{U})$
35		eldifsn	$⊢ T \in (V ∖ \{0_{U}\}) \leftrightarrow (T \in V \land T \neq 0_{U})$
36	34 35	sylibr	$⊢ (φ \land T \neq 0_{U}) \to T \in (V ∖ \{0_{U}\})$
37	1 2 3 4 5 6 7 32 33 14 36	dihjat1lem	$⊢ (φ \land T \neq 0_{U}) \to X \underset{˙}{\lor} N (\{T\}) = X \underset{˙}{\oplus} N (\{T\})$
38	31 37	pm2.61dane	$⊢ φ \to X \underset{˙}{\lor} N (\{T\}) = X \underset{˙}{\oplus} N (\{T\})$

Metamath Proof Explorer

Theorem dihjat1

Proof