Metamath Proof Explorer


Theorem paddclN

Description: The projective sum of two subspaces is a subspace. Part of Lemma 16.2 of MaedaMaeda p. 68. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses paddidm.s S=PSubSpK
paddidm.p +˙=+𝑃K
Assertion paddclN KHLXSYSX+˙YS

Proof

Step Hyp Ref Expression
1 paddidm.s S=PSubSpK
2 paddidm.p +˙=+𝑃K
3 simp1 KHLXSYSKHL
4 eqid AtomsK=AtomsK
5 4 1 psubssat KHLXSXAtomsK
6 5 3adant3 KHLXSYSXAtomsK
7 4 1 psubssat KHLYSYAtomsK
8 7 3adant2 KHLXSYSYAtomsK
9 4 2 paddssat KHLXAtomsKYAtomsKX+˙YAtomsK
10 3 6 8 9 syl3anc KHLXSYSX+˙YAtomsK
11 olc pAtomsKqX+˙YrX+˙YpKqjoinKrpX+˙YpX+˙YpAtomsKqX+˙YrX+˙YpKqjoinKr
12 eqid K=K
13 eqid joinK=joinK
14 12 13 4 2 elpadd KHLX+˙YAtomsKX+˙YAtomsKpX+˙Y+˙X+˙YpX+˙YpX+˙YpAtomsKqX+˙YrX+˙YpKqjoinKr
15 3 10 10 14 syl3anc KHLXSYSpX+˙Y+˙X+˙YpX+˙YpX+˙YpAtomsKqX+˙YrX+˙YpKqjoinKr
16 4 2 padd4N KHLXAtomsKYAtomsKXAtomsKYAtomsKX+˙Y+˙X+˙Y=X+˙X+˙Y+˙Y
17 3 6 8 6 8 16 syl122anc KHLXSYSX+˙Y+˙X+˙Y=X+˙X+˙Y+˙Y
18 1 2 paddidm KHLXSX+˙X=X
19 18 3adant3 KHLXSYSX+˙X=X
20 1 2 paddidm KHLYSY+˙Y=Y
21 20 3adant2 KHLXSYSY+˙Y=Y
22 19 21 oveq12d KHLXSYSX+˙X+˙Y+˙Y=X+˙Y
23 17 22 eqtrd KHLXSYSX+˙Y+˙X+˙Y=X+˙Y
24 23 eleq2d KHLXSYSpX+˙Y+˙X+˙YpX+˙Y
25 15 24 bitr3d KHLXSYSpX+˙YpX+˙YpAtomsKqX+˙YrX+˙YpKqjoinKrpX+˙Y
26 11 25 syl5ib KHLXSYSpAtomsKqX+˙YrX+˙YpKqjoinKrpX+˙Y
27 26 expd KHLXSYSpAtomsKqX+˙YrX+˙YpKqjoinKrpX+˙Y
28 27 ralrimiv KHLXSYSpAtomsKqX+˙YrX+˙YpKqjoinKrpX+˙Y
29 12 13 4 1 ispsubsp2 KHLX+˙YSX+˙YAtomsKpAtomsKqX+˙YrX+˙YpKqjoinKrpX+˙Y
30 29 3ad2ant1 KHLXSYSX+˙YSX+˙YAtomsKpAtomsKqX+˙YrX+˙YpKqjoinKrpX+˙Y
31 10 28 30 mpbir2and KHLXSYSX+˙YS