dvhopN

Description: Decompose a DVecH vector expressed as an ordered pair into the sum of two components, the first from the translation group vector base of DVecA and the other from the one-dimensional vector subspace E . Part of Lemma M of Crawley p. 121, line 18. We represent their e, sigma, f by ` <. (I |`` B ) , ( I |`T ) >. , U , <. F , O >. . We swapped the order of vector sum (their juxtaposition i.e. composition) to show <. F , O >. first. Note that O and ` (I |`T ) are the zero and one of the division ring E , and ` ( I |`B ) is the zero of the translation group. S is the scalar product. (Contributed by NM, 21-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvhop.b	$⊢ B = {Base}_{K}$
	dvhop.h	$⊢ H = LHyp (K)$
	dvhop.t	$⊢ T = LTrn (K) (W)$
	dvhop.e	$⊢ E = TEndo (K) (W)$
	dvhop.p	$⊢ P = (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c)))$
	dvhop.a	$⊢ A = (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) P 2^{nd} (g)⟩)$
	dvhop.s	$⊢ S = (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
	dvhop.o	$⊢ O = (c \in T ⟼ {I ↾}_{B})$
Assertion	dvhopN	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to ⟨F, U⟩ = ⟨F, O⟩ A (U S ⟨{I ↾}_{B}, {I ↾}_{T}⟩)$

Proof

Step	Hyp	Ref	Expression
1		dvhop.b	$⊢ B = {Base}_{K}$
2		dvhop.h	$⊢ H = LHyp (K)$
3		dvhop.t	$⊢ T = LTrn (K) (W)$
4		dvhop.e	$⊢ E = TEndo (K) (W)$
5		dvhop.p	$⊢ P = (a \in E, b \in E ⟼ (c \in T ⟼ a (c) \circ b (c)))$
6		dvhop.a	$⊢ A = (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), 2^{nd} (f) P 2^{nd} (g)⟩)$
7		dvhop.s	$⊢ S = (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
8		dvhop.o	$⊢ O = (c \in T ⟼ {I ↾}_{B})$
9		simprr	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to U \in E$
10	1 2 3	idltrn	$⊢ (K \in HL \land W \in H) \to {I ↾}_{B} \in T$
11	10	adantr	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to {I ↾}_{B} \in T$
12	2 3 4	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in E$
13	12	adantr	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to {I ↾}_{T} \in E$
14	7	dvhopspN	$⊢ (U \in E \land ({I ↾}_{B} \in T \land {I ↾}_{T} \in E)) \to U S ⟨{I ↾}_{B}, {I ↾}_{T}⟩ = ⟨U ({I ↾}_{B}), U \circ ({I ↾}_{T})⟩$
15	9 11 13 14	syl12anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to U S ⟨{I ↾}_{B}, {I ↾}_{T}⟩ = ⟨U ({I ↾}_{B}), U \circ ({I ↾}_{T})⟩$
16	1 2 4	tendoid	$⊢ ((K \in HL \land W \in H) \land U \in E) \to U ({I ↾}_{B}) = {I ↾}_{B}$
17	16	adantrl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to U ({I ↾}_{B}) = {I ↾}_{B}$
18	2 3 4	tendo1mulr	$⊢ ((K \in HL \land W \in H) \land U \in E) \to U \circ ({I ↾}_{T}) = U$
19	18	adantrl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to U \circ ({I ↾}_{T}) = U$
20	17 19	opeq12d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to ⟨U ({I ↾}_{B}), U \circ ({I ↾}_{T})⟩ = ⟨{I ↾}_{B}, U⟩$
21	15 20	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to U S ⟨{I ↾}_{B}, {I ↾}_{T}⟩ = ⟨{I ↾}_{B}, U⟩$
22	21	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to ⟨F, O⟩ A (U S ⟨{I ↾}_{B}, {I ↾}_{T}⟩) = ⟨F, O⟩ A ⟨{I ↾}_{B}, U⟩$
23		simprl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to F \in T$
24	1 2 3 4 8	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
25	24	adantr	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to O \in E$
26	6	dvhopaddN	$⊢ ((F \in T \land O \in E) \land ({I ↾}_{B} \in T \land U \in E)) \to ⟨F, O⟩ A ⟨{I ↾}_{B}, U⟩ = ⟨F \circ ({I ↾}_{B}), O P U⟩$
27	23 25 11 9 26	syl22anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to ⟨F, O⟩ A ⟨{I ↾}_{B}, U⟩ = ⟨F \circ ({I ↾}_{B}), O P U⟩$
28	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
29	28	adantrr	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to F : B \underset{1-1 onto}{⟶} B$
30		f1of	$⊢ F : B \underset{1-1 onto}{⟶} B \to F : B ⟶ B$
31		fcoi1	$⊢ F : B ⟶ B \to F \circ ({I ↾}_{B}) = F$
32	29 30 31	3syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to F \circ ({I ↾}_{B}) = F$
33	1 2 3 4 8 5	tendo0pl	$⊢ ((K \in HL \land W \in H) \land U \in E) \to O P U = U$
34	33	adantrl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to O P U = U$
35	32 34	opeq12d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to ⟨F \circ ({I ↾}_{B}), O P U⟩ = ⟨F, U⟩$
36	22 27 35	3eqtrrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land U \in E)) \to ⟨F, U⟩ = ⟨F, O⟩ A (U S ⟨{I ↾}_{B}, {I ↾}_{T}⟩)$

Metamath Proof Explorer

Theorem dvhopN

Proof