Metamath Proof Explorer

Theorem dihjat1

Description: Subspace sum of a closed subspace and an atom. ( pmapjat1 analog.) (Contributed by NM, 1-Oct-2014)

Ref Expression
Hypotheses dihjat1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihjat1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihjat1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dihjat1.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dihjat1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dihjat1.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihjat1.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
dihjat1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihjat1.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
dihjat1.q ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion dihjat1 ( 𝜑 → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )

Proof

Step Hyp Ref Expression
1 dihjat1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihjat1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dihjat1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 dihjat1.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
5 dihjat1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6 dihjat1.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7 dihjat1.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
8 dihjat1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 dihjat1.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
10 dihjat1.q ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
11 sneq ⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → { 𝑇 } = { ( 0g ‘ 𝑈 ) } )
12 11 fveq2d ⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑇 } ) = ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) )
13 1 2 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
14 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
15 14 5 lspsn0 ⊢ ( 𝑈 ∈ LMod → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
16 13 15 syl ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
17 12 16 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑇 = ( 0g ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝑇 } ) = { ( 0g ‘ 𝑈 ) } )
18 17 oveq2d ⊢ ( ( 𝜑 ∧ 𝑇 = ( 0g ‘ 𝑈 ) ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ∨ { ( 0g ‘ 𝑈 ) } ) )
19 1 2 14 6 7 8 9 djh01 ⊢ ( 𝜑 → ( 𝑋 ∨ { ( 0g ‘ 𝑈 ) } ) = 𝑋 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑇 = ( 0g ‘ 𝑈 ) ) → ( 𝑋 ∨ { ( 0g ‘ 𝑈 ) } ) = 𝑋 )
21 17 oveq2d ⊢ ( ( 𝜑 ∧ 𝑇 = ( 0g ‘ 𝑈 ) ) → ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ⊕ { ( 0g ‘ 𝑈 ) } ) )
22 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
23 1 2 6 22 dihrnlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
24 8 9 23 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
25 22 lsssubg ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ ( LSubSp ‘ 𝑈 ) ) → 𝑋 ∈ ( SubGrp ‘ 𝑈 ) )
26 13 24 25 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( SubGrp ‘ 𝑈 ) )
27 14 4 lsm01 ⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝑈 ) → ( 𝑋 ⊕ { ( 0g ‘ 𝑈 ) } ) = 𝑋 )
28 26 27 syl ⊢ ( 𝜑 → ( 𝑋 ⊕ { ( 0g ‘ 𝑈 ) } ) = 𝑋 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑇 = ( 0g ‘ 𝑈 ) ) → ( 𝑋 ⊕ { ( 0g ‘ 𝑈 ) } ) = 𝑋 )
30 21 29 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑇 = ( 0g ‘ 𝑈 ) ) → 𝑋 = ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )
31 18 20 30 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑇 = ( 0g ‘ 𝑈 ) ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )
32 8 adantr ⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
33 9 adantr ⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → 𝑋 ∈ ran 𝐼 )
34 10 anim1i ⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑇 ∈ 𝑉 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) )
35 eldifsn ⊢ ( 𝑇 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑇 ∈ 𝑉 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) )
36 34 35 sylibr ⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → 𝑇 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
37 1 2 3 4 5 6 7 32 33 14 36 dihjat1lem ⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )
38 31 37 pm2.61dane ⊢ ( 𝜑 → ( 𝑋 ∨ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑋 ⊕ ( 𝑁 ‘ { 𝑇 } ) ) )