Metamath Proof Explorer


Theorem paddclN

Description: The projective sum of two subspaces is a subspace. Part of Lemma 16.2 of MaedaMaeda p. 68. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses paddidm.s 𝑆 = ( PSubSp ‘ 𝐾 )
paddidm.p + = ( +𝑃𝐾 )
Assertion paddclN ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 paddidm.s 𝑆 = ( PSubSp ‘ 𝐾 )
2 paddidm.p + = ( +𝑃𝐾 )
3 simp1 ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → 𝐾 ∈ HL )
4 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
5 4 1 psubssat ( ( 𝐾 ∈ HL ∧ 𝑋𝑆 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
6 5 3adant3 ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
7 4 1 psubssat ( ( 𝐾 ∈ HL ∧ 𝑌𝑆 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
8 7 3adant2 ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
9 4 2 paddssat ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
10 3 6 8 9 syl3anc ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
11 olc ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑋 + 𝑌 ) ∃ 𝑟 ∈ ( 𝑋 + 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → ( ( 𝑝 ∈ ( 𝑋 + 𝑌 ) ∨ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑋 + 𝑌 ) ∃ 𝑟 ∈ ( 𝑋 + 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) )
12 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
13 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
14 12 13 4 2 elpadd ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) ↔ ( ( 𝑝 ∈ ( 𝑋 + 𝑌 ) ∨ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑋 + 𝑌 ) ∃ 𝑟 ∈ ( 𝑋 + 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
15 3 10 10 14 syl3anc ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) ↔ ( ( 𝑝 ∈ ( 𝑋 + 𝑌 ) ∨ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑋 + 𝑌 ) ∃ 𝑟 ∈ ( 𝑋 + 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
16 4 2 padd4N ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
17 3 6 8 6 8 16 syl122anc ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) = ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) )
18 1 2 paddidm ( ( 𝐾 ∈ HL ∧ 𝑋𝑆 ) → ( 𝑋 + 𝑋 ) = 𝑋 )
19 18 3adant3 ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( 𝑋 + 𝑋 ) = 𝑋 )
20 1 2 paddidm ( ( 𝐾 ∈ HL ∧ 𝑌𝑆 ) → ( 𝑌 + 𝑌 ) = 𝑌 )
21 20 3adant2 ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( 𝑌 + 𝑌 ) = 𝑌 )
22 19 21 oveq12d ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( ( 𝑋 + 𝑋 ) + ( 𝑌 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) )
23 17 22 eqtrd ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) = ( 𝑋 + 𝑌 ) )
24 23 eleq2d ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + ( 𝑋 + 𝑌 ) ) ↔ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) )
25 15 24 bitr3d ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( ( ( 𝑝 ∈ ( 𝑋 + 𝑌 ) ∨ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) ∨ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑋 + 𝑌 ) ∃ 𝑟 ∈ ( 𝑋 + 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ↔ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) )
26 11 25 syl5ib ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( 𝑋 + 𝑌 ) ∃ 𝑟 ∈ ( 𝑋 + 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → 𝑝 ∈ ( 𝑋 + 𝑌 ) ) )
27 26 expd ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → ( ∃ 𝑞 ∈ ( 𝑋 + 𝑌 ) ∃ 𝑟 ∈ ( 𝑋 + 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) → 𝑝 ∈ ( 𝑋 + 𝑌 ) ) ) )
28 27 ralrimiv ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ∀ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ∃ 𝑞 ∈ ( 𝑋 + 𝑌 ) ∃ 𝑟 ∈ ( 𝑋 + 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) → 𝑝 ∈ ( 𝑋 + 𝑌 ) ) )
29 12 13 4 1 ispsubsp2 ( 𝐾 ∈ HL → ( ( 𝑋 + 𝑌 ) ∈ 𝑆 ↔ ( ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ∃ 𝑞 ∈ ( 𝑋 + 𝑌 ) ∃ 𝑟 ∈ ( 𝑋 + 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) → 𝑝 ∈ ( 𝑋 + 𝑌 ) ) ) ) )
30 29 3ad2ant1 ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( ( 𝑋 + 𝑌 ) ∈ 𝑆 ↔ ( ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ∃ 𝑞 ∈ ( 𝑋 + 𝑌 ) ∃ 𝑟 ∈ ( 𝑋 + 𝑌 ) 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) → 𝑝 ∈ ( 𝑋 + 𝑌 ) ) ) ) )
31 10 28 30 mpbir2and ( ( 𝐾 ∈ HL ∧ 𝑋𝑆𝑌𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )