dochkrsat

Description: The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014)

	Ref	Expression
Hypotheses	dochkrsat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochkrsat.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochkrsat.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochkrsat.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
	dochkrsat.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	dochkrsat.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	dochkrsat.z	⊢ 0 = ( 0_g ‘ 𝑈 )
	dochkrsat.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochkrsat.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	dochkrsat	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { 0 } ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dochkrsat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochkrsat.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochkrsat.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochkrsat.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
5		dochkrsat.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		dochkrsat.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		dochkrsat.z	⊢ 0 = ( 0_g ‘ 𝑈 )
8		dochkrsat.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		dochkrsat.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
11		eqid	⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
12	1 2 3 10 11 5 6 8 9	dochkrshp	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( Base ‘ 𝑈 ) ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ ( LSHyp ‘ 𝑈 ) ) )
13	1 3 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
14	10 5 6 13 9	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) )
15	1 2 3 10 7 8 14	dochn0nv	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { 0 } ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ ( Base ‘ 𝑈 ) ) )
16		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
17	1 3 10 16 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
18	8 14 17	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
19	1 2 3 16 4 11 8 18	dochsatshpb	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ ( LSHyp ‘ 𝑈 ) ) )
20	12 15 19	3bitr4d	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { 0 } ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ) )

Metamath Proof Explorer

Theorem dochkrsat

Proof