This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ { 𝑥 ∈ 𝑆 ∣ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 } )