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 ↾ 𝐵 ) , 𝑆 ⟩ } ) )