Metamath Proof Explorer


Theorem diblsmopel

Description: Membership in subspace sum for partial isomorphism B. (Contributed by NM, 21-Sep-2014) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses diblsmopel.b B = Base K
diblsmopel.l ˙ = K
diblsmopel.h H = LHyp K
diblsmopel.t T = LTrn K W
diblsmopel.o O = f T I B
diblsmopel.v V = DVecA K W
diblsmopel.u U = DVecH K W
diblsmopel.q ˙ = LSSum V
diblsmopel.p ˙ = LSSum U
diblsmopel.j J = DIsoA K W
diblsmopel.i I = DIsoB K W
diblsmopel.k φ K HL W H
diblsmopel.x φ X B X ˙ W
diblsmopel.y φ Y B Y ˙ W
Assertion diblsmopel φ F S I X ˙ I Y F J X ˙ J Y S = O

Proof

Step Hyp Ref Expression
1 diblsmopel.b B = Base K
2 diblsmopel.l ˙ = K
3 diblsmopel.h H = LHyp K
4 diblsmopel.t T = LTrn K W
5 diblsmopel.o O = f T I B
6 diblsmopel.v V = DVecA K W
7 diblsmopel.u U = DVecH K W
8 diblsmopel.q ˙ = LSSum V
9 diblsmopel.p ˙ = LSSum U
10 diblsmopel.j J = DIsoA K W
11 diblsmopel.i I = DIsoB K W
12 diblsmopel.k φ K HL W H
13 diblsmopel.x φ X B X ˙ W
14 diblsmopel.y φ Y B Y ˙ W
15 eqid LSubSp U = LSubSp U
16 1 2 3 7 11 15 diblss K HL W H X B X ˙ W I X LSubSp U
17 12 13 16 syl2anc φ I X LSubSp U
18 1 2 3 7 11 15 diblss K HL W H Y B Y ˙ W I Y LSubSp U
19 12 14 18 syl2anc φ I Y LSubSp U
20 eqid + U = + U
21 3 7 20 15 9 dvhopellsm K HL W H I X LSubSp U I Y LSubSp U F S I X ˙ I Y x y z w x y I X z w I Y F S = x y + U z w
22 12 17 19 21 syl3anc φ F S I X ˙ I Y x y z w x y I X z w I Y F S = x y + U z w
23 excom y z w x y I X z w I Y F S = x y + U z w z y w x y I X z w I Y F S = x y + U z w
24 1 2 3 4 5 10 11 dibopelval2 K HL W H X B X ˙ W x y I X x J X y = O
25 12 13 24 syl2anc φ x y I X x J X y = O
26 1 2 3 4 5 10 11 dibopelval2 K HL W H Y B Y ˙ W z w I Y z J Y w = O
27 12 14 26 syl2anc φ z w I Y z J Y w = O
28 25 27 anbi12d φ x y I X z w I Y x J X y = O z J Y w = O
29 an4 x J X y = O z J Y w = O x J X z J Y y = O w = O
30 ancom x J X z J Y y = O w = O y = O w = O x J X z J Y
31 29 30 bitri x J X y = O z J Y w = O y = O w = O x J X z J Y
32 28 31 bitrdi φ x y I X z w I Y y = O w = O x J X z J Y
33 32 anbi1d φ x y I X z w I Y F S = x y + U z w y = O w = O x J X z J Y F S = x y + U z w
34 anass y = O w = O x J X z J Y F S = x y + U z w y = O w = O x J X z J Y F S = x y + U z w
35 df-3an y = O w = O x J X z J Y F S = x y + U z w y = O w = O x J X z J Y F S = x y + U z w
36 34 35 bitr4i y = O w = O x J X z J Y F S = x y + U z w y = O w = O x J X z J Y F S = x y + U z w
37 33 36 bitrdi φ x y I X z w I Y F S = x y + U z w y = O w = O x J X z J Y F S = x y + U z w
38 37 2exbidv φ y w x y I X z w I Y F S = x y + U z w y w y = O w = O x J X z J Y F S = x y + U z w
39 4 fvexi T V
40 39 mptex f T I B V
41 5 40 eqeltri O V
42 opeq2 y = O x y = x O
43 42 oveq1d y = O x y + U z w = x O + U z w
44 43 eqeq2d y = O F S = x y + U z w F S = x O + U z w
45 44 anbi2d y = O x J X z J Y F S = x y + U z w x J X z J Y F S = x O + U z w
46 opeq2 w = O z w = z O
47 46 oveq2d w = O x O + U z w = x O + U z O
48 47 eqeq2d w = O F S = x O + U z w F S = x O + U z O
49 48 anbi2d w = O x J X z J Y F S = x O + U z w x J X z J Y F S = x O + U z O
50 41 41 45 49 ceqsex2v y w y = O w = O x J X z J Y F S = x y + U z w x J X z J Y F S = x O + U z O
51 12 adantr φ x J X z J Y K HL W H
52 13 adantr φ x J X z J Y X B X ˙ W
53 simprl φ x J X z J Y x J X
54 1 2 3 4 10 diael K HL W H X B X ˙ W x J X x T
55 51 52 53 54 syl3anc φ x J X z J Y x T
56 eqid TEndo K W = TEndo K W
57 1 3 4 56 5 tendo0cl K HL W H O TEndo K W
58 51 57 syl φ x J X z J Y O TEndo K W
59 14 adantr φ x J X z J Y Y B Y ˙ W
60 simprr φ x J X z J Y z J Y
61 1 2 3 4 10 diael K HL W H Y B Y ˙ W z J Y z T
62 51 59 60 61 syl3anc φ x J X z J Y z T
63 eqid Scalar U = Scalar U
64 eqid + Scalar U = + Scalar U
65 3 4 56 7 63 20 64 dvhopvadd K HL W H x T O TEndo K W z T O TEndo K W x O + U z O = x z O + Scalar U O
66 51 55 58 62 58 65 syl122anc φ x J X z J Y x O + U z O = x z O + Scalar U O
67 66 eqeq2d φ x J X z J Y F S = x O + U z O F S = x z O + Scalar U O
68 vex x V
69 vex z V
70 68 69 coex x z V
71 ovex O + Scalar U O V
72 70 71 opth2 F S = x z O + Scalar U O F = x z S = O + Scalar U O
73 eqid + V = + V
74 3 4 6 73 dvavadd K HL W H x T z T x + V z = x z
75 51 55 62 74 syl12anc φ x J X z J Y x + V z = x z
76 75 eqeq2d φ x J X z J Y F = x + V z F = x z
77 76 bicomd φ x J X z J Y F = x z F = x + V z
78 eqid s TEndo K W , t TEndo K W f T s f t f = s TEndo K W , t TEndo K W f T s f t f
79 3 4 56 7 63 78 64 dvhfplusr K HL W H + Scalar U = s TEndo K W , t TEndo K W f T s f t f
80 51 79 syl φ x J X z J Y + Scalar U = s TEndo K W , t TEndo K W f T s f t f
81 80 oveqd φ x J X z J Y O + Scalar U O = O s TEndo K W , t TEndo K W f T s f t f O
82 1 3 4 56 5 78 tendo0pl K HL W H O TEndo K W O s TEndo K W , t TEndo K W f T s f t f O = O
83 51 58 82 syl2anc φ x J X z J Y O s TEndo K W , t TEndo K W f T s f t f O = O
84 81 83 eqtrd φ x J X z J Y O + Scalar U O = O
85 84 eqeq2d φ x J X z J Y S = O + Scalar U O S = O
86 77 85 anbi12d φ x J X z J Y F = x z S = O + Scalar U O F = x + V z S = O
87 72 86 syl5bb φ x J X z J Y F S = x z O + Scalar U O F = x + V z S = O
88 67 87 bitrd φ x J X z J Y F S = x O + U z O F = x + V z S = O
89 88 pm5.32da φ x J X z J Y F S = x O + U z O x J X z J Y F = x + V z S = O
90 50 89 syl5bb φ y w y = O w = O x J X z J Y F S = x y + U z w x J X z J Y F = x + V z S = O
91 38 90 bitrd φ y w x y I X z w I Y F S = x y + U z w x J X z J Y F = x + V z S = O
92 91 exbidv φ z y w x y I X z w I Y F S = x y + U z w z x J X z J Y F = x + V z S = O
93 23 92 syl5bb φ y z w x y I X z w I Y F S = x y + U z w z x J X z J Y F = x + V z S = O
94 93 exbidv φ x y z w x y I X z w I Y F S = x y + U z w x z x J X z J Y F = x + V z S = O
95 anass x J X z J Y F = x + V z S = O x J X z J Y F = x + V z S = O
96 95 bicomi x J X z J Y F = x + V z S = O x J X z J Y F = x + V z S = O
97 96 2exbii x z x J X z J Y F = x + V z S = O x z x J X z J Y F = x + V z S = O
98 19.41vv x z x J X z J Y F = x + V z S = O x z x J X z J Y F = x + V z S = O
99 97 98 bitri x z x J X z J Y F = x + V z S = O x z x J X z J Y F = x + V z S = O
100 3 6 dvalvec K HL W H V LVec
101 lveclmod V LVec V LMod
102 eqid LSubSp V = LSubSp V
103 102 lsssssubg V LMod LSubSp V SubGrp V
104 12 100 101 103 4syl φ LSubSp V SubGrp V
105 1 2 3 6 10 102 dialss K HL W H X B X ˙ W J X LSubSp V
106 12 13 105 syl2anc φ J X LSubSp V
107 104 106 sseldd φ J X SubGrp V
108 1 2 3 6 10 102 dialss K HL W H Y B Y ˙ W J Y LSubSp V
109 12 14 108 syl2anc φ J Y LSubSp V
110 104 109 sseldd φ J Y SubGrp V
111 73 8 lsmelval J X SubGrp V J Y SubGrp V F J X ˙ J Y x J X z J Y F = x + V z
112 107 110 111 syl2anc φ F J X ˙ J Y x J X z J Y F = x + V z
113 r2ex x J X z J Y F = x + V z x z x J X z J Y F = x + V z
114 112 113 bitrdi φ F J X ˙ J Y x z x J X z J Y F = x + V z
115 114 anbi1d φ F J X ˙ J Y S = O x z x J X z J Y F = x + V z S = O
116 115 bicomd φ x z x J X z J Y F = x + V z S = O F J X ˙ J Y S = O
117 99 116 syl5bb φ x z x J X z J Y F = x + V z S = O F J X ˙ J Y S = O
118 22 94 117 3bitrd φ F S I X ˙ I Y F J X ˙ J Y S = O