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 ↾ 𝑇 ) ⟩ ) ) )