Metamath Proof Explorer


Theorem dihopellsm

Description: Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014)

Ref Expression
Hypotheses dihopellsm.b B = Base K
dihopellsm.h H = LHyp K
dihopellsm.t T = LTrn K W
dihopellsm.e E = TEndo K W
dihopellsm.a A = v E , w E i T v i w i
dihopellsm.u U = DVecH K W
dihopellsm.l L = LSubSp U
dihopellsm.p ˙ = LSSum U
dihopellsm.i I = DIsoH K W
dihopellsm.k φ K HL W H
dihopellsm.x φ X B
dihopellsm.y φ Y B
Assertion dihopellsm φ F S I X ˙ I Y g t h u g t I X h u I Y F = g h S = t A u

Proof

Step Hyp Ref Expression
1 dihopellsm.b B = Base K
2 dihopellsm.h H = LHyp K
3 dihopellsm.t T = LTrn K W
4 dihopellsm.e E = TEndo K W
5 dihopellsm.a A = v E , w E i T v i w i
6 dihopellsm.u U = DVecH K W
7 dihopellsm.l L = LSubSp U
8 dihopellsm.p ˙ = LSSum U
9 dihopellsm.i I = DIsoH K W
10 dihopellsm.k φ K HL W H
11 dihopellsm.x φ X B
12 dihopellsm.y φ Y B
13 eqid LSubSp U = LSubSp U
14 1 2 9 6 13 dihlss K HL W H X B I X LSubSp U
15 10 11 14 syl2anc φ I X LSubSp U
16 1 2 9 6 13 dihlss K HL W H Y B I Y LSubSp U
17 10 12 16 syl2anc φ I Y LSubSp U
18 eqid + U = + U
19 2 6 18 13 8 dvhopellsm K HL W H I X LSubSp U I Y LSubSp U F S I X ˙ I Y g t h u g t I X h u I Y F S = g t + U h u
20 10 15 17 19 syl3anc φ F S I X ˙ I Y g t h u g t I X h u I Y F S = g t + U h u
21 10 adantr φ g t I X K HL W H
22 11 adantr φ g t I X X B
23 simpr φ g t I X g t I X
24 1 2 3 4 9 21 22 23 dihopcl φ g t I X g T t E
25 10 adantr φ h u I Y K HL W H
26 12 adantr φ h u I Y Y B
27 simpr φ h u I Y h u I Y
28 1 2 3 4 9 25 26 27 dihopcl φ h u I Y h T u E
29 24 28 anim12dan φ g t I X h u I Y g T t E h T u E
30 10 adantr φ g T t E h T u E K HL W H
31 simprl φ g T t E h T u E g T t E
32 simprr φ g T t E h T u E h T u E
33 2 3 4 5 6 18 dvhopvadd2 K HL W H g T t E h T u E g t + U h u = g h t A u
34 30 31 32 33 syl3anc φ g T t E h T u E g t + U h u = g h t A u
35 34 eqeq2d φ g T t E h T u E F S = g t + U h u F S = g h t A u
36 vex g V
37 vex h V
38 36 37 coex g h V
39 ovex t A u V
40 38 39 opth2 F S = g h t A u F = g h S = t A u
41 35 40 bitrdi φ g T t E h T u E F S = g t + U h u F = g h S = t A u
42 29 41 syldan φ g t I X h u I Y F S = g t + U h u F = g h S = t A u
43 42 pm5.32da φ g t I X h u I Y F S = g t + U h u g t I X h u I Y F = g h S = t A u
44 43 4exbidv φ g t h u g t I X h u I Y F S = g t + U h u g t h u g t I X h u I Y F = g h S = t A u
45 20 44 bitrd φ F S I X ˙ I Y g t h u g t I X h u I Y F = g h S = t A u