Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ocvpj Structured version   Unicode version

Theorem ocvpj 18617
 Description: The orthocomplement of a projection subspace is a projection subspace. (Contributed by Mario Carneiro, 16-Oct-2015.)
Hypotheses
Ref Expression
ocvpj.k
ocvpj.o
Assertion
Ref Expression
ocvpj

Proof of Theorem ocvpj
StepHypRef Expression
1 ocvpj.k . . . . . 6
2 eqid 2467 . . . . . 6
31, 2pjcss 18616 . . . . 5
43sselda 3509 . . . 4
5 eqid 2467 . . . . 5
65, 2cssss 18585 . . . 4
74, 6syl 16 . . 3
8 ocvpj.o . . . 4
9 eqid 2467 . . . 4
105, 8, 9ocvlss 18572 . . 3
117, 10syldan 470 . 2
12 phllmod 18534 . . . . . 6
1312adantr 465 . . . . 5
14 lmodabl 17428 . . . . 5
1513, 14syl 16 . . . 4
169lsssssubg 17475 . . . . . 6 SubGrp
1713, 16syl 16 . . . . 5 SubGrp
1817, 11sseldd 3510 . . . 4 SubGrp
192, 9csslss 18591 . . . . . 6
204, 19syldan 470 . . . . 5
2117, 20sseldd 3510 . . . 4 SubGrp
22 eqid 2467 . . . . 5
2322lsmcom 16737 . . . 4 SubGrp SubGrp
2415, 18, 21, 23syl3anc 1228 . . 3
258, 2cssi 18584 . . . . 5
264, 25syl 16 . . . 4
2726oveq2d 6311 . . 3
285, 9, 8, 22, 1pjdm2 18611 . . . 4
2928simplbda 624 . . 3
3024, 27, 293eqtr3d 2516 . 2
315, 9, 8, 22, 1pjdm2 18611 . . 3