Metamath Proof Explorer


Theorem 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 ˙ = LSSum U
dihjat1.n N = LSpan U
dihjat1.i I = DIsoH K W
dihjat1.j ˙ = joinH K W
dihjat1.k φ K HL W H
dihjat1.x φ X ran I
dihjat1.q φ T V
Assertion dihjat1 φ X ˙ N T = X ˙ 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 ˙ = LSSum U
5 dihjat1.n N = LSpan U
6 dihjat1.i I = DIsoH K W
7 dihjat1.j ˙ = joinH K W
8 dihjat1.k φ K HL W H
9 dihjat1.x φ X ran I
10 dihjat1.q φ T V
11 sneq T = 0 U T = 0 U
12 11 fveq2d T = 0 U N T = N 0 U
13 1 2 8 dvhlmod φ U LMod
14 eqid 0 U = 0 U
15 14 5 lspsn0 U LMod N 0 U = 0 U
16 13 15 syl φ N 0 U = 0 U
17 12 16 sylan9eqr φ T = 0 U N T = 0 U
18 17 oveq2d φ T = 0 U X ˙ N T = X ˙ 0 U
19 1 2 14 6 7 8 9 djh01 φ X ˙ 0 U = X
20 19 adantr φ T = 0 U X ˙ 0 U = X
21 17 oveq2d φ T = 0 U X ˙ N T = X ˙ 0 U
22 eqid LSubSp U = LSubSp U
23 1 2 6 22 dihrnlss K HL W H X ran I X LSubSp U
24 8 9 23 syl2anc φ X LSubSp U
25 22 lsssubg U LMod X LSubSp U X SubGrp U
26 13 24 25 syl2anc φ X SubGrp U
27 14 4 lsm01 X SubGrp U X ˙ 0 U = X
28 26 27 syl φ X ˙ 0 U = X
29 28 adantr φ T = 0 U X ˙ 0 U = X
30 21 29 eqtr2d φ T = 0 U X = X ˙ N T
31 18 20 30 3eqtrd φ T = 0 U X ˙ N T = X ˙ N T
32 8 adantr φ T 0 U K HL W H
33 9 adantr φ T 0 U X ran I
34 10 anim1i φ T 0 U T V T 0 U
35 eldifsn T V 0 U T V T 0 U
36 34 35 sylibr φ T 0 U T V 0 U
37 1 2 3 4 5 6 7 32 33 14 36 dihjat1lem φ T 0 U X ˙ N T = X ˙ N T
38 31 37 pm2.61dane φ X ˙ N T = X ˙ N T