Theorem diaf1oN

Description: The partial isomorphism A for a lattice K is a one-to-one, onto function. Part of Lemma M of Crawley p. 121 line 12, with closed subspaces rather than subspaces. See diadm for the domain. (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	diaf1oN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1-onto→ { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } )

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 3	diaf11N	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )
7		f1of1	⊢ ( 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 → 𝐼 : dom 𝐼 –1-1→ ran 𝐼 )
8	6 7	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1→ ran 𝐼 )
9	1 2 3 4 5	diarnN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 = { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } )
10		f1eq3	⊢ ( ran 𝐼 = { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } → ( 𝐼 : dom 𝐼 –1-1→ ran 𝐼 ↔ 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } ) )
11	9 10	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 : dom 𝐼 –1-1→ ran 𝐼 ↔ 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } ) )
12	8 11	mpbid	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } )
13		dff1o5	⊢ ( 𝐼 : dom 𝐼 –1-1-onto→ { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } ↔ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } ∧ ran 𝐼 = { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } ) )
14	12 9 13	sylanbrc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1-onto→ { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } )