Metamath Proof Explorer

Theorem dihjat2

Description: The subspace sum of a closed subspace and an atom is the same as their subspace join. (Contributed by NM, 1-Oct-2014)

Ref Expression
Hypotheses dihjat2.h ⊢ H = LHyp ⁡ K
dihjat2.i ⊢ I = DIsoH ⁡ K ⁡ W
dihjat2.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
dihjat2.u ⊢ U = DVecH ⁡ K ⁡ W
dihjat2.p ⊢ ⊕ ˙ = LSSum ⁡ U
dihjat2.a ⊢ A = LSAtoms ⁡ U
dihjat2.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihjat2.x ⊢ φ → X ∈ ran ⁡ I
dihjat2.q ⊢ φ → Q ∈ A
Assertion dihjat2 ⊢ φ → X ∨ ˙ Q = X ⊕ ˙ Q

Proof

Step Hyp Ref Expression
1 dihjat2.h ⊢ H = LHyp ⁡ K
2 dihjat2.i ⊢ I = DIsoH ⁡ K ⁡ W
3 dihjat2.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
4 dihjat2.u ⊢ U = DVecH ⁡ K ⁡ W
5 dihjat2.p ⊢ ⊕ ˙ = LSSum ⁡ U
6 dihjat2.a ⊢ A = LSAtoms ⁡ U
7 dihjat2.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 dihjat2.x ⊢ φ → X ∈ ran ⁡ I
9 dihjat2.q ⊢ φ → Q ∈ A
10 eqid ⊢ Base U = Base U
11 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
12 7 adantr ⊢ φ ∧ v ∈ Base U → K ∈ HL ∧ W ∈ H
13 8 adantr ⊢ φ ∧ v ∈ Base U → X ∈ ran ⁡ I
14 simpr ⊢ φ ∧ v ∈ Base U → v ∈ Base U
15 1 4 10 5 11 2 3 12 13 14 dihjat1 ⊢ φ ∧ v ∈ Base U → X ∨ ˙ LSpan ⁡ U ⁡ v = X ⊕ ˙ LSpan ⁡ U ⁡ v
16 15 adantr ⊢ φ ∧ v ∈ Base U ∧ Q = LSpan ⁡ U ⁡ v → X ∨ ˙ LSpan ⁡ U ⁡ v = X ⊕ ˙ LSpan ⁡ U ⁡ v
17 oveq2 ⊢ Q = LSpan ⁡ U ⁡ v → X ∨ ˙ Q = X ∨ ˙ LSpan ⁡ U ⁡ v
18 17 adantl ⊢ φ ∧ v ∈ Base U ∧ Q = LSpan ⁡ U ⁡ v → X ∨ ˙ Q = X ∨ ˙ LSpan ⁡ U ⁡ v
19 oveq2 ⊢ Q = LSpan ⁡ U ⁡ v → X ⊕ ˙ Q = X ⊕ ˙ LSpan ⁡ U ⁡ v
20 19 adantl ⊢ φ ∧ v ∈ Base U ∧ Q = LSpan ⁡ U ⁡ v → X ⊕ ˙ Q = X ⊕ ˙ LSpan ⁡ U ⁡ v
21 16 18 20 3eqtr4d ⊢ φ ∧ v ∈ Base U ∧ Q = LSpan ⁡ U ⁡ v → X ∨ ˙ Q = X ⊕ ˙ Q
22 1 4 7 dvhlmod ⊢ φ → U ∈ LMod
23 10 11 6 islsati ⊢ U ∈ LMod ∧ Q ∈ A → ∃ v ∈ Base U Q = LSpan ⁡ U ⁡ v
24 22 9 23 syl2anc ⊢ φ → ∃ v ∈ Base U Q = LSpan ⁡ U ⁡ v
25 21 24 r19.29a ⊢ φ → X ∨ ˙ Q = X ⊕ ˙ Q