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

Theorem dihjat1lem 32227
 Description: Subspace sum of a closed subspace and an atom. (pmapjat1 30651 analog.) TODO: merge into dihjat1 32228? (Contributed by NM, 18-Aug-2014.)
Hypotheses
Ref Expression
dihjat1.h
dihjat1.u
dihjat1.v
dihjat1.p
dihjat1.n
dihjat1.i
dihjat1.j joinH
dihjat1.k
dihjat1.x
dihjat1.o
dihjat1lem.q
Assertion
Ref Expression
dihjat1lem

Proof of Theorem dihjat1lem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 449 . . . 4
21oveq1d 6097 . . 3
31oveq1d 6097 . . . 4
4 dihjat1.h . . . . . . 7
5 dihjat1.u . . . . . . 7
6 dihjat1.o . . . . . . 7
7 dihjat1.i . . . . . . 7
8 dihjat1.j . . . . . . 7 joinH
9 dihjat1.k . . . . . . 7
10 dihjat1lem.q . . . . . . . . 9
11 eldifi 3470 . . . . . . . . 9
1210, 11syl 16 . . . . . . . 8
13 dihjat1.v . . . . . . . . 9
14 dihjat1.n . . . . . . . . 9
154, 5, 13, 14, 7dihlsprn 32130 . . . . . . . 8
169, 12, 15syl2anc 644 . . . . . . 7
174, 5, 6, 7, 8, 9, 16djh02 32212 . . . . . 6
184, 5, 9dvhlmod 31909 . . . . . . . 8
19 eqid 2437 . . . . . . . . . 10
2013, 19, 14lspsncl 16054 . . . . . . . . 9
2118, 12, 20syl2anc 644 . . . . . . . 8
2219lsssubg 16034 . . . . . . . 8 SubGrp
2318, 21, 22syl2anc 644 . . . . . . 7 SubGrp
24 dihjat1.p . . . . . . . 8
256, 24lsm02 15305 . . . . . . 7 SubGrp
2623, 25syl 16 . . . . . 6
2717, 26eqtr4d 2472 . . . . 5
2827adantr 453 . . . 4
293, 28eqtr4d 2472 . . 3
302, 29eqtr4d 2472 . 2
3118adantr 453 . . . 4
32 dihjat1.x . . . . . . . 8
334, 5, 7, 13dihrnss 32077 . . . . . . . 8
349, 32, 33syl2anc 644 . . . . . . 7
3513, 19lssss 16014 . . . . . . . 8
3621, 35syl 16 . . . . . . 7
374, 7, 5, 13, 8djhcl 32199 . . . . . . 7
389, 34, 36, 37syl12anc 1183 . . . . . 6
394, 5, 7, 13dihrnss 32077 . . . . . 6
409, 38, 39syl2anc 644 . . . . 5
4140adantr 453 . . . 4
424, 5, 7, 19dihrnlss 32076 . . . . . . 7
439, 32, 42syl2anc 644 . . . . . 6
4419, 24lsmcl 16156 . . . . . 6
4518, 43, 21, 44syl3anc 1185 . . . . 5
4645adantr 453 . . . 4
47 simplr 733 . . . . . . . 8
489ad2antrr 708 . . . . . . . . 9
4932ad2antrr 708 . . . . . . . . 9
50 simpr 449 . . . . . . . . 9
5110ad2antrr 708 . . . . . . . . 9
524, 5, 13, 6, 14, 7, 8, 48, 49, 50, 51djhcvat42 32214 . . . . . . . 8
5347, 52mpand 658 . . . . . . 7
54 simprrl 742 . . . . . . . . . . 11
5518ad3antrrr 712 . . . . . . . . . . . 12
5643ad3antrrr 712 . . . . . . . . . . . 12
57 eldifi 3470 . . . . . . . . . . . . 13
5857ad2antrl 710 . . . . . . . . . . . 12
5913, 19, 14, 55, 56, 58lspsnel5 16072 . . . . . . . . . . 11
6054, 59mpbird 225 . . . . . . . . . 10
6112ad3antrrr 712 . . . . . . . . . . . 12
6213, 14lspsnid 16070 . . . . . . . . . . . 12
6355, 61, 62syl2anc 644 . . . . . . . . . . 11
64 simprrr 743 . . . . . . . . . . 11
65 sneq 3826 . . . . . . . . . . . . . . 15
6665fveq2d 5733 . . . . . . . . . . . . . 14
6766oveq2d 6098 . . . . . . . . . . . . 13
6867sseq2d 3377 . . . . . . . . . . . 12
6968rspcev 3053 . . . . . . . . . . 11
7063, 64, 69syl2anc 644 . . . . . . . . . 10
7160, 70jca 520 . . . . . . . . 9
7271ex 425 . . . . . . . 8
7372reximdv2 2816 . . . . . . 7
7453, 73syld 43 . . . . . 6
7574anim2d 550 . . . . 5
764, 5, 7, 19dihrnlss 32076 . . . . . . . 8
779, 38, 76syl2anc 644 . . . . . . 7
7813, 19, 14, 18, 77lspsnel6 16071 . . . . . 6
7978ad2antrr 708 . . . . 5
8013, 19, 24, 14, 18, 43, 21lsmelval2 16158 . . . . . . 7
819ad2antrr 708 . . . . . . . . . . . 12
8243ad2antrr 708 . . . . . . . . . . . . 13
83 simplr 733 . . . . . . . . . . . . 13
8413, 19lssel 16015 . . . . . . . . . . . . 13
8582, 83, 84syl2anc 644 . . . . . . . . . . . 12
8621ad2antrr 708 . . . . . . . . . . . . 13
87 simpr 449 . . . . . . . . . . . . 13
8813, 19lssel 16015 . . . . . . . . . . . . 13
8986, 87, 88syl2anc 644 . . . . . . . . . . . 12
904, 5, 13, 24, 14, 7, 8, 81, 85, 89djhlsmat 32226 . . . . . . . . . . 11
9190sseq2d 3377 . . . . . . . . . 10
9291rexbidva 2723 . . . . . . . . 9
9392rexbidva 2723 . . . . . . . 8
9493anbi2d 686 . . . . . . 7
9580, 94bitrd 246 . . . . . 6
9695ad2antrr 708 . . . . 5
9775, 79, 963imtr4d 261 . . . 4
9813, 6, 19, 31, 41, 46, 97lssssr 16030 . . 3
994, 5, 13, 24, 8, 9, 34, 36djhsumss 32206 . . . 4