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 ) → ( 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ 𝐴 )