dihatexv - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dihatexv		Structured version Visualization version GIF version

Theorem dihatexv 41327

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

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

**Assertion**
Ref	Expression
dihatexv	⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })(𝐼‘𝑄) = (𝑁‘{𝑥})))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝑥,𝐼 𝑥,𝐾 𝑥,𝑁 𝑥,𝑄 𝑥,𝑉 𝑥,𝑊 𝜑,𝑥 Allowed substitution hints: 𝑈(𝑥) 𝐻(𝑥) 0 (𝑥)

Proof of Theorem dihatexv Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 ∖ cdif 3900 {csn 4577 ⟨cop 4583 class class class wbr 5092 ↦ cmpt 5173 I cid 5513 ^◡ccnv 5618 ↾ cres 5621 ‘cfv 6482 ℩crio 7305 Basecbs 17120 lecple 17168 occoc 17169 0_gc0g 17343 0.cp0 18327 LModclmod 20763 LSpanclspn 20874 LSAtomsclsa 38963 OPcops 39161 Atomscatm 39252 AtLatcal 39253 HLchlt 39339 LHypclh 39973 LTrncltrn 40090 TEndoctendo 40741 DVecHcdvh 41067 DIsoHcdih 41217

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-riotaBAD 38942

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-tpos 8159 df-undef 8206 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-er 8625 df-map 8755 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-n0 12385 df-z 12472 df-uz 12736 df-fz 13411 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-sca 17177 df-vsca 17178 df-0g 17345 df-proset 18200 df-poset 18219 df-plt 18234 df-lub 18250 df-glb 18251 df-join 18252 df-meet 18253 df-p0 18329 df-p1 18330 df-lat 18338 df-clat 18405 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-submnd 18658 df-grp 18815 df-minusg 18816 df-sbg 18817 df-subg 19002 df-cntz 19196 df-lsm 19515 df-cmn 19661 df-abl 19662 df-mgp 20026 df-rng 20038 df-ur 20067 df-ring 20120 df-oppr 20222 df-dvdsr 20242 df-unit 20243 df-invr 20273 df-dvr 20286 df-drng 20616 df-lmod 20765 df-lss 20835 df-lsp 20875 df-lvec 21007 df-lsatoms 38965 df-oposet 39165 df-ol 39167 df-oml 39168 df-covers 39255 df-ats 39256 df-atl 39287 df-cvlat 39311 df-hlat 39340 df-llines 39487 df-lplanes 39488 df-lvols 39489 df-lines 39490 df-psubsp 39492 df-pmap 39493 df-padd 39785 df-lhyp 39977 df-laut 39978 df-ldil 40093 df-ltrn 40094 df-trl 40148 df-tendo 40744 df-edring 40746 df-disoa 41018 df-dvech 41068 df-dib 41128 df-dic 41162 df-dih 41218

This theorem is referenced by: dihatexv2 41328

W3C validator