Metamath Proof Explorer

Theorem dihlatat

Description: The reverse isomorphism H of a 1-dim subspace is an atom. (Contributed by NM, 28-Apr-2014)

Ref Expression
Hypotheses dihlatat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihlatat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihlatat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihlatat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihlatat.l ⊢ 𝐿 = ( LSAtoms ‘ 𝑈 )
Assertion dihlatat ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐿 ) → ( ◡ 𝐼 ‘ 𝑄 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 dihlatat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 dihlatat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihlatat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dihlatat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 dihlatat.l ⊢ 𝐿 = ( LSAtoms ‘ 𝑈 )
6 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 2 3 6 dvhlvec ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LVec )
8 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
9 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
10 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
11 8 9 10 5 islsat ⊢ ( 𝑈 ∈ LVec → ( 𝑄 ∈ 𝐿 ↔ ∃ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
12 7 11 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑄 ∈ 𝐿 ↔ ∃ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
13 12 biimpa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐿 ) → ∃ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
14 eldifsn ⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑈 ) ) )
15 1 2 3 8 10 9 4 dihlspsnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑈 ) ) → ( ◡ 𝐼 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ∈ 𝐴 )
16 15 3expb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑈 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑈 ) ) ) → ( ◡ 𝐼 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ∈ 𝐴 )
17 14 16 sylan2b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ) → ( ◡ 𝐼 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ∈ 𝐴 )
18 fveq2 ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( ◡ 𝐼 ‘ 𝑄 ) = ( ◡ 𝐼 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
19 18 eleq1d ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( ( ◡ 𝐼 ‘ 𝑄 ) ∈ 𝐴 ↔ ( ◡ 𝐼 ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ∈ 𝐴 ) )
20 17 19 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) ) → ( 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( ◡ 𝐼 ‘ 𝑄 ) ∈ 𝐴 ) )
21 20 rexlimdva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ∃ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( ◡ 𝐼 ‘ 𝑄 ) ∈ 𝐴 ) )
22 21 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐿 ) → ( ∃ 𝑣 ∈ ( ( Base ‘ 𝑈 ) ∖ { ( 0g ‘ 𝑈 ) } ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( ◡ 𝐼 ‘ 𝑄 ) ∈ 𝐴 ) )
23 13 22 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐿 ) → ( ◡ 𝐼 ‘ 𝑄 ) ∈ 𝐴 )