Metamath Proof Explorer

Theorem osumclN

Description: Closure of orthogonal sum. If X and Y are orthogonal closed projective subspaces, then their sum is closed. (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses osumcl.p ⊢ + = ( +𝑃 ‘ 𝐾 )
osumcl.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
osumcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion osumclN ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 osumcl.p ⊢ + = ( +𝑃 ‘ 𝐾 )
2 osumcl.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3 osumcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
4 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝐾 ∈ HL )
5 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝑋 ∈ 𝐶 )
6 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7 6 3 psubclssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
8 4 5 7 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
9 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝑌 ∈ 𝐶 )
10 6 3 psubclssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
11 4 9 10 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
12 6 1 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
13 4 8 11 12 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
14 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ 𝑋 = ∅ ) → 𝐾 ∈ HL )
15 oveq1 ⊢ ( 𝑋 = ∅ → ( 𝑋 + 𝑌 ) = ( ∅ + 𝑌 ) )
16 6 1 padd02 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ∅ + 𝑌 ) = 𝑌 )
17 4 11 16 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ∅ + 𝑌 ) = 𝑌 )
18 15 17 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ 𝑋 = ∅ ) → ( 𝑋 + 𝑌 ) = 𝑌 )
19 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ 𝑋 = ∅ ) → 𝑌 ∈ 𝐶 )
20 18 19 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ 𝑋 = ∅ ) → ( 𝑋 + 𝑌 ) ∈ 𝐶 )
21 2 3 psubcli2N ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ∈ 𝐶 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) = ( 𝑋 + 𝑌 ) )
22 14 20 21 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ 𝑋 = ∅ ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) = ( 𝑋 + 𝑌 ) )
23 1 2 3 osumcllem11N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → ( 𝑋 + 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) )
24 23 anassrs ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ 𝑋 ≠ ∅ ) → ( 𝑋 + 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) )
25 24 eqcomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ 𝑋 ≠ ∅ ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) = ( 𝑋 + 𝑌 ) )
26 22 25 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) = ( 𝑋 + 𝑌 ) )
27 6 2 3 ispsubclN ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 + 𝑌 ) ∈ 𝐶 ↔ ( ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) = ( 𝑋 + 𝑌 ) ) ) )
28 4 27 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ( 𝑋 + 𝑌 ) ∈ 𝐶 ↔ ( ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) = ( 𝑋 + 𝑌 ) ) ) )
29 13 26 28 mpbir2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐶 )