Metamath Proof Explorer


Theorem padd12N

Description: Commutative/associative law for projective subspace sum. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses paddass.a A = Atoms K
paddass.p + ˙ = + 𝑃 K
Assertion padd12N K HL X A Y A Z A X + ˙ Y + ˙ Z = Y + ˙ X + ˙ Z

Proof

Step Hyp Ref Expression
1 paddass.a A = Atoms K
2 paddass.p + ˙ = + 𝑃 K
3 hllat K HL K Lat
4 3 adantr K HL X A Y A Z A K Lat
5 simpr1 K HL X A Y A Z A X A
6 simpr2 K HL X A Y A Z A Y A
7 1 2 paddcom K Lat X A Y A X + ˙ Y = Y + ˙ X
8 4 5 6 7 syl3anc K HL X A Y A Z A X + ˙ Y = Y + ˙ X
9 8 oveq1d K HL X A Y A Z A X + ˙ Y + ˙ Z = Y + ˙ X + ˙ Z
10 1 2 paddass K HL X A Y A Z A X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z
11 simpl K HL X A Y A Z A K HL
12 simpr3 K HL X A Y A Z A Z A
13 1 2 paddass K HL Y A X A Z A Y + ˙ X + ˙ Z = Y + ˙ X + ˙ Z
14 11 6 5 12 13 syl13anc K HL X A Y A Z A Y + ˙ X + ˙ Z = Y + ˙ X + ˙ Z
15 9 10 14 3eqtr3d K HL X A Y A Z A X + ˙ Y + ˙ Z = Y + ˙ X + ˙ Z