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 unity ` ( _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 \in T ⟼ {I ↾}_{B})$
	dihp.i	$⊢ I = DIsoH (K) (W)$
	dihp.u	$⊢ U = DVecH (K) (W)$
	dihp.n	$⊢ N = LSpan (U)$
	dihp.k	$⊢ φ \to (K \in HL \land W \in H)$
	dihp.s	$⊢ φ \to (S \in E \land S \neq O)$
Assertion	dihpN	$⊢ φ \to 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 \in 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	$⊢ φ \to (K \in HL \land W \in H)$
11		dihp.s	$⊢ φ \to (S \in E \land S \neq O)$
12		eqid	$⊢ 0_{U} = 0_{U}$
13		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
14	2 8 10	dvhlvec	$⊢ φ \to U \in LVec$
15	2 3 7 8 13 10	dihat	$⊢ φ \to I (P) \in LSAtoms (U)$
16		eqid	$⊢ \leq_{K} = \leq_{K}$
17		eqid	$⊢ Atoms (K) = Atoms (K)$
18	16 17 2 3	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in Atoms (K) \land \neg P \leq_{K} W)$
19		eqid	$⊢ (ι f \in T \| f (P) = P) = (ι f \in T \| f (P) = P)$
20	1 16 17 2 4 19	ltrniotaidvalN	$⊢ ((K \in HL \land W \in H) \land (P \in Atoms (K) \land \neg P \leq_{K} W)) \to (ι f \in T \| f (P) = P) = {I ↾}_{B}$
21	10 18 20	syl2anc2	$⊢ φ \to (ι f \in T \| f (P) = P) = {I ↾}_{B}$
22	21	fveq2d	$⊢ φ \to S ((ι f \in T \| f (P) = P)) = S ({I ↾}_{B})$
23	11	simpld	$⊢ φ \to S \in E$
24	1 2 5	tendoid	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S ({I ↾}_{B}) = {I ↾}_{B}$
25	10 23 24	syl2anc	$⊢ φ \to S ({I ↾}_{B}) = {I ↾}_{B}$
26	22 25	eqtr2d	$⊢ φ \to {I ↾}_{B} = S ((ι f \in T \| f (P) = P))$
27	1	fvexi	$⊢ B \in V$
28		resiexg	$⊢ B \in V \to {I ↾}_{B} \in V$
29	27 28	mp1i	$⊢ φ \to {I ↾}_{B} \in V$
30		eqeq1	$⊢ g = {I ↾}_{B} \to (g = s ((ι f \in T \| f (P) = P)) \leftrightarrow {I ↾}_{B} = s ((ι f \in T \| f (P) = P)))$
31	30	anbi1d	$⊢ g = {I ↾}_{B} \to ((g = s ((ι f \in T \| f (P) = P)) \land s \in E) \leftrightarrow ({I ↾}_{B} = s ((ι f \in T \| f (P) = P)) \land s \in E))$
32		fveq1	$⊢ s = S \to s ((ι f \in T \| f (P) = P)) = S ((ι f \in T \| f (P) = P))$
33	32	eqeq2d	$⊢ s = S \to ({I ↾}_{B} = s ((ι f \in T \| f (P) = P)) \leftrightarrow {I ↾}_{B} = S ((ι f \in T \| f (P) = P)))$
34		eleq1	$⊢ s = S \to (s \in E \leftrightarrow S \in E)$
35	33 34	anbi12d	$⊢ s = S \to (({I ↾}_{B} = s ((ι f \in T \| f (P) = P)) \land s \in E) \leftrightarrow ({I ↾}_{B} = S ((ι f \in T \| f (P) = P)) \land S \in E))$
36	31 35	opelopabg	$⊢ ({I ↾}_{B} \in V \land S \in E) \to (⟨{I ↾}_{B}, S⟩ \in \{⟨g, s⟩ \| (g = s ((ι f \in T \| f (P) = P)) \land s \in E)\} \leftrightarrow ({I ↾}_{B} = S ((ι f \in T \| f (P) = P)) \land S \in E))$
37	29 23 36	syl2anc	$⊢ φ \to (⟨{I ↾}_{B}, S⟩ \in \{⟨g, s⟩ \| (g = s ((ι f \in T \| f (P) = P)) \land s \in E)\} \leftrightarrow ({I ↾}_{B} = S ((ι f \in T \| f (P) = P)) \land S \in E))$
38	26 23 37	mpbir2and	$⊢ φ \to ⟨{I ↾}_{B}, S⟩ \in \{⟨g, s⟩ \| (g = s ((ι f \in T \| f (P) = P)) \land s \in E)\}$
39		eqid	$⊢ DIsoC (K) (W) = DIsoC (K) (W)$
40	16 17 2 39 7	dihvalcqat	$⊢ ((K \in HL \land W \in H) \land (P \in Atoms (K) \land \neg P \leq_{K} W)) \to I (P) = DIsoC (K) (W) (P)$
41	10 18 40	syl2anc2	$⊢ φ \to I (P) = DIsoC (K) (W) (P)$
42	16 17 2 3 4 5 39	dicval	$⊢ ((K \in HL \land W \in H) \land (P \in Atoms (K) \land \neg P \leq_{K} W)) \to DIsoC (K) (W) (P) = \{⟨g, s⟩ \| (g = s ((ι f \in T \| f (P) = P)) \land s \in E)\}$
43	10 18 42	syl2anc2	$⊢ φ \to DIsoC (K) (W) (P) = \{⟨g, s⟩ \| (g = s ((ι f \in T \| f (P) = P)) \land s \in E)\}$
44	41 43	eqtr2d	$⊢ φ \to \{⟨g, s⟩ \| (g = s ((ι f \in T \| f (P) = P)) \land s \in E)\} = I (P)$
45	38 44	eleqtrd	$⊢ φ \to ⟨{I ↾}_{B}, S⟩ \in I (P)$
46	11	simprd	$⊢ φ \to S \neq O$
47	1 2 4 8 12 6	dvh0g	$⊢ (K \in HL \land W \in H) \to 0_{U} = ⟨{I ↾}_{B}, O⟩$
48	10 47	syl	$⊢ φ \to 0_{U} = ⟨{I ↾}_{B}, O⟩$
49	48	eqeq2d	$⊢ φ \to (⟨{I ↾}_{B}, S⟩ = 0_{U} \leftrightarrow ⟨{I ↾}_{B}, S⟩ = ⟨{I ↾}_{B}, O⟩)$
50	27 28	ax-mp	$⊢ {I ↾}_{B} \in V$
51	4	fvexi	$⊢ T \in V$
52	51	mptex	$⊢ (f \in T ⟼ {I ↾}_{B}) \in V$
53	6 52	eqeltri	$⊢ O \in V$
54	50 53	opth2	$⊢ ⟨{I ↾}_{B}, S⟩ = ⟨{I ↾}_{B}, O⟩ \leftrightarrow ({I ↾}_{B} = {I ↾}_{B} \land S = O)$
55	54	simprbi	$⊢ ⟨{I ↾}_{B}, S⟩ = ⟨{I ↾}_{B}, O⟩ \to S = O$
56	49 55	syl6bi	$⊢ φ \to (⟨{I ↾}_{B}, S⟩ = 0_{U} \to S = O)$
57	56	necon3d	$⊢ φ \to (S \neq O \to ⟨{I ↾}_{B}, S⟩ \neq 0_{U})$
58	46 57	mpd	$⊢ φ \to ⟨{I ↾}_{B}, S⟩ \neq 0_{U}$
59	12 9 13 14 15 45 58	lsatel	$⊢ φ \to I (P) = N (\{⟨{I ↾}_{B}, S⟩\})$

Metamath Proof Explorer

Theorem dihpN

Proof