Metamath Proof Explorer


Theorem paddss12

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

Ref Expression
Hypotheses padd0.a A = Atoms K
padd0.p + ˙ = + 𝑃 K
Assertion paddss12 K B Y A W A X Y Z W X + ˙ Z Y + ˙ W

Proof

Step Hyp Ref Expression
1 padd0.a A = Atoms K
2 padd0.p + ˙ = + 𝑃 K
3 simpl1 K B Y A W A X Y Z W K B
4 simpl2 K B Y A W A X Y Z W Y A
5 sstr Z W W A Z A
6 5 ancoms W A Z W Z A
7 6 ad2ant2l Y A W A X Y Z W Z A
8 7 3adantl1 K B Y A W A X Y Z W Z A
9 3 4 8 3jca K B Y A W A X Y Z W K B Y A Z A
10 simprl K B Y A W A X Y Z W X Y
11 1 2 paddss1 K B Y A Z A X Y X + ˙ Z Y + ˙ Z
12 9 10 11 sylc K B Y A W A X Y Z W X + ˙ Z Y + ˙ Z
13 1 2 paddss2 K B W A Y A Z W Y + ˙ Z Y + ˙ W
14 13 3com23 K B Y A W A Z W Y + ˙ Z Y + ˙ W
15 14 imp K B Y A W A Z W Y + ˙ Z Y + ˙ W
16 15 adantrl K B Y A W A X Y Z W Y + ˙ Z Y + ˙ W
17 12 16 sstrd K B Y A W A X Y Z W X + ˙ Z Y + ˙ W
18 17 ex K B Y A W A X Y Z W X + ˙ Z Y + ˙ W