Metamath Proof Explorer

Theorem dihlspsnat

Description: The inverse isomorphism H of the span of a singleton is a Hilbert lattice atom. (Contributed by NM, 27-Apr-2014)

Ref Expression
Hypotheses dihlspsnat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihlspsnat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihlspsnat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihlspsnat.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dihlspsnat.o ⊢ 0 = ( 0g ‘ 𝑈 )
dihlspsnat.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dihlspsnat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihlspsnat ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 dihlspsnat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 dihlspsnat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihlspsnat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dihlspsnat.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dihlspsnat.o ⊢ 0 = ( 0g ‘ 𝑈 )
6 dihlspsnat.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7 dihlspsnat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
10 8 2 7 3 9 dihf11 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : ( Base ‘ 𝐾 ) –1-1→ ( LSubSp ‘ 𝑈 ) )
11 10 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝐼 : ( Base ‘ 𝐾 ) –1-1→ ( LSubSp ‘ 𝑈 ) )
12 f1f1orn ⊢ ( 𝐼 : ( Base ‘ 𝐾 ) –1-1→ ( LSubSp ‘ 𝑈 ) → 𝐼 : ( Base ‘ 𝐾 ) –1-1-onto→ ran 𝐼 )
13 11 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝐼 : ( Base ‘ 𝐾 ) –1-1-onto→ ran 𝐼 )
14 2 3 4 6 7 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
15 14 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
16 f1ocnvdm ⊢ ( ( 𝐼 : ( Base ‘ 𝐾 ) –1-1-onto→ ran 𝐼 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Base ‘ 𝐾 ) )
17 13 15 16 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Base ‘ 𝐾 ) )
18 fveq2 ⊢ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 0. ‘ 𝐾 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) )
19 2 7 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝑁 ‘ { 𝑋 } ) )
20 14 19 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝑁 ‘ { 𝑋 } ) )
21 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
22 21 2 7 3 5 dih0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
23 22 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
24 20 23 eqeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) = { 0 } ) )
25 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
26 2 3 25 dvhlmod ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LMod )
27 4 5 6 lspsneq0 ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
28 26 27 sylan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 0 } ↔ 𝑋 = 0 ) )
29 24 28 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ↔ 𝑋 = 0 ) )
30 18 29 syl5ib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 0. ‘ 𝐾 ) → 𝑋 = 0 ) )
31 30 necon3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ≠ 0 → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ≠ ( 0. ‘ 𝐾 ) ) )
32 31 3impia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ≠ ( 0. ‘ 𝐾 ) )
33 simpll1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
34 2 3 33 dvhlvec ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑈 ∈ LVec )
35 simplr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
36 8 2 7 3 9 dihlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ 𝑥 ) ∈ ( LSubSp ‘ 𝑈 ) )
37 33 35 36 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝐼 ‘ 𝑥 ) ∈ ( LSubSp ‘ 𝑈 ) )
38 simpll2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑋 ∈ 𝑉 )
39 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) )
40 4 5 9 6 lspsnat ⊢ ( ( ( 𝑈 ∈ LVec ∧ ( 𝐼 ‘ 𝑥 ) ∈ ( LSubSp ‘ 𝑈 ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝑁 ‘ { 𝑋 } ) ∨ ( 𝐼 ‘ 𝑥 ) = { 0 } ) )
41 34 37 38 39 40 syl31anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝑁 ‘ { 𝑋 } ) ∨ ( 𝐼 ‘ 𝑥 ) = { 0 } ) )
42 41 ex ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝑁 ‘ { 𝑋 } ) ∨ ( 𝐼 ‘ 𝑥 ) = { 0 } ) ) )
43 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
44 43 15 19 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝑁 ‘ { 𝑋 } ) )
45 44 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝑁 ‘ { 𝑋 } ) )
46 45 sseq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) ↔ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ) )
47 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
48 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
49 17 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Base ‘ 𝐾 ) )
50 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
51 8 50 2 7 dihord ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) ↔ 𝑥 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) )
52 47 48 49 51 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) ↔ 𝑥 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) )
53 46 52 bitr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ↔ 𝑥 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) )
54 45 eqeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) ↔ ( 𝐼 ‘ 𝑥 ) = ( 𝑁 ‘ { 𝑋 } ) ) )
55 8 2 7 dih11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) ↔ 𝑥 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) )
56 47 48 49 55 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) ↔ 𝑥 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) )
57 54 56 bitr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝑁 ‘ { 𝑋 } ) ↔ 𝑥 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ) )
58 47 22 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
59 58 eqeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ↔ ( 𝐼 ‘ 𝑥 ) = { 0 } ) )
60 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ HL )
61 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
62 8 21 op0cl ⊢ ( 𝐾 ∈ OP → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
63 60 61 62 3syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
64 8 2 7 dih11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ↔ 𝑥 = ( 0. ‘ 𝐾 ) ) )
65 47 48 63 64 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ↔ 𝑥 = ( 0. ‘ 𝐾 ) ) )
66 59 65 bitr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑥 ) = { 0 } ↔ 𝑥 = ( 0. ‘ 𝐾 ) ) )
67 57 66 orbi12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝐼 ‘ 𝑥 ) = ( 𝑁 ‘ { 𝑋 } ) ∨ ( 𝐼 ‘ 𝑥 ) = { 0 } ) ↔ ( 𝑥 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∨ 𝑥 = ( 0. ‘ 𝐾 ) ) ) )
68 42 53 67 3imtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑥 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∨ 𝑥 = ( 0. ‘ 𝐾 ) ) ) )
69 68 ralrimiva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑥 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∨ 𝑥 = ( 0. ‘ 𝐾 ) ) ) )
70 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝐾 ∈ HL )
71 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
72 8 50 21 1 isat3 ⊢ ( 𝐾 ∈ AtLat → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ 𝐴 ↔ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ≠ ( 0. ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑥 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∨ 𝑥 = ( 0. ‘ 𝐾 ) ) ) ) ) )
73 70 71 72 3syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ 𝐴 ↔ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ≠ ( 0. ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑥 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∨ 𝑥 = ( 0. ‘ 𝐾 ) ) ) ) ) )
74 17 32 69 73 mpbir3and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ 𝐴 )