Metamath Proof Explorer

Theorem dochkrsm

Description: The subspace sum of a closed subspace and a kernel orthocomplement is closed. ( djhlsmcl can be used to convert sum to join.) (Contributed by NM, 29-Jan-2015)

Ref Expression
Hypotheses dochkrsm.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochkrsm.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dochkrsm.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochkrsm.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochkrsm.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dochkrsm.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
dochkrsm.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
dochkrsm.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochkrsm.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
dochkrsm.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion dochkrsm ( 𝜑 → ( 𝑋 ⊕ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dochkrsm.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochkrsm.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dochkrsm.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 dochkrsm.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dochkrsm.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
6 dochkrsm.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7 dochkrsm.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
8 dochkrsm.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 dochkrsm.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
10 dochkrsm.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
11 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
12 8 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 9 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → 𝑋 ∈ ran 𝐼 )
14 simpr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
15 1 2 4 5 11 12 13 14 dihsmatrn ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ( 𝑋 ⊕ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ ran 𝐼 )
16 oveq2 ⊢ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = { ( 0g ‘ 𝑈 ) } → ( 𝑋 ⊕ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝑋 ⊕ { ( 0g ‘ 𝑈 ) } ) )
17 1 4 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
18 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
19 1 4 2 18 dihrnlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
20 8 9 19 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
21 18 lsssubg ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ ( LSubSp ‘ 𝑈 ) ) → 𝑋 ∈ ( SubGrp ‘ 𝑈 ) )
22 17 20 21 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( SubGrp ‘ 𝑈 ) )
23 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
24 23 5 lsm01 ⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝑈 ) → ( 𝑋 ⊕ { ( 0g ‘ 𝑈 ) } ) = 𝑋 )
25 22 24 syl ⊢ ( 𝜑 → ( 𝑋 ⊕ { ( 0g ‘ 𝑈 ) } ) = 𝑋 )
26 16 25 sylan9eqr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( 𝑋 ⊕ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = 𝑋 )
27 9 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = { ( 0g ‘ 𝑈 ) } ) → 𝑋 ∈ ran 𝐼 )
28 26 27 eqeltrd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = { ( 0g ‘ 𝑈 ) } ) → ( 𝑋 ⊕ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ ran 𝐼 )
29 1 3 4 23 11 6 7 8 10 dochsat0 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ∨ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = { ( 0g ‘ 𝑈 ) } ) )
30 15 28 29 mpjaodan ⊢ ( 𝜑 → ( 𝑋 ⊕ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ ran 𝐼 )