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 41537

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 2734	. . . . . . . . 9 ⊢ (le‘𝐾) = (le‘𝐾)
7		dihatexv.a	. . . . . . . . 9 ⊢ 𝐴 = (Atoms‘𝐾)
8		dihatexv.h	. . . . . . . . 9 ⊢ 𝐻 = (LHyp‘𝐾)
9		eqid 2734	. . . . . . . . 9 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
10		eqid 2734	. . . . . . . . 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 41440	. . . . . . . 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 2734	. . . . . . . . . . . . . 14 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
19	5, 8, 9, 18, 10	tendo0cl 40989	. . . . . . . . . . . . 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 41287	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊))) → ⟨𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))⟩ ∈ 𝑉)
23	16, 17, 20, 22	syl12anc 836	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) ∧ 𝑔 ∈ ((LTrn‘𝐾)‘𝑊)) → ⟨𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))⟩ ∈ 𝑉)
24		sneq 4588	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))⟩ → {𝑥} = {⟨𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))⟩})
25	24	fveq2d 6836	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))⟩ → (𝑁‘{𝑥}) = (𝑁‘{⟨𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))⟩}))
26	25	rspceeqv 3597	. . . . . . . . . . 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 3135	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) → (∃𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔 ≠ ( I ↾ 𝐵) ∧ (𝐼‘𝑄) = (𝑁‘{⟨𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))⟩})) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥})))
31	15, 30	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥}))
32	1	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
33		eqid 2734	. . . . . . . . . . 11 ⊢ ((oc‘𝐾)‘𝑊) = ((oc‘𝐾)‘𝑊)
34	6, 7, 8, 33	lhpocnel2 40218	. . . . . . . . . 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 2734	. . . . . . . . . 10 ⊢ (℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) = (℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄)
39	6, 7, 8, 9, 38	ltrniotacl 40778	. . . . . . . . 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 40968	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ ((LTrn‘𝐾)‘𝑊)) ∈ ((TEndo‘𝐾)‘𝑊))
42	32, 41	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → ( I ↾ ((LTrn‘𝐾)‘𝑊)) ∈ ((TEndo‘𝐾)‘𝑊))
43	8, 9, 18, 11, 21	dvhelvbasei 41287	. . . . . . . 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 41441	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐼‘𝑄) = (𝑁‘{⟨(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩}))
46	32, 36, 37, 45	syl12anc 836	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (𝐼‘𝑄) = (𝑁‘{⟨(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩}))
47		sneq 4588	. . . . . . . . 9 ⊢ (𝑥 = ⟨(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ → {𝑥} = {⟨(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩})
48	47	fveq2d 6836	. . . . . . . 8 ⊢ (𝑥 = ⟨(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ → (𝑁‘{𝑥}) = (𝑁‘{⟨(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩}))
49	48	rspceeqv 3597	. . . . . . 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 39559	. . . . . . . . . . 11 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
55	53, 54	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝐾 ∈ AtLat)
56		simpllr 775	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝑄 ∈ 𝐴)
57		eqid 2734	. . . . . . . . . . 11 ⊢ (0.‘𝐾) = (0.‘𝐾)
58	57, 7	atn0 39507	. . . . . . . . . 10 ⊢ ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴) → 𝑄 ≠ (0.‘𝐾))
59	55, 56, 58	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝑄 ≠ (0.‘𝐾))
60		sneq 4588	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → {𝑥} = { 0 })
61	60	fveq2d 6836	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (𝑁‘{𝑥}) = (𝑁‘{ 0 }))
62	61	3ad2ant3 1135	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝑁‘{𝑥}) = (𝑁‘{ 0 }))
63		simp1ll 1237	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → 𝜑)
64	8, 11, 1	dvhlmod 41309	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ∈ LMod)
65		dihatexv.o	. . . . . . . . . . . . . . . 16 ⊢ 0 = (0_g‘𝑈)
66	65, 13	lspsn0 20957	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ LMod → (𝑁‘{ 0 }) = { 0 })
67	63, 64, 66	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝑁‘{ 0 }) = { 0 })
68	62, 67	eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝑁‘{𝑥}) = { 0 })
69		simp2 1137	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝐼‘𝑄) = (𝑁‘{𝑥}))
70	57, 8, 12, 11, 65	dih0 41479	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐼‘(0.‘𝐾)) = { 0 })
71	63, 1, 70	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝐼‘(0.‘𝐾)) = { 0 })
72	68, 69, 71	3eqtr4d 2779	. . . . . . . . . . . 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 39561	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
78	5, 57	op0cl 39383	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ OP → (0.‘𝐾) ∈ 𝐵)
79	76, 77, 78	3syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (0.‘𝐾) ∈ 𝐵)
80	5, 8, 12	dih11 41464	. . . . . . . . . . . . 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 2951	. . . . . . . . 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 3147	. . . . 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 41471	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐵) → (^◡𝐼‘(𝐼‘𝑄)) = 𝑄)
94	91, 92, 93	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → (^◡𝐼‘(𝐼‘𝑄)) = 𝑄)
95		fveq2 6832	. . . . . . . 8 ⊢ ((𝐼‘𝑄) = (𝑁‘{𝑥}) → (^◡𝐼‘(𝐼‘𝑄)) = (^◡𝐼‘(𝑁‘{𝑥})))
96	95	ad2antll 729	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → (^◡𝐼‘(𝐼‘𝑄)) = (^◡𝐼‘(𝑁‘{𝑥})))
97	94, 96	eqtr3d 2771	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑄 = (^◡𝐼‘(𝑁‘{𝑥})))
98	64	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑈 ∈ LMod)
99		simplr 768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑥 ∈ 𝑉)
100		simprl 770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑥 ≠ 0 )
101		eqid 2734	. . . . . . . . 9 ⊢ (LSAtoms‘𝑈) = (LSAtoms‘𝑈)
102	21, 13, 65, 101	lsatlspsn2 39191	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) → (𝑁‘{𝑥}) ∈ (LSAtoms‘𝑈))
103	98, 99, 100, 102	syl3anc 1373	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → (𝑁‘{𝑥}) ∈ (LSAtoms‘𝑈))
104	7, 8, 11, 12, 101	dihlatat 41536	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑥}) ∈ (LSAtoms‘𝑈)) → (^◡𝐼‘(𝑁‘{𝑥})) ∈ 𝐴)
105	91, 103, 104	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → (^◡𝐼‘(𝑁‘{𝑥})) ∈ 𝐴)
106	97, 105	eqeltrd 2834	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑄 ∈ 𝐴)
107	106	ex 412	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝑄 ∈ 𝐴))
108	107	rexlimdva 3135	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝑄 ∈ 𝐴))
109	90, 108	impbid 212	. 2 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝑉 (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))))
110		rexdifsn 4748	. 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 1541 ∈ wcel 2113 ≠ wne 2930 ∃wrex 3058 ∖ cdif 3896 {csn 4578 ⟨cop 4584 class class class wbr 5096 ↦ cmpt 5177 I cid 5516 ^◡ccnv 5621 ↾ cres 5624 ‘cfv 6490 ℩crio 7312 Basecbs 17134 lecple 17182 occoc 17183 0_gc0g 17357 0.cp0 18342 LModclmod 20809 LSpanclspn 20920 LSAtomsclsa 39173 OPcops 39371 Atomscatm 39462 AtLatcal 39463 HLchlt 39549 LHypclh 40183 LTrncltrn 40300 TEndoctendo 40951 DVecHcdvh 41277 DIsoHcdih 41427

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101 ax-riotaBAD 39152

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-tp 4583 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-iin 4947 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-tpos 8166 df-undef 8213 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-map 8763 df-en 8882 df-dom 8883 df-sdom 8884 df-fin 8885 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-nn 12144 df-2 12206 df-3 12207 df-4 12208 df-5 12209 df-6 12210 df-n0 12400 df-z 12487 df-uz 12750 df-fz 13422 df-struct 17072 df-sets 17089 df-slot 17107 df-ndx 17119 df-base 17135 df-ress 17156 df-plusg 17188 df-mulr 17189 df-sca 17191 df-vsca 17192 df-0g 17359 df-proset 18215 df-poset 18234 df-plt 18249 df-lub 18265 df-glb 18266 df-join 18267 df-meet 18268 df-p0 18344 df-p1 18345 df-lat 18353 df-clat 18420 df-mgm 18563 df-sgrp 18642 df-mnd 18658 df-submnd 18707 df-grp 18864 df-minusg 18865 df-sbg 18866 df-subg 19051 df-cntz 19244 df-lsm 19563 df-cmn 19709 df-abl 19710 df-mgp 20074 df-rng 20086 df-ur 20115 df-ring 20168 df-oppr 20271 df-dvdsr 20291 df-unit 20292 df-invr 20322 df-dvr 20335 df-drng 20662 df-lmod 20811 df-lss 20881 df-lsp 20921 df-lvec 21053 df-lsatoms 39175 df-oposet 39375 df-ol 39377 df-oml 39378 df-covers 39465 df-ats 39466 df-atl 39497 df-cvlat 39521 df-hlat 39550 df-llines 39697 df-lplanes 39698 df-lvols 39699 df-lines 39700 df-psubsp 39702 df-pmap 39703 df-padd 39995 df-lhyp 40187 df-laut 40188 df-ldil 40303 df-ltrn 40304 df-trl 40358 df-tendo 40954 df-edring 40956 df-disoa 41228 df-dvech 41278 df-dib 41338 df-dic 41372 df-dih 41428

This theorem is referenced by: dihatexv2 41538

W3C validator