Metamath Proof Explorer

Theorem dihjat4

Description: Transfer the subspace sum of a closed subspace and an atom back to lattice join. (Contributed by NM, 25-Apr-2015)

Ref Expression
Hypotheses dihjat4.j ⊢ ∨ = ( join ‘ 𝐾 )
dihjat4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihjat4.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihjat4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihjat4.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dihjat4.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dihjat4.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihjat4.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
dihjat4.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion dihjat4 ( 𝜑 → ( 𝑋 ⊕ 𝑄 ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑄 ) ) ) )

Proof

Step Hyp Ref Expression
1 dihjat4.j ⊢ ∨ = ( join ‘ 𝐾 )
2 dihjat4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihjat4.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dihjat4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dihjat4.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
6 dihjat4.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
7 dihjat4.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 dihjat4.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
9 dihjat4.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
12 10 2 3 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
13 7 8 12 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
14 11 2 4 3 6 dihlatat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) → ( ◡ 𝐼 ‘ 𝑄 ) ∈ ( Atoms ‘ 𝐾 ) )
15 7 9 14 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑄 ) ∈ ( Atoms ‘ 𝐾 ) )
16 10 2 1 11 4 5 3 7 13 15 dihjat3 ⊢ ( 𝜑 → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑄 ) ) ) = ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ⊕ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑄 ) ) ) )
17 2 3 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
18 7 8 17 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
19 2 4 3 6 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ ran 𝐼 )
20 7 9 19 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ ran 𝐼 )
21 2 3 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑄 ) ) = 𝑄 )
22 7 20 21 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑄 ) ) = 𝑄 )
23 18 22 oveq12d ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ⊕ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑄 ) ) ) = ( 𝑋 ⊕ 𝑄 ) )
24 16 23 eqtr2d ⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑄 ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑄 ) ) ) )