dihatexv2

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

	Ref	Expression
Hypotheses	dihatexv2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dihatexv2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihatexv2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dihatexv2.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dihatexv2.o	⊢ 0 = ( 0_g ‘ 𝑈 )
	dihatexv2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	dihatexv2.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihatexv2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	dihatexv2	⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihatexv2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		dihatexv2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dihatexv2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dihatexv2.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dihatexv2.o	⊢ 0 = ( 0_g ‘ 𝑈 )
6		dihatexv2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7		dihatexv2.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
8		dihatexv2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10	9 1	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
11	10	anim2i	⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝐴 ) → ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) )
12	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		eldifi	⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) → 𝑥 ∈ 𝑉 )
14	2 3 4 6 7	dihlsprn	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑥 } ) ∈ ran 𝐼 )
15	8 13 14	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑁 ‘ { 𝑥 } ) ∈ ran 𝐼 )
16	9 2 7	dihcnvcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑥 } ) ∈ ran 𝐼 ) → ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ∈ ( Base ‘ 𝐾 ) )
17	12 15 16	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ∈ ( Base ‘ 𝐾 ) )
18		eleq1a	⊢ ( ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ∈ ( Base ‘ 𝐾 ) → ( 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) ) )
19	17 18	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) ) )
20	19	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) ) )
21	20	imdistani	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) → ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) )
22	8	adantr	⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
24	9 1 2 3 4 5 6 7 22 23	dihatexv	⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) )
25	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
26	22 13 14	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑁 ‘ { 𝑥 } ) ∈ ran 𝐼 )
27	2 7	dihcnvid2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑥 } ) ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) = ( 𝑁 ‘ { 𝑥 } ) )
28	25 26 27	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐼 ‘ ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) = ( 𝑁 ‘ { 𝑥 } ) )
29	28	eqeq2d	⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝐼 ‘ 𝑄 ) = ( 𝐼 ‘ ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) ↔ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ) )
30		simplr	⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
31	25 26 16	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ∈ ( Base ‘ 𝐾 ) )
32	9 2 7	dih11	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ 𝑄 ) = ( 𝐼 ‘ ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) ↔ 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) )
33	25 30 31 32	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝐼 ‘ 𝑄 ) = ( 𝐼 ‘ ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) ↔ 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) )
34	29 33	bitr3d	⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ↔ 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) )
35	34	rexbidva	⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 𝑥 } ) ↔ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) )
36	24 35	bitrd	⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) )
37	11 21 36	pm5.21nd	⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝑄 = ( ^◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑥 } ) ) ) )

Metamath Proof Explorer

Theorem dihatexv2

Proof