Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihjat1 Structured version   Unicode version

Theorem dihjat1 32325
 Description: Subspace sum of a closed subspace and an atom. (pmapjat1 30748 analog.) (Contributed by NM, 1-Oct-2014.)
Hypotheses
Ref Expression
dihjat1.h
dihjat1.u
dihjat1.v
dihjat1.p
dihjat1.n
dihjat1.i
dihjat1.j joinH
dihjat1.k
dihjat1.x
dihjat1.q
Assertion
Ref Expression
dihjat1

Proof of Theorem dihjat1
StepHypRef Expression
1 sneq 3849 . . . . . 6
21fveq2d 5761 . . . . 5
3 dihjat1.h . . . . . . 7
4 dihjat1.u . . . . . . 7
5 dihjat1.k . . . . . . 7
63, 4, 5dvhlmod 32006 . . . . . 6
7 eqid 2442 . . . . . . 7
8 dihjat1.n . . . . . . 7
97, 8lspsn0 16115 . . . . . 6
106, 9syl 16 . . . . 5
112, 10sylan9eqr 2496 . . . 4
1211oveq2d 6126 . . 3
13 dihjat1.i . . . . 5
14 dihjat1.j . . . . 5 joinH
15 dihjat1.x . . . . 5
163, 4, 7, 13, 14, 5, 15djh01 32308 . . . 4
1811oveq2d 6126 . . . 4
19 eqid 2442 . . . . . . . . 9
203, 4, 13, 19dihrnlss 32173 . . . . . . . 8
215, 15, 20syl2anc 644 . . . . . . 7
2219lsssubg 16064 . . . . . . 7 SubGrp
236, 21, 22syl2anc 644 . . . . . 6 SubGrp
24 dihjat1.p . . . . . . 7
257, 24lsm01 15334 . . . . . 6 SubGrp
2623, 25syl 16 . . . . 5
2726adantr 453 . . . 4
2818, 27eqtr2d 2475 . . 3
2912, 17, 283eqtrd 2478 . 2
30 dihjat1.v . . 3