# Metamath Proof Explorer

Description: Projective subspace sum is associative. Equation 16.2.1 of MaedaMaeda p. 68. In our version, the subspaces do not have to be nonempty. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses paddass.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$

### Proof

Step Hyp Ref Expression
1 paddass.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 simpl ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\to {K}\in \mathrm{HL}$
4 simpr3 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\to {Z}\subseteq {A}$
5 simpr2 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\to {Y}\subseteq {A}$
6 simpr1 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\to {X}\subseteq {A}$
8 3 4 5 6 7 syl13anc
9 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
11 9 10 syl3an1
13 12 oveq1d
15 3 5 6 14 syl3anc
17 9 16 syl3an1
18 3 15 4 17 syl3anc
19 13 18 eqtrd