Metamath Proof Explorer

Theorem dihatexv

Description: There is a nonzero vector that maps to every lattice atom. (Contributed by NM, 16-Aug-2014)

Ref Expression
Hypotheses dihatexv.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihatexv.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihatexv.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihatexv.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihatexv.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dihatexv.o ⊢ 0 = ( 0g ‘ 𝑈 )
dihatexv.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dihatexv.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihatexv.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihatexv.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
Assertion dihatexv ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) )

Proof

Step Hyp Ref Expression
1 dihatexv.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihatexv.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 dihatexv.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihatexv.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dihatexv.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
6 dihatexv.o ⊢ 0 = ( 0g ‘ 𝑈 )
7 dihatexv.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 dihatexv.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
9 dihatexv.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 dihatexv.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
11 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 simplr ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → 𝑄 ∈ 𝐴 )
13 simpr ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → 𝑄 ( le ‘ 𝐾 ) 𝑊 )
14 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
15 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
16 eqid ⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) )
17 1 14 2 3 15 16 4 8 7 dih1dimb2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ) → ∃ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ } ) ) )
18 11 12 13 17 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ∃ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ } ) ) )
19 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
20 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
21 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
22 1 3 15 21 16 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
23 19 22 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
24 3 15 21 4 5 dvhelvbasei ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ ∈ 𝑉 )
25 19 20 23 24 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ ∈ 𝑉 )
26 sneq ⊢ ( 𝑥 = ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ → { 𝑥 } = { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ } )
27 26 fveq2d ⊢ ( 𝑥 = ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ → ( 𝑁 ‘ { 𝑥 } ) = ( 𝑁 ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ } ) )
28 27 rspceeqv ⊢ ( ( ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ ∈ 𝑉 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ } ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) )
29 25 28 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ } ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) )
30 29 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ } ) → ∃ 𝑥 ∈ 𝑉 ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) )
31 30 adantld ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑔 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ } ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) )
32 31 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( ∃ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝑔 , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ 𝐵 ) ) ⟩ } ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) )
33 18 32 mpd ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) )
34 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
35 eqid ⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
36 14 2 3 35 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) )
37 34 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) )
38 simplr ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → 𝑄 ∈ 𝐴 )
39 simpr ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 )
40 eqid ⊢ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) = ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 )
41 14 2 3 15 40 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
42 34 37 38 39 41 syl112anc ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
43 3 15 21 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
44 34 43 syl ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
45 3 15 21 4 5 dvhelvbasei ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ 𝑉 )
46 34 42 44 45 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ 𝑉 )
47 14 2 3 35 15 8 4 7 40 dih1dimc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) )
48 34 38 39 47 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) )
49 sneq ⊢ ( 𝑥 = ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ → { 𝑥 } = { ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } )
50 49 fveq2d ⊢ ( 𝑥 = ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ → ( 𝑁 ‘ { 𝑥 } ) = ( 𝑁 ‘ { ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) )
51 50 rspceeqv ⊢ ( ( ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ 𝑉 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ ( ℩ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑓 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) )
52 46 48 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑊 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) )
53 33 52 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) )
54 9 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
55 54 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝐾 ∈ HL )
56 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
57 55 56 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝐾 ∈ AtLat )
58 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑄 ∈ 𝐴 )
59 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
60 59 2 atn0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≠ ( 0. ‘ 𝐾 ) )
61 57 58 60 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑄 ≠ ( 0. ‘ 𝐾 ) )
62 sneq ⊢ ( 𝑥 = 0 → { 𝑥 } = { 0 } )
63 62 fveq2d ⊢ ( 𝑥 = 0 → ( 𝑁 ‘ { 𝑥 } ) = ( 𝑁 ‘ { 0 } ) )
64 63 3ad2ant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → ( 𝑁 ‘ { 𝑥 } ) = ( 𝑁 ‘ { 0 } ) )
65 simp1ll ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → 𝜑 )
66 3 4 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
67 6 7 lspsn0 ⊢ ( 𝑈 ∈ LMod → ( 𝑁 ‘ { 0 } ) = { 0 } )
68 65 66 67 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → ( 𝑁 ‘ { 0 } ) = { 0 } )
69 64 68 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → ( 𝑁 ‘ { 𝑥 } ) = { 0 } )
70 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) )
71 59 3 8 4 6 dih0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
72 65 9 71 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
73 69 70 72 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → ( 𝐼 ‘ 𝑄 ) = ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) )
74 65 9 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
75 65 10 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → 𝑄 ∈ 𝐵 )
76 65 54 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → 𝐾 ∈ HL )
77 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
78 1 59 op0cl ⊢ ( 𝐾 ∈ OP → ( 0. ‘ 𝐾 ) ∈ 𝐵 )
79 76 77 78 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → ( 0. ‘ 𝐾 ) ∈ 𝐵 )
80 1 3 8 dih11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐵 ∧ ( 0. ‘ 𝐾 ) ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝑄 ) = ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ↔ 𝑄 = ( 0. ‘ 𝐾 ) ) )
81 74 75 79 80 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → ( ( 𝐼 ‘ 𝑄 ) = ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ↔ 𝑄 = ( 0. ‘ 𝐾 ) ) )
82 73 81 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ∧ 𝑥 = 0 ) → 𝑄 = ( 0. ‘ 𝐾 ) )
83 82 3expia ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝑥 = 0 → 𝑄 = ( 0. ‘ 𝐾 ) ) )
84 83 necon3d ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝑄 ≠ ( 0. ‘ 𝐾 ) → 𝑥 ≠ 0 ) )
85 61 84 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑥 ≠ 0 )
86 85 ex ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) → 𝑥 ≠ 0 ) )
87 86 ancrd ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) → ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) )
88 87 reximdva ⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ 𝑉 ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) → ∃ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) )
89 53 88 mpd ⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) )
90 89 ex ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 → ∃ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) )
91 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
92 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → 𝑄 ∈ 𝐵 )
93 1 3 8 dihcnvid1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐵 ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 𝑄 ) ) = 𝑄 )
94 91 92 93 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 𝑄 ) ) = 𝑄 )
95 fveq2 ⊢ ( ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 𝑄 ) ) = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) )
96 95 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 𝑄 ) ) = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) )
97 94 96 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → 𝑄 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) )
98 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → 𝑈 ∈ LMod )
99 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → 𝑥 ∈ 𝑉 )
100 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → 𝑥 ≠ 0 )
101 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
102 5 7 6 101 lsatlspsn2 ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) → ( 𝑁 ‘ { 𝑥 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
103 98 99 100 102 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → ( 𝑁 ‘ { 𝑥 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
104 2 3 4 8 101 dihlatat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑥 } ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ∈ 𝐴 )
105 91 103 104 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ∈ 𝐴 )
106 97 105 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) → 𝑄 ∈ 𝐴 )
107 106 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑄 ∈ 𝐴 ) )
108 107 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑄 ∈ 𝐴 ) )
109 90 108 impbid ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) ) )
110 rexdifsn ⊢ ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝑉 ( 𝑥 ≠ 0 ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) )
111 109 110 bitr4di ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) )