Metamath Proof Explorer

Theorem dihpN

Description: The value of isomorphism H at the fiducial atom P is determined by the vector <. 0 , S >. (the zero translation ltrnid and a nonzero member of the endomorphism ring). In particular, S can be replaced with the ring unit ` ( _I |`T ) . (Contributed by NM, 26-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihp.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihp.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihp.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihp.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
dihp.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihp.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dihp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihp.s ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) )
Assertion dihpN ( 𝜑 → ( 𝐼 ‘ 𝑃 ) = ( 𝑁 ‘ { ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 dihp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihp.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
4 dihp.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 dihp.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 dihp.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
7 dihp.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
8 dihp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
9 dihp.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
10 dihp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 dihp.s ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) )
12 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
13 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
14 2 8 10 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
15 2 3 7 8 13 10 dihat ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑃 ) ∈ ( LSAtoms ‘ 𝑈 ) )
16 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
17 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
18 16 17 2 3 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑊 ) )
19 eqid ⊢ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 )
20 1 16 17 2 4 19 ltrniotaidvalN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) = ( I ↾ 𝐵 ) )
21 10 18 20 syl2anc2 ⊢ ( 𝜑 → ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) = ( I ↾ 𝐵 ) )
22 21 fveq2d ⊢ ( 𝜑 → ( 𝑆 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) = ( 𝑆 ‘ ( I ↾ 𝐵 ) ) )
23 11 simpld ⊢ ( 𝜑 → 𝑆 ∈ 𝐸 )
24 1 2 5 tendoid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑆 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
25 10 23 24 syl2anc ⊢ ( 𝜑 → ( 𝑆 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
26 22 25 eqtr2d ⊢ ( 𝜑 → ( I ↾ 𝐵 ) = ( 𝑆 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) )
27 1 fvexi ⊢ 𝐵 ∈ V
28 resiexg ⊢ ( 𝐵 ∈ V → ( I ↾ 𝐵 ) ∈ V )
29 27 28 mp1i ⊢ ( 𝜑 → ( I ↾ 𝐵 ) ∈ V )
30 eqeq1 ⊢ ( 𝑔 = ( I ↾ 𝐵 ) → ( 𝑔 = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ↔ ( I ↾ 𝐵 ) = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ) )
31 30 anbi1d ⊢ ( 𝑔 = ( I ↾ 𝐵 ) → ( ( 𝑔 = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑠 ∈ 𝐸 ) ↔ ( ( I ↾ 𝐵 ) = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑠 ∈ 𝐸 ) ) )
32 fveq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) = ( 𝑆 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) )
33 32 eqeq2d ⊢ ( 𝑠 = 𝑆 → ( ( I ↾ 𝐵 ) = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ↔ ( I ↾ 𝐵 ) = ( 𝑆 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ) )
34 eleq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∈ 𝐸 ↔ 𝑆 ∈ 𝐸 ) )
35 33 34 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ( I ↾ 𝐵 ) = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑠 ∈ 𝐸 ) ↔ ( ( I ↾ 𝐵 ) = ( 𝑆 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑆 ∈ 𝐸 ) ) )
36 31 35 opelopabg ⊢ ( ( ( I ↾ 𝐵 ) ∈ V ∧ 𝑆 ∈ 𝐸 ) → ( ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ ∈ { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑠 ∈ 𝐸 ) } ↔ ( ( I ↾ 𝐵 ) = ( 𝑆 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑆 ∈ 𝐸 ) ) )
37 29 23 36 syl2anc ⊢ ( 𝜑 → ( ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ ∈ { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑠 ∈ 𝐸 ) } ↔ ( ( I ↾ 𝐵 ) = ( 𝑆 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑆 ∈ 𝐸 ) ) )
38 26 23 37 mpbir2and ⊢ ( 𝜑 → ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ ∈ { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑠 ∈ 𝐸 ) } )
39 eqid ⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
40 16 17 2 39 7 dihvalcqat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑃 ) = ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) )
41 10 18 40 syl2anc2 ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑃 ) = ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) )
42 16 17 2 3 4 5 39 dicval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) = { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑠 ∈ 𝐸 ) } )
43 10 18 42 syl2anc2 ⊢ ( 𝜑 → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) = { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑠 ∈ 𝐸 ) } )
44 41 43 eqtr2d ⊢ ( 𝜑 → { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 = ( 𝑠 ‘ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑃 ) ) ∧ 𝑠 ∈ 𝐸 ) } = ( 𝐼 ‘ 𝑃 ) )
45 38 44 eleqtrd ⊢ ( 𝜑 → ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑃 ) )
46 11 simprd ⊢ ( 𝜑 → 𝑆 ≠ 𝑂 )
47 1 2 4 8 12 6 dvh0g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ 𝑈 ) = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )
48 10 47 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )
49 48 eqeq2d ⊢ ( 𝜑 → ( ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ = ( 0g ‘ 𝑈 ) ↔ ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ) )
50 27 28 ax-mp ⊢ ( I ↾ 𝐵 ) ∈ V
51 4 fvexi ⊢ 𝑇 ∈ V
52 51 mptex ⊢ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ∈ V
53 6 52 eqeltri ⊢ 𝑂 ∈ V
54 50 53 opth2 ⊢ ( ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ↔ ( ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) ∧ 𝑆 = 𝑂 ) )
55 54 simprbi ⊢ ( ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ → 𝑆 = 𝑂 )
56 49 55 syl6bi ⊢ ( 𝜑 → ( ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ = ( 0g ‘ 𝑈 ) → 𝑆 = 𝑂 ) )
57 56 necon3d ⊢ ( 𝜑 → ( 𝑆 ≠ 𝑂 → ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ ≠ ( 0g ‘ 𝑈 ) ) )
58 46 57 mpd ⊢ ( 𝜑 → ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ ≠ ( 0g ‘ 𝑈 ) )
59 12 9 13 14 15 45 58 lsatel ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑃 ) = ( 𝑁 ‘ { ⟨ ( I ↾ 𝐵 ) , 𝑆 ⟩ } ) )