Metamath Proof Explorer

Theorem paddass

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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddass.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddass ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 paddass.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 paddass.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 simpl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝐾 ∈ HL )
4 simpr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑍 ⊆ 𝐴 )
5 simpr2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑌 ⊆ 𝐴 )
6 simpr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑋 ⊆ 𝐴 )
7 1 2 paddasslem18 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑍 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) ) → ( 𝑍 + ( 𝑌 + 𝑋 ) ) ⊆ ( ( 𝑍 + 𝑌 ) + 𝑋 ) )
8 3 4 5 6 7 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑍 + ( 𝑌 + 𝑋 ) ) ⊆ ( ( 𝑍 + 𝑌 ) + 𝑋 ) )
9 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
10 1 2 paddcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
11 9 10 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
12 11 3adant3r3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )
13 12 oveq1d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑌 + 𝑋 ) + 𝑍 ) )
14 1 2 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑌 + 𝑋 ) ⊆ 𝐴 )
15 3 5 6 14 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑌 + 𝑋 ) ⊆ 𝐴 )
16 1 2 paddcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑌 + 𝑋 ) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑌 + 𝑋 ) + 𝑍 ) = ( 𝑍 + ( 𝑌 + 𝑋 ) ) )
17 9 16 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑌 + 𝑋 ) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑌 + 𝑋 ) + 𝑍 ) = ( 𝑍 + ( 𝑌 + 𝑋 ) ) )
18 3 15 4 17 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑌 + 𝑋 ) + 𝑍 ) = ( 𝑍 + ( 𝑌 + 𝑋 ) ) )
19 13 18 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑍 + ( 𝑌 + 𝑋 ) ) )
20 1 2 paddcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑌 + 𝑍 ) = ( 𝑍 + 𝑌 ) )
21 9 20 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑌 + 𝑍 ) = ( 𝑍 + 𝑌 ) )
22 21 3adant3r1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑌 + 𝑍 ) = ( 𝑍 + 𝑌 ) )
23 22 oveq2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( 𝑋 + ( 𝑍 + 𝑌 ) ) )
24 1 2 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑍 + 𝑌 ) ⊆ 𝐴 )
25 3 4 5 24 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑍 + 𝑌 ) ⊆ 𝐴 )
26 1 2 paddcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ ( 𝑍 + 𝑌 ) ⊆ 𝐴 ) → ( 𝑋 + ( 𝑍 + 𝑌 ) ) = ( ( 𝑍 + 𝑌 ) + 𝑋 ) )
27 9 26 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ ( 𝑍 + 𝑌 ) ⊆ 𝐴 ) → ( 𝑋 + ( 𝑍 + 𝑌 ) ) = ( ( 𝑍 + 𝑌 ) + 𝑋 ) )
28 3 6 25 27 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + ( 𝑍 + 𝑌 ) ) = ( ( 𝑍 + 𝑌 ) + 𝑋 ) )
29 23 28 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ( 𝑍 + 𝑌 ) + 𝑋 ) )
30 8 19 29 3sstr4d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) ⊆ ( 𝑋 + ( 𝑌 + 𝑍 ) ) )
31 1 2 paddasslem18 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
32 30 31 eqssd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )