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 ⊢ B = Base K
dihp.h ⊢ H = LHyp ⁡ K
dihp.p ⊢ P = oc ⁡ K ⁡ W
dihp.t ⊢ T = LTrn ⁡ K ⁡ W
dihp.e ⊢ E = TEndo ⁡ K ⁡ W
dihp.o ⊢ O = f ∈ T ⟼ I ↾ B
dihp.i ⊢ I = DIsoH ⁡ K ⁡ W
dihp.u ⊢ U = DVecH ⁡ K ⁡ W
dihp.n ⊢ N = LSpan ⁡ U
dihp.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihp.s ⊢ φ → S ∈ E ∧ S ≠ O
Assertion dihpN ⊢ φ → I ⁡ P = N ⁡ I ↾ B S

Proof

Step Hyp Ref Expression
1 dihp.b ⊢ B = Base K
2 dihp.h ⊢ H = LHyp ⁡ K
3 dihp.p ⊢ P = oc ⁡ K ⁡ W
4 dihp.t ⊢ T = LTrn ⁡ K ⁡ W
5 dihp.e ⊢ E = TEndo ⁡ K ⁡ W
6 dihp.o ⊢ O = f ∈ T ⟼ I ↾ B
7 dihp.i ⊢ I = DIsoH ⁡ K ⁡ W
8 dihp.u ⊢ U = DVecH ⁡ K ⁡ W
9 dihp.n ⊢ N = LSpan ⁡ U
10 dihp.k ⊢ φ → K ∈ HL ∧ W ∈ H
11 dihp.s ⊢ φ → S ∈ E ∧ S ≠ O
12 eqid ⊢ 0 U = 0 U
13 eqid ⊢ LSAtoms ⁡ U = LSAtoms ⁡ U
14 2 8 10 dvhlvec ⊢ φ → U ∈ LVec
15 2 3 7 8 13 10 dihat ⊢ φ → I ⁡ P ∈ LSAtoms ⁡ U
16 eqid ⊢ ≤ K = ≤ K
17 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
18 16 17 2 3 lhpocnel2 ⊢ K ∈ HL ∧ W ∈ H → P ∈ Atoms ⁡ K ∧ ¬ P ≤ K W
19 eqid ⊢ ι f ∈ T | f ⁡ P = P = ι f ∈ T | f ⁡ P = P
20 1 16 17 2 4 19 ltrniotaidvalN ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ Atoms ⁡ K ∧ ¬ P ≤ K W → ι f ∈ T | f ⁡ P = P = I ↾ B
21 10 18 20 syl2anc2 ⊢ φ → ι f ∈ T | f ⁡ P = P = I ↾ B
22 21 fveq2d ⊢ φ → S ⁡ ι f ∈ T | f ⁡ P = P = S ⁡ I ↾ B
23 11 simpld ⊢ φ → S ∈ E
24 1 2 5 tendoid ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E → S ⁡ I ↾ B = I ↾ B
25 10 23 24 syl2anc ⊢ φ → S ⁡ I ↾ B = I ↾ B
26 22 25 eqtr2d ⊢ φ → I ↾ B = S ⁡ ι f ∈ T | f ⁡ P = P
27 1 fvexi ⊢ B ∈ V
28 resiexg ⊢ B ∈ V → I ↾ B ∈ V
29 27 28 mp1i ⊢ φ → I ↾ B ∈ V
30 eqeq1 ⊢ g = I ↾ B → g = s ⁡ ι f ∈ T | f ⁡ P = P ↔ I ↾ B = s ⁡ ι f ∈ T | f ⁡ P = P
31 30 anbi1d ⊢ g = I ↾ B → g = s ⁡ ι f ∈ T | f ⁡ P = P ∧ s ∈ E ↔ I ↾ B = s ⁡ ι f ∈ T | f ⁡ P = P ∧ s ∈ E
32 fveq1 ⊢ s = S → s ⁡ ι f ∈ T | f ⁡ P = P = S ⁡ ι f ∈ T | f ⁡ P = P
33 32 eqeq2d ⊢ s = S → I ↾ B = s ⁡ ι f ∈ T | f ⁡ P = P ↔ I ↾ B = S ⁡ ι f ∈ T | f ⁡ P = P
34 eleq1 ⊢ s = S → s ∈ E ↔ S ∈ E
35 33 34 anbi12d ⊢ s = S → I ↾ B = s ⁡ ι f ∈ T | f ⁡ P = P ∧ s ∈ E ↔ I ↾ B = S ⁡ ι f ∈ T | f ⁡ P = P ∧ S ∈ E
36 31 35 opelopabg ⊢ I ↾ B ∈ V ∧ S ∈ E → I ↾ B S ∈ g s | g = s ⁡ ι f ∈ T | f ⁡ P = P ∧ s ∈ E ↔ I ↾ B = S ⁡ ι f ∈ T | f ⁡ P = P ∧ S ∈ E
37 29 23 36 syl2anc ⊢ φ → I ↾ B S ∈ g s | g = s ⁡ ι f ∈ T | f ⁡ P = P ∧ s ∈ E ↔ I ↾ B = S ⁡ ι f ∈ T | f ⁡ P = P ∧ S ∈ E
38 26 23 37 mpbir2and ⊢ φ → I ↾ B S ∈ g s | g = s ⁡ ι f ∈ T | f ⁡ P = P ∧ s ∈ E
39 eqid ⊢ DIsoC ⁡ K ⁡ W = DIsoC ⁡ K ⁡ W
40 16 17 2 39 7 dihvalcqat ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ Atoms ⁡ K ∧ ¬ P ≤ K W → I ⁡ P = DIsoC ⁡ K ⁡ W ⁡ P
41 10 18 40 syl2anc2 ⊢ φ → I ⁡ P = DIsoC ⁡ K ⁡ W ⁡ P
42 16 17 2 3 4 5 39 dicval ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ Atoms ⁡ K ∧ ¬ P ≤ K W → DIsoC ⁡ K ⁡ W ⁡ P = g s | g = s ⁡ ι f ∈ T | f ⁡ P = P ∧ s ∈ E
43 10 18 42 syl2anc2 ⊢ φ → DIsoC ⁡ K ⁡ W ⁡ P = g s | g = s ⁡ ι f ∈ T | f ⁡ P = P ∧ s ∈ E
44 41 43 eqtr2d ⊢ φ → g s | g = s ⁡ ι f ∈ T | f ⁡ P = P ∧ s ∈ E = I ⁡ P
45 38 44 eleqtrd ⊢ φ → I ↾ B S ∈ I ⁡ P
46 11 simprd ⊢ φ → S ≠ O
47 1 2 4 8 12 6 dvh0g ⊢ K ∈ HL ∧ W ∈ H → 0 U = I ↾ B O
48 10 47 syl ⊢ φ → 0 U = I ↾ B O
49 48 eqeq2d ⊢ φ → I ↾ B S = 0 U ↔ I ↾ B S = I ↾ B O
50 27 28 ax-mp ⊢ I ↾ B ∈ V
51 4 fvexi ⊢ T ∈ V
52 51 mptex ⊢ f ∈ T ⟼ I ↾ B ∈ V
53 6 52 eqeltri ⊢ O ∈ V
54 50 53 opth2 ⊢ I ↾ B S = I ↾ B O ↔ I ↾ B = I ↾ B ∧ S = O
55 54 simprbi ⊢ I ↾ B S = I ↾ B O → S = O
56 49 55 syl6bi ⊢ φ → I ↾ B S = 0 U → S = O
57 56 necon3d ⊢ φ → S ≠ O → I ↾ B S ≠ 0 U
58 46 57 mpd ⊢ φ → I ↾ B S ≠ 0 U
59 12 9 13 14 15 45 58 lsatel ⊢ φ → I ⁡ P = N ⁡ I ↾ B S