Metamath Proof Explorer


Theorem paddss1

Description: Subset law for projective subspace sum. ( unss1 analog.) (Contributed by NM, 7-Mar-2012)

Ref Expression
Hypotheses padd0.a A=AtomsK
padd0.p +˙=+𝑃K
Assertion paddss1 KBYAZAXYX+˙ZY+˙Z

Proof

Step Hyp Ref Expression
1 padd0.a A=AtomsK
2 padd0.p +˙=+𝑃K
3 ssel XYpXpY
4 3 orim1d XYpXpZpYpZ
5 ssrexv XYqXrZpKqjoinKrqYrZpKqjoinKr
6 5 anim2d XYpAqXrZpKqjoinKrpAqYrZpKqjoinKr
7 4 6 orim12d XYpXpZpAqXrZpKqjoinKrpYpZpAqYrZpKqjoinKr
8 7 adantl KBYAZAXYpXpZpAqXrZpKqjoinKrpYpZpAqYrZpKqjoinKr
9 simpl1 KBYAZAXYKB
10 sstr XYYAXA
11 10 3ad2antr2 XYKBYAZAXA
12 11 ancoms KBYAZAXYXA
13 simpl3 KBYAZAXYZA
14 eqid K=K
15 eqid joinK=joinK
16 14 15 1 2 elpadd KBXAZApX+˙ZpXpZpAqXrZpKqjoinKr
17 9 12 13 16 syl3anc KBYAZAXYpX+˙ZpXpZpAqXrZpKqjoinKr
18 14 15 1 2 elpadd KBYAZApY+˙ZpYpZpAqYrZpKqjoinKr
19 18 adantr KBYAZAXYpY+˙ZpYpZpAqYrZpKqjoinKr
20 8 17 19 3imtr4d KBYAZAXYpX+˙ZpY+˙Z
21 20 ssrdv KBYAZAXYX+˙ZY+˙Z
22 21 ex KBYAZAXYX+˙ZY+˙Z