Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
dvhop.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvhop.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvhop.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dvhop.p ⊢ 𝑃 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) )
dvhop.a ⊢ 𝐴 = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ( 2nd ‘ 𝑓 ) 𝑃 ( 2nd ‘ 𝑔 ) ) ⟩ )
dvhop.s ⊢ 𝑆 = ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
dvhop.o ⊢ 𝑂 = ( 𝑐 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion dvhopN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ⟨ 𝐹 , 𝑈 ⟩ = ( ⟨ 𝐹 , 𝑂 ⟩ 𝐴 ( 𝑈 𝑆 ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 dvhop.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dvhop.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dvhop.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 dvhop.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 dvhop.p ⊢ 𝑃 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) )
6 dvhop.a ⊢ 𝐴 = ( 𝑓 ∈ ( 𝑇 × 𝐸 ) , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( ( 1st ‘ 𝑓 ) ∘ ( 1st ‘ 𝑔 ) ) , ( ( 2nd ‘ 𝑓 ) 𝑃 ( 2nd ‘ 𝑔 ) ) ⟩ )
7 dvhop.s ⊢ 𝑆 = ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ ⟨ ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) ⟩ )
8 dvhop.o ⊢ 𝑂 = ( 𝑐 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
9 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → 𝑈 ∈ 𝐸 )
10 1 2 3 idltrn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
11 10 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
12 2 3 4 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
13 12 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
14 7 dvhopspN ⊢ ( ( 𝑈 ∈ 𝐸 ∧ ( ( I ↾ 𝐵 ) ∈ 𝑇 ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) ) → ( 𝑈 𝑆 ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ) = ⟨ ( 𝑈 ‘ ( I ↾ 𝐵 ) ) , ( 𝑈 ∘ ( I ↾ 𝑇 ) ) ⟩ )
15 9 11 13 14 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝑈 𝑆 ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ) = ⟨ ( 𝑈 ‘ ( I ↾ 𝐵 ) ) , ( 𝑈 ∘ ( I ↾ 𝑇 ) ) ⟩ )
16 1 2 4 tendoid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) → ( 𝑈 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
17 16 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝑈 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
18 2 3 4 tendo1mulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) → ( 𝑈 ∘ ( I ↾ 𝑇 ) ) = 𝑈 )
19 18 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝑈 ∘ ( I ↾ 𝑇 ) ) = 𝑈 )
20 17 19 opeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ⟨ ( 𝑈 ‘ ( I ↾ 𝐵 ) ) , ( 𝑈 ∘ ( I ↾ 𝑇 ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , 𝑈 ⟩ )
21 15 20 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝑈 𝑆 ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ) = ⟨ ( I ↾ 𝐵 ) , 𝑈 ⟩ )
22 21 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( ⟨ 𝐹 , 𝑂 ⟩ 𝐴 ( 𝑈 𝑆 ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ) ) = ( ⟨ 𝐹 , 𝑂 ⟩ 𝐴 ⟨ ( I ↾ 𝐵 ) , 𝑈 ⟩ ) )
23 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → 𝐹 ∈ 𝑇 )
24 1 2 3 4 8 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ 𝐸 )
25 24 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → 𝑂 ∈ 𝐸 )
26 6 dvhopaddN ⊢ ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑂 ∈ 𝐸 ) ∧ ( ( I ↾ 𝐵 ) ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( ⟨ 𝐹 , 𝑂 ⟩ 𝐴 ⟨ ( I ↾ 𝐵 ) , 𝑈 ⟩ ) = ⟨ ( 𝐹 ∘ ( I ↾ 𝐵 ) ) , ( 𝑂 𝑃 𝑈 ) ⟩ )
27 23 25 11 9 26 syl22anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( ⟨ 𝐹 , 𝑂 ⟩ 𝐴 ⟨ ( I ↾ 𝐵 ) , 𝑈 ⟩ ) = ⟨ ( 𝐹 ∘ ( I ↾ 𝐵 ) ) , ( 𝑂 𝑃 𝑈 ) ⟩ )
28 1 2 3 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
29 28 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
30 f1of ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → 𝐹 : 𝐵 ⟶ 𝐵 )
31 fcoi1 ⊢ ( 𝐹 : 𝐵 ⟶ 𝐵 → ( 𝐹 ∘ ( I ↾ 𝐵 ) ) = 𝐹 )
32 29 30 31 3syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝐹 ∘ ( I ↾ 𝐵 ) ) = 𝐹 )
33 1 2 3 4 8 5 tendo0pl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ) → ( 𝑂 𝑃 𝑈 ) = 𝑈 )
34 33 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝑂 𝑃 𝑈 ) = 𝑈 )
35 32 34 opeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ⟨ ( 𝐹 ∘ ( I ↾ 𝐵 ) ) , ( 𝑂 𝑃 𝑈 ) ⟩ = ⟨ 𝐹 , 𝑈 ⟩ )
36 22 27 35 3eqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ⟨ 𝐹 , 𝑈 ⟩ = ( ⟨ 𝐹 , 𝑂 ⟩ 𝐴 ( 𝑈 𝑆 ⟨ ( I ↾ 𝐵 ) , ( I ↾ 𝑇 ) ⟩ ) ) )