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 imbitrid ⊢ ( ( 𝐾 ∈ 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 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )