Theorem dihlspsnat 42499

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

Hypotheses

Ref	Expression
dihlspsnat.a	⊢ 𝐴 = (Atoms‘𝐾)
dihlspsnat.h	⊢ 𝐻 = (LHyp‘𝐾)
dihlspsnat.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihlspsnat.v	⊢ 𝑉 = (Base‘𝑈)
dihlspsnat.o	⊢ 0 = (0g‘𝑈)
dihlspsnat.n	⊢ 𝑁 = (LSpan‘𝑈)
dihlspsnat.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)

Assertion

Ref	Expression
dihlspsnat	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (◡𝐼‘(𝑁‘{𝑋})) ∈ 𝐴)

Proof of Theorem dihlspsnat

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2760	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		dihlspsnat.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
3		dihlspsnat.i	. . . . . 6 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
4		dihlspsnat.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
5		eqid 2760	. . . . . 6 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
6	1, 2, 3, 4, 5	dihf11 42433	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:(Base‘𝐾)–1-1→(LSubSp‘𝑈))
7	6	3ad2ant1 1151	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝐼:(Base‘𝐾)–1-1→(LSubSp‘𝑈))
8		f1f1orn 6841	. . . 4 ⊢ (𝐼:(Base‘𝐾)–1-1→(LSubSp‘𝑈) → 𝐼:(Base‘𝐾)–1-1-onto→ran 𝐼)
9	7, 8	syl 18	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝐼:(Base‘𝐾)–1-1-onto→ran 𝐼)
10		dihlspsnat.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
11		dihlspsnat.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
12	2, 4, 10, 11, 3	dihlsprn 42497	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ ran 𝐼)
13	12	3adant3 1150	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋}) ∈ ran 𝐼)
14		f1ocnvdm 7297	. . 3 ⊢ ((𝐼:(Base‘𝐾)–1-1-onto→ran 𝐼 ∧ (𝑁‘{𝑋}) ∈ ran 𝐼) → (◡𝐼‘(𝑁‘{𝑋})) ∈ (Base‘𝐾))
15	9, 13, 14	syl2anc 596	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (◡𝐼‘(𝑁‘{𝑋})) ∈ (Base‘𝐾))
16		fveq2 6890	. . . . 5 ⊢ ((◡𝐼‘(𝑁‘{𝑋})) = (0.‘𝐾) → (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) = (𝐼‘(0.‘𝐾)))
17	2, 3	dihcnvid2 42439	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑋}) ∈ ran 𝐼) → (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) = (𝑁‘{𝑋}))
18	12, 17	syldan 603	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) = (𝑁‘{𝑋}))
19		eqid 2760	. . . . . . . . 9 ⊢ (0.‘𝐾) = (0.‘𝐾)
20		dihlspsnat.o	. . . . . . . . 9 ⊢ 0 = (0g‘𝑈)
21	19, 2, 3, 4, 20	dih0 42446	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐼‘(0.‘𝐾)) = { 0 })
22	21	adantr 486	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → (𝐼‘(0.‘𝐾)) = { 0 })
23	18, 22	eqeq12d 2776	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → ((𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) = (𝐼‘(0.‘𝐾)) ↔ (𝑁‘{𝑋}) = { 0 }))
24		id 23	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
25	2, 4, 24	dvhlmod 42276	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LMod)
26	10, 20, 11	lspsneq0 21296	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑁‘{𝑋}) = { 0 } ↔ 𝑋 = 0 ))
27	25, 26	sylan 592	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → ((𝑁‘{𝑋}) = { 0 } ↔ 𝑋 = 0 ))
28	23, 27	bitrd 282	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → ((𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) = (𝐼‘(0.‘𝐾)) ↔ 𝑋 = 0 ))
29	16, 28	imbitrid 247	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → ((◡𝐼‘(𝑁‘{𝑋})) = (0.‘𝐾) → 𝑋 = 0 ))
30	29	necon3d 2976	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → (𝑋 ≠ 0 → (◡𝐼‘(𝑁‘{𝑋})) ≠ (0.‘𝐾)))
31	30	3impia 1135	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (◡𝐼‘(𝑁‘{𝑋})) ≠ (0.‘𝐾))
32		simpll1 1231	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (𝐼‘𝑥) ⊆ (𝑁‘{𝑋})) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
33	2, 4, 32	dvhlvec 42275	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (𝐼‘𝑥) ⊆ (𝑁‘{𝑋})) → 𝑈 ∈ LVec)
34		simplr 781	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (𝐼‘𝑥) ⊆ (𝑁‘{𝑋})) → 𝑥 ∈ (Base‘𝐾))
35	1, 2, 3, 4, 5	dihlss 42416	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝐼‘𝑥) ∈ (LSubSp‘𝑈))
36	32, 34, 35	syl2anc 596	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (𝐼‘𝑥) ⊆ (𝑁‘{𝑋})) → (𝐼‘𝑥) ∈ (LSubSp‘𝑈))
37		simpll2 1232	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (𝐼‘𝑥) ⊆ (𝑁‘{𝑋})) → 𝑋 ∈ 𝑉)
38		simpr 490	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (𝐼‘𝑥) ⊆ (𝑁‘{𝑋})) → (𝐼‘𝑥) ⊆ (𝑁‘{𝑋}))
39	10, 20, 5, 11	lspsnat 21432	. . . . . 6 ⊢ (((𝑈 ∈ LVec ∧ (𝐼‘𝑥) ∈ (LSubSp‘𝑈) ∧ 𝑋 ∈ 𝑉) ∧ (𝐼‘𝑥) ⊆ (𝑁‘{𝑋})) → ((𝐼‘𝑥) = (𝑁‘{𝑋}) ∨ (𝐼‘𝑥) = { 0 }))
40	33, 36, 37, 38, 39	syl31anc 1400	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (𝐼‘𝑥) ⊆ (𝑁‘{𝑋})) → ((𝐼‘𝑥) = (𝑁‘{𝑋}) ∨ (𝐼‘𝑥) = { 0 }))
41	40	ex 418	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐼‘𝑥) ⊆ (𝑁‘{𝑋}) → ((𝐼‘𝑥) = (𝑁‘{𝑋}) ∨ (𝐼‘𝑥) = { 0 })))
42		simp1 1154	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
43	42, 13, 17	syl2anc 596	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) = (𝑁‘{𝑋}))
44	43	adantr 486	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) = (𝑁‘{𝑋}))
45	44	sseq2d 3941	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐼‘𝑥) ⊆ (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) ↔ (𝐼‘𝑥) ⊆ (𝑁‘{𝑋})))
46		simpl1 1210	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
47		simpr 490	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → 𝑥 ∈ (Base‘𝐾))
48	15	adantr 486	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → (◡𝐼‘(𝑁‘{𝑋})) ∈ (Base‘𝐾))
49		eqid 2760	. . . . . . 7 ⊢ (le‘𝐾) = (le‘𝐾)
50	1, 49, 2, 3	dihord 42430	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ (Base‘𝐾) ∧ (◡𝐼‘(𝑁‘{𝑋})) ∈ (Base‘𝐾)) → ((𝐼‘𝑥) ⊆ (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) ↔ 𝑥(le‘𝐾)(◡𝐼‘(𝑁‘{𝑋}))))
51	46, 47, 48, 50	syl3anc 1398	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐼‘𝑥) ⊆ (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) ↔ 𝑥(le‘𝐾)(◡𝐼‘(𝑁‘{𝑋}))))
52	45, 51	bitr3d 284	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐼‘𝑥) ⊆ (𝑁‘{𝑋}) ↔ 𝑥(le‘𝐾)(◡𝐼‘(𝑁‘{𝑋}))))
53	44	eqeq2d 2771	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐼‘𝑥) = (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) ↔ (𝐼‘𝑥) = (𝑁‘{𝑋})))
54	1, 2, 3	dih11 42431	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ (Base‘𝐾) ∧ (◡𝐼‘(𝑁‘{𝑋})) ∈ (Base‘𝐾)) → ((𝐼‘𝑥) = (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) ↔ 𝑥 = (◡𝐼‘(𝑁‘{𝑋}))))
55	46, 47, 48, 54	syl3anc 1398	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐼‘𝑥) = (𝐼‘(◡𝐼‘(𝑁‘{𝑋}))) ↔ 𝑥 = (◡𝐼‘(𝑁‘{𝑋}))))
56	53, 55	bitr3d 284	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐼‘𝑥) = (𝑁‘{𝑋}) ↔ 𝑥 = (◡𝐼‘(𝑁‘{𝑋}))))
57	46, 21	syl 18	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝐼‘(0.‘𝐾)) = { 0 })
58	57	eqeq2d 2771	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐼‘𝑥) = (𝐼‘(0.‘𝐾)) ↔ (𝐼‘𝑥) = { 0 }))
59		simpl1l 1243	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → 𝐾 ∈ HL)
60		hlop 40528	. . . . . . . 8 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
61	1, 19	op0cl 40350	. . . . . . . 8 ⊢ (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
62	59, 60, 61	3syl 19	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → (0.‘𝐾) ∈ (Base‘𝐾))
63	1, 2, 3	dih11 42431	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ (Base‘𝐾) ∧ (0.‘𝐾) ∈ (Base‘𝐾)) → ((𝐼‘𝑥) = (𝐼‘(0.‘𝐾)) ↔ 𝑥 = (0.‘𝐾)))
64	46, 47, 62, 63	syl3anc 1398	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐼‘𝑥) = (𝐼‘(0.‘𝐾)) ↔ 𝑥 = (0.‘𝐾)))
65	58, 64	bitr3d 284	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐼‘𝑥) = { 0 } ↔ 𝑥 = (0.‘𝐾)))
66	56, 65	orbi12d 932	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → (((𝐼‘𝑥) = (𝑁‘{𝑋}) ∨ (𝐼‘𝑥) = { 0 }) ↔ (𝑥 = (◡𝐼‘(𝑁‘{𝑋})) ∨ 𝑥 = (0.‘𝐾))))
67	41, 52, 66	3imtr3d 296	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥(le‘𝐾)(◡𝐼‘(𝑁‘{𝑋})) → (𝑥 = (◡𝐼‘(𝑁‘{𝑋})) ∨ 𝑥 = (0.‘𝐾))))
68	67	ralrimiva 3154	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ∀𝑥 ∈ (Base‘𝐾)(𝑥(le‘𝐾)(◡𝐼‘(𝑁‘{𝑋})) → (𝑥 = (◡𝐼‘(𝑁‘{𝑋})) ∨ 𝑥 = (0.‘𝐾))))
69		simp1l 1216	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝐾 ∈ HL)
70		hlatl 40526	. . 3 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
71		dihlspsnat.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
72	1, 49, 19, 71	isat3 40473	. . 3 ⊢ (𝐾 ∈ AtLat → ((◡𝐼‘(𝑁‘{𝑋})) ∈ 𝐴 ↔ ((◡𝐼‘(𝑁‘{𝑋})) ∈ (Base‘𝐾) ∧ (◡𝐼‘(𝑁‘{𝑋})) ≠ (0.‘𝐾) ∧ ∀𝑥 ∈ (Base‘𝐾)(𝑥(le‘𝐾)(◡𝐼‘(𝑁‘{𝑋})) → (𝑥 = (◡𝐼‘(𝑁‘{𝑋})) ∨ 𝑥 = (0.‘𝐾))))))
73	69, 70, 72	3syl 19	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ((◡𝐼‘(𝑁‘{𝑋})) ∈ 𝐴 ↔ ((◡𝐼‘(𝑁‘{𝑋})) ∈ (Base‘𝐾) ∧ (◡𝐼‘(𝑁‘{𝑋})) ≠ (0.‘𝐾) ∧ ∀𝑥 ∈ (Base‘𝐾)(𝑥(le‘𝐾)(◡𝐼‘(𝑁‘{𝑋})) → (𝑥 = (◡𝐼‘(𝑁‘{𝑋})) ∨ 𝑥 = (0.‘𝐾))))))
74	15, 31, 68, 73	mpbir3and 1361	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (◡𝐼‘(𝑁‘{𝑋})) ∈ 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076   ⊆ wss 3896  {csn 4584   class class class wbr 5102  ^◡ccnv 5650  ran crn 5652  –1-1→wf1 6540  –1-1-onto→wf1o 6542  ‘cfv 6543  Basecbs 17396  lecple 17444  0_gc0g 17619  0.cp0 18604  LModclmod 21144  LSubSpclss 21215  LSpanclspn 21255  LVecclvec 21386  OPcops 40338  Atomscatm 40429  AtLatcal 40430  HLchlt 40516  LHypclh 41150  DVecHcdvh 42244  DIsoHcdih 42394

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284  ax-riotaBAD 40119

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7882  df-1st 8005  df-2nd 8006  df-tpos 8250  df-undef 8297  df-frecs 8306  df-wrecs 8337  df-recs 8386  df-rdg 8425  df-1o 8483  df-er 8724  df-map 8856  df-en 8981  df-dom 8982  df-sdom 8983  df-fin 8984  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-nn 12343  df-2 12412  df-3 12413  df-4 12414  df-5 12415  df-6 12416  df-n0 12614  df-z 12701  df-uz 12973  df-fz 13647  df-struct 17334  df-sets 17351  df-slot 17369  df-ndx 17381  df-base 17397  df-ress 17418  df-plusg 17450  df-mulr 17451  df-sca 17453  df-vsca 17454  df-0g 17621  df-proset 18477  df-poset 18496  df-plt 18511  df-lub 18527  df-glb 18528  df-join 18529  df-meet 18530  df-p0 18606  df-p1 18607  df-lat 18615  df-clat 18682  df-mgm 18825  df-sgrp 18917  df-mnd 18933  df-submnd 18988  df-grp 19156  df-minusg 19157  df-sbg 19158  df-subg 19342  df-cntz 19540  df-lsm 19859  df-cmn 20005  df-abl 20006  df-mgp 20370  df-rng 20384  df-ur 20417  df-ring 20470  df-oppr 20576  df-dvdsr 20596  df-unit 20597  df-invr 20627  df-dvr 20640  df-drng 20991  df-lmod 21146  df-lss 21216  df-lsp 21256  df-lvec 21387  df-lsatoms 40142  df-oposet 40342  df-ol 40344  df-oml 40345  df-covers 40432  df-ats 40433  df-atl 40464  df-cvlat 40488  df-hlat 40517  df-llines 40664  df-lplanes 40665  df-lvols 40666  df-lines 40667  df-psubsp 40669  df-pmap 40670  df-padd 40962  df-lhyp 41154  df-laut 41155  df-ldil 41270  df-ltrn 41271  df-trl 41325  df-tendo 41921  df-edring 41923  df-disoa 42195  df-dvech 42245  df-dib 42305  df-dic 42339  df-dih 42395

This theorem is used by:  dihlatat  42503  djhcvat42  42581  dihprrnlem1N  42590  dihprrnlem2  42591