Theorem diarnN

Description: Partial isomorphism A maps onto the set of all closed subspaces of partial vector space A. Part of Lemma M of Crawley p. 121 line 12, with closed subspaces rather than subspaces. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvadia.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvadia.u	⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
	dvadia.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
	dvadia.n	⊢ ⊥ = ( ( ocA ‘ 𝐾 ) ‘ 𝑊 )
	dvadia.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
Assertion	diarnN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 = { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		dvadia.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dvadia.u	⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
3		dvadia.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4		dvadia.n	⊢ ⊥ = ( ( ocA ‘ 𝐾 ) ‘ 𝑊 )
5		dvadia.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6	1 2 3 5	diasslssN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 ⊆ 𝑆 )
7		sseqin2	⊢ ( ran 𝐼 ⊆ 𝑆 ↔ ( 𝑆 ∩ ran 𝐼 ) = ran 𝐼 )
8	6 7	sylib	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∩ ran 𝐼 ) = ran 𝐼 )
9	1 3 4	doca3N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 )
10	9	ex	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑥 ∈ ran 𝐼 → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) )
11	10	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ran 𝐼 → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) )
12	1 2 3 4 5	dvadiaN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝑆 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ) → 𝑥 ∈ ran 𝐼 )
13	12	expr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 → 𝑥 ∈ ran 𝐼 ) )
14	11 13	impbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ran 𝐼 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) )
15	14	rabbi2dva	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∩ ran 𝐼 ) = { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } )
16	8 15	eqtr3d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 = { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } )