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	⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑄 ) = ( 𝐼 ‘ ( ( ^◡ 𝐼 ‘ 𝑋 ) ∨ ( ^◡ 𝐼 ‘ 𝑄 ) ) ) )

Metamath Proof Explorer

Theorem dihjat4

Proof