Metamath Proof Explorer

Theorem ipdirilem

Description: Lemma for ipdiri . (Contributed by NM, 26-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
ip1i.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
ip1i.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
ip1i.7 โŠข ๐‘ƒ = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
ip1i.9 โŠข ๐‘ˆ โˆˆ CPreHilOLD
ipdiri.8 โŠข ๐ด โˆˆ ๐‘‹
ipdiri.9 โŠข ๐ต โˆˆ ๐‘‹
ipdiri.10 โŠข ๐ถ โˆˆ ๐‘‹
Assertion ipdirilem ( ( ๐ด ๐บ ๐ต ) ๐‘ƒ ๐ถ ) = ( ( ๐ด ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) )

Proof

Step Hyp Ref Expression
1 ip1i.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
2 ip1i.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
3 ip1i.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
4 ip1i.7 โŠข ๐‘ƒ = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
5 ip1i.9 โŠข ๐‘ˆ โˆˆ CPreHilOLD
6 ipdiri.8 โŠข ๐ด โˆˆ ๐‘‹
7 ipdiri.9 โŠข ๐ต โˆˆ ๐‘‹
8 ipdiri.10 โŠข ๐ถ โˆˆ ๐‘‹
9 2cn โŠข 2 โˆˆ โ„‚
10 2ne0 โŠข 2 โ‰  0
11 9 10 recidi โŠข ( 2 ยท ( 1 / 2 ) ) = 1
12 11 oveq1i โŠข ( ( 2 ยท ( 1 / 2 ) ) ๐‘† ( ๐ด ๐บ ๐ต ) ) = ( 1 ๐‘† ( ๐ด ๐บ ๐ต ) )
13 5 phnvi โŠข ๐‘ˆ โˆˆ NrmCVec
14 halfcn โŠข ( 1 / 2 ) โˆˆ โ„‚
15 1 2 nvgcl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐บ ๐ต ) โˆˆ ๐‘‹ )
16 13 6 7 15 mp3an โŠข ( ๐ด ๐บ ๐ต ) โˆˆ ๐‘‹
17 9 14 16 3pm3.2i โŠข ( 2 โˆˆ โ„‚ โˆง ( 1 / 2 ) โˆˆ โ„‚ โˆง ( ๐ด ๐บ ๐ต ) โˆˆ ๐‘‹ )
18 1 3 nvsass โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( 2 โˆˆ โ„‚ โˆง ( 1 / 2 ) โˆˆ โ„‚ โˆง ( ๐ด ๐บ ๐ต ) โˆˆ ๐‘‹ ) ) โ†’ ( ( 2 ยท ( 1 / 2 ) ) ๐‘† ( ๐ด ๐บ ๐ต ) ) = ( 2 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ) )
19 13 17 18 mp2an โŠข ( ( 2 ยท ( 1 / 2 ) ) ๐‘† ( ๐ด ๐บ ๐ต ) ) = ( 2 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) )
20 1 3 nvsid โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ๐ด ๐บ ๐ต ) โˆˆ ๐‘‹ ) โ†’ ( 1 ๐‘† ( ๐ด ๐บ ๐ต ) ) = ( ๐ด ๐บ ๐ต ) )
21 13 16 20 mp2an โŠข ( 1 ๐‘† ( ๐ด ๐บ ๐ต ) ) = ( ๐ด ๐บ ๐ต )
22 12 19 21 3eqtr3i โŠข ( 2 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ) = ( ๐ด ๐บ ๐ต )
23 22 oveq1i โŠข ( ( 2 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ) ๐‘ƒ ๐ถ ) = ( ( ๐ด ๐บ ๐ต ) ๐‘ƒ ๐ถ )
24 1 3 nvscl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( 1 / 2 ) โˆˆ โ„‚ โˆง ( ๐ด ๐บ ๐ต ) โˆˆ ๐‘‹ ) โ†’ ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) โˆˆ ๐‘‹ )
25 13 14 16 24 mp3an โŠข ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) โˆˆ ๐‘‹
26 1 2 3 4 5 25 8 ip2i โŠข ( ( 2 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ) ๐‘ƒ ๐ถ ) = ( 2 ยท ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐‘ƒ ๐ถ ) )
27 23 26 eqtr3i โŠข ( ( ๐ด ๐บ ๐ต ) ๐‘ƒ ๐ถ ) = ( 2 ยท ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐‘ƒ ๐ถ ) )
28 neg1cn โŠข - 1 โˆˆ โ„‚
29 1 3 nvscl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง - 1 โˆˆ โ„‚ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ๐ต ) โˆˆ ๐‘‹ )
30 13 28 7 29 mp3an โŠข ( - 1 ๐‘† ๐ต ) โˆˆ ๐‘‹
31 1 2 nvgcl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ โˆง ( - 1 ๐‘† ๐ต ) โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) โˆˆ ๐‘‹ )
32 13 6 30 31 mp3an โŠข ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) โˆˆ ๐‘‹
33 1 3 nvscl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( 1 / 2 ) โˆˆ โ„‚ โˆง ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) โˆˆ ๐‘‹ ) โ†’ ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) โˆˆ ๐‘‹ )
34 13 14 32 33 mp3an โŠข ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) โˆˆ ๐‘‹
35 1 2 3 4 5 25 34 8 ip1i โŠข ( ( ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) ๐‘ƒ ๐ถ ) + ( ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( - 1 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) ) ๐‘ƒ ๐ถ ) ) = ( 2 ยท ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐‘ƒ ๐ถ ) )
36 eqid โŠข ( 1st โ€˜ ๐‘ˆ ) = ( 1st โ€˜ ๐‘ˆ )
37 36 nvvc โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( 1st โ€˜ ๐‘ˆ ) โˆˆ CVecOLD )
38 13 37 ax-mp โŠข ( 1st โ€˜ ๐‘ˆ ) โˆˆ CVecOLD
39 2 vafval โŠข ๐บ = ( 1st โ€˜ ( 1st โ€˜ ๐‘ˆ ) )
40 39 vcablo โŠข ( ( 1st โ€˜ ๐‘ˆ ) โˆˆ CVecOLD โ†’ ๐บ โˆˆ AbelOp )
41 38 40 ax-mp โŠข ๐บ โˆˆ AbelOp
42 6 7 pm3.2i โŠข ( ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ )
43 6 30 pm3.2i โŠข ( ๐ด โˆˆ ๐‘‹ โˆง ( - 1 ๐‘† ๐ต ) โˆˆ ๐‘‹ )
44 1 2 bafval โŠข ๐‘‹ = ran ๐บ
45 44 ablo4 โŠข ( ( ๐บ โˆˆ AbelOp โˆง ( ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โˆง ( ๐ด โˆˆ ๐‘‹ โˆง ( - 1 ๐‘† ๐ต ) โˆˆ ๐‘‹ ) ) โ†’ ( ( ๐ด ๐บ ๐ต ) ๐บ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( ( ๐ด ๐บ ๐ด ) ๐บ ( ๐ต ๐บ ( - 1 ๐‘† ๐ต ) ) ) )
46 41 42 43 45 mp3an โŠข ( ( ๐ด ๐บ ๐ต ) ๐บ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( ( ๐ด ๐บ ๐ด ) ๐บ ( ๐ต ๐บ ( - 1 ๐‘† ๐ต ) ) )
47 3 smfval โŠข ๐‘† = ( 2nd โ€˜ ( 1st โ€˜ ๐‘ˆ ) )
48 39 47 44 vc2OLD โŠข ( ( ( 1st โ€˜ ๐‘ˆ ) โˆˆ CVecOLD โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐บ ๐ด ) = ( 2 ๐‘† ๐ด ) )
49 38 6 48 mp2an โŠข ( ๐ด ๐บ ๐ด ) = ( 2 ๐‘† ๐ด )
50 eqid โŠข ( 0vec โ€˜ ๐‘ˆ ) = ( 0vec โ€˜ ๐‘ˆ )
51 1 2 3 50 nvrinv โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ต ๐บ ( - 1 ๐‘† ๐ต ) ) = ( 0vec โ€˜ ๐‘ˆ ) )
52 13 7 51 mp2an โŠข ( ๐ต ๐บ ( - 1 ๐‘† ๐ต ) ) = ( 0vec โ€˜ ๐‘ˆ )
53 49 52 oveq12i โŠข ( ( ๐ด ๐บ ๐ด ) ๐บ ( ๐ต ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( ( 2 ๐‘† ๐ด ) ๐บ ( 0vec โ€˜ ๐‘ˆ ) )
54 1 3 nvscl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง 2 โˆˆ โ„‚ โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( 2 ๐‘† ๐ด ) โˆˆ ๐‘‹ )
55 13 9 6 54 mp3an โŠข ( 2 ๐‘† ๐ด ) โˆˆ ๐‘‹
56 1 2 50 nv0rid โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( 2 ๐‘† ๐ด ) โˆˆ ๐‘‹ ) โ†’ ( ( 2 ๐‘† ๐ด ) ๐บ ( 0vec โ€˜ ๐‘ˆ ) ) = ( 2 ๐‘† ๐ด ) )
57 13 55 56 mp2an โŠข ( ( 2 ๐‘† ๐ด ) ๐บ ( 0vec โ€˜ ๐‘ˆ ) ) = ( 2 ๐‘† ๐ด )
58 46 53 57 3eqtri โŠข ( ( ๐ด ๐บ ๐ต ) ๐บ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( 2 ๐‘† ๐ด )
59 58 oveq2i โŠข ( ( 1 / 2 ) ๐‘† ( ( ๐ด ๐บ ๐ต ) ๐บ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) = ( ( 1 / 2 ) ๐‘† ( 2 ๐‘† ๐ด ) )
60 14 9 6 3pm3.2i โŠข ( ( 1 / 2 ) โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง ๐ด โˆˆ ๐‘‹ )
61 1 3 nvsass โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ( 1 / 2 ) โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง ๐ด โˆˆ ๐‘‹ ) ) โ†’ ( ( ( 1 / 2 ) ยท 2 ) ๐‘† ๐ด ) = ( ( 1 / 2 ) ๐‘† ( 2 ๐‘† ๐ด ) ) )
62 13 60 61 mp2an โŠข ( ( ( 1 / 2 ) ยท 2 ) ๐‘† ๐ด ) = ( ( 1 / 2 ) ๐‘† ( 2 ๐‘† ๐ด ) )
63 59 62 eqtr4i โŠข ( ( 1 / 2 ) ๐‘† ( ( ๐ด ๐บ ๐ต ) ๐บ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) = ( ( ( 1 / 2 ) ยท 2 ) ๐‘† ๐ด )
64 14 16 32 3pm3.2i โŠข ( ( 1 / 2 ) โˆˆ โ„‚ โˆง ( ๐ด ๐บ ๐ต ) โˆˆ ๐‘‹ โˆง ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) โˆˆ ๐‘‹ )
65 1 2 3 nvdi โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ( 1 / 2 ) โˆˆ โ„‚ โˆง ( ๐ด ๐บ ๐ต ) โˆˆ ๐‘‹ โˆง ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) โˆˆ ๐‘‹ ) ) โ†’ ( ( 1 / 2 ) ๐‘† ( ( ๐ด ๐บ ๐ต ) ๐บ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) = ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) )
66 13 64 65 mp2an โŠข ( ( 1 / 2 ) ๐‘† ( ( ๐ด ๐บ ๐ต ) ๐บ ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) = ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) )
67 ax-1cn โŠข 1 โˆˆ โ„‚
68 67 9 10 divcan1i โŠข ( ( 1 / 2 ) ยท 2 ) = 1
69 68 oveq1i โŠข ( ( ( 1 / 2 ) ยท 2 ) ๐‘† ๐ด ) = ( 1 ๐‘† ๐ด )
70 1 3 nvsid โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( 1 ๐‘† ๐ด ) = ๐ด )
71 13 6 70 mp2an โŠข ( 1 ๐‘† ๐ด ) = ๐ด
72 69 71 eqtri โŠข ( ( ( 1 / 2 ) ยท 2 ) ๐‘† ๐ด ) = ๐ด
73 63 66 72 3eqtr3i โŠข ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) = ๐ด
74 73 oveq1i โŠข ( ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) ๐‘ƒ ๐ถ ) = ( ๐ด ๐‘ƒ ๐ถ )
75 28 14 mulcomi โŠข ( - 1 ยท ( 1 / 2 ) ) = ( ( 1 / 2 ) ยท - 1 )
76 75 oveq1i โŠข ( ( - 1 ยท ( 1 / 2 ) ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( ( ( 1 / 2 ) ยท - 1 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) )
77 28 14 32 3pm3.2i โŠข ( - 1 โˆˆ โ„‚ โˆง ( 1 / 2 ) โˆˆ โ„‚ โˆง ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) โˆˆ ๐‘‹ )
78 1 3 nvsass โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( - 1 โˆˆ โ„‚ โˆง ( 1 / 2 ) โˆˆ โ„‚ โˆง ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) โˆˆ ๐‘‹ ) ) โ†’ ( ( - 1 ยท ( 1 / 2 ) ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( - 1 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) )
79 13 77 78 mp2an โŠข ( ( - 1 ยท ( 1 / 2 ) ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( - 1 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) )
80 14 28 32 3pm3.2i โŠข ( ( 1 / 2 ) โˆˆ โ„‚ โˆง - 1 โˆˆ โ„‚ โˆง ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) โˆˆ ๐‘‹ )
81 1 3 nvsass โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ( 1 / 2 ) โˆˆ โ„‚ โˆง - 1 โˆˆ โ„‚ โˆง ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) โˆˆ ๐‘‹ ) ) โ†’ ( ( ( 1 / 2 ) ยท - 1 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( ( 1 / 2 ) ๐‘† ( - 1 ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) )
82 13 80 81 mp2an โŠข ( ( ( 1 / 2 ) ยท - 1 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( ( 1 / 2 ) ๐‘† ( - 1 ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) )
83 28 6 30 3pm3.2i โŠข ( - 1 โˆˆ โ„‚ โˆง ๐ด โˆˆ ๐‘‹ โˆง ( - 1 ๐‘† ๐ต ) โˆˆ ๐‘‹ )
84 1 2 3 nvdi โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( - 1 โˆˆ โ„‚ โˆง ๐ด โˆˆ ๐‘‹ โˆง ( - 1 ๐‘† ๐ต ) โˆˆ ๐‘‹ ) ) โ†’ ( - 1 ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( ( - 1 ๐‘† ๐ด ) ๐บ ( - 1 ๐‘† ( - 1 ๐‘† ๐ต ) ) ) )
85 13 83 84 mp2an โŠข ( - 1 ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( ( - 1 ๐‘† ๐ด ) ๐บ ( - 1 ๐‘† ( - 1 ๐‘† ๐ต ) ) )
86 neg1mulneg1e1 โŠข ( - 1 ยท - 1 ) = 1
87 86 oveq1i โŠข ( ( - 1 ยท - 1 ) ๐‘† ๐ต ) = ( 1 ๐‘† ๐ต )
88 28 28 7 3pm3.2i โŠข ( - 1 โˆˆ โ„‚ โˆง - 1 โˆˆ โ„‚ โˆง ๐ต โˆˆ ๐‘‹ )
89 1 3 nvsass โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( - 1 โˆˆ โ„‚ โˆง - 1 โˆˆ โ„‚ โˆง ๐ต โˆˆ ๐‘‹ ) ) โ†’ ( ( - 1 ยท - 1 ) ๐‘† ๐ต ) = ( - 1 ๐‘† ( - 1 ๐‘† ๐ต ) ) )
90 13 88 89 mp2an โŠข ( ( - 1 ยท - 1 ) ๐‘† ๐ต ) = ( - 1 ๐‘† ( - 1 ๐‘† ๐ต ) )
91 1 3 nvsid โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( 1 ๐‘† ๐ต ) = ๐ต )
92 13 7 91 mp2an โŠข ( 1 ๐‘† ๐ต ) = ๐ต
93 87 90 92 3eqtr3i โŠข ( - 1 ๐‘† ( - 1 ๐‘† ๐ต ) ) = ๐ต
94 93 oveq2i โŠข ( ( - 1 ๐‘† ๐ด ) ๐บ ( - 1 ๐‘† ( - 1 ๐‘† ๐ต ) ) ) = ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต )
95 85 94 eqtri โŠข ( - 1 ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต )
96 95 oveq2i โŠข ( ( 1 / 2 ) ๐‘† ( - 1 ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) = ( ( 1 / 2 ) ๐‘† ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) )
97 82 96 eqtri โŠข ( ( ( 1 / 2 ) ยท - 1 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) = ( ( 1 / 2 ) ๐‘† ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) )
98 76 79 97 3eqtr3i โŠข ( - 1 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) = ( ( 1 / 2 ) ๐‘† ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) )
99 98 oveq2i โŠข ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( - 1 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) ) = ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( ( 1 / 2 ) ๐‘† ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) )
100 1 3 nvscl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง - 1 โˆˆ โ„‚ โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( - 1 ๐‘† ๐ด ) โˆˆ ๐‘‹ )
101 13 28 6 100 mp3an โŠข ( - 1 ๐‘† ๐ด ) โˆˆ ๐‘‹
102 1 2 nvgcl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( - 1 ๐‘† ๐ด ) โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) โˆˆ ๐‘‹ )
103 13 101 7 102 mp3an โŠข ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) โˆˆ ๐‘‹
104 14 16 103 3pm3.2i โŠข ( ( 1 / 2 ) โˆˆ โ„‚ โˆง ( ๐ด ๐บ ๐ต ) โˆˆ ๐‘‹ โˆง ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) โˆˆ ๐‘‹ )
105 1 2 3 nvdi โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ( 1 / 2 ) โˆˆ โ„‚ โˆง ( ๐ด ๐บ ๐ต ) โˆˆ ๐‘‹ โˆง ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) โˆˆ ๐‘‹ ) ) โ†’ ( ( 1 / 2 ) ๐‘† ( ( ๐ด ๐บ ๐ต ) ๐บ ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) ) = ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( ( 1 / 2 ) ๐‘† ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) ) )
106 13 104 105 mp2an โŠข ( ( 1 / 2 ) ๐‘† ( ( ๐ด ๐บ ๐ต ) ๐บ ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) ) = ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( ( 1 / 2 ) ๐‘† ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) )
107 99 106 eqtr4i โŠข ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( - 1 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) ) = ( ( 1 / 2 ) ๐‘† ( ( ๐ด ๐บ ๐ต ) ๐บ ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) )
108 101 7 pm3.2i โŠข ( ( - 1 ๐‘† ๐ด ) โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ )
109 44 ablo4 โŠข ( ( ๐บ โˆˆ AbelOp โˆง ( ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โˆง ( ( - 1 ๐‘† ๐ด ) โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) ) โ†’ ( ( ๐ด ๐บ ๐ต ) ๐บ ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) = ( ( ๐ด ๐บ ( - 1 ๐‘† ๐ด ) ) ๐บ ( ๐ต ๐บ ๐ต ) ) )
110 41 42 108 109 mp3an โŠข ( ( ๐ด ๐บ ๐ต ) ๐บ ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) = ( ( ๐ด ๐บ ( - 1 ๐‘† ๐ด ) ) ๐บ ( ๐ต ๐บ ๐ต ) )
111 1 2 3 50 nvrinv โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ๐ด ๐บ ( - 1 ๐‘† ๐ด ) ) = ( 0vec โ€˜ ๐‘ˆ ) )
112 13 6 111 mp2an โŠข ( ๐ด ๐บ ( - 1 ๐‘† ๐ด ) ) = ( 0vec โ€˜ ๐‘ˆ )
113 112 oveq1i โŠข ( ( ๐ด ๐บ ( - 1 ๐‘† ๐ด ) ) ๐บ ( ๐ต ๐บ ๐ต ) ) = ( ( 0vec โ€˜ ๐‘ˆ ) ๐บ ( ๐ต ๐บ ๐ต ) )
114 1 2 nvgcl โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐ต โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ต ๐บ ๐ต ) โˆˆ ๐‘‹ )
115 13 7 7 114 mp3an โŠข ( ๐ต ๐บ ๐ต ) โˆˆ ๐‘‹
116 1 2 50 nv0lid โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ๐ต ๐บ ๐ต ) โˆˆ ๐‘‹ ) โ†’ ( ( 0vec โ€˜ ๐‘ˆ ) ๐บ ( ๐ต ๐บ ๐ต ) ) = ( ๐ต ๐บ ๐ต ) )
117 13 115 116 mp2an โŠข ( ( 0vec โ€˜ ๐‘ˆ ) ๐บ ( ๐ต ๐บ ๐ต ) ) = ( ๐ต ๐บ ๐ต )
118 113 117 eqtri โŠข ( ( ๐ด ๐บ ( - 1 ๐‘† ๐ด ) ) ๐บ ( ๐ต ๐บ ๐ต ) ) = ( ๐ต ๐บ ๐ต )
119 39 47 44 vc2OLD โŠข ( ( ( 1st โ€˜ ๐‘ˆ ) โˆˆ CVecOLD โˆง ๐ต โˆˆ ๐‘‹ ) โ†’ ( ๐ต ๐บ ๐ต ) = ( 2 ๐‘† ๐ต ) )
120 38 7 119 mp2an โŠข ( ๐ต ๐บ ๐ต ) = ( 2 ๐‘† ๐ต )
121 110 118 120 3eqtri โŠข ( ( ๐ด ๐บ ๐ต ) ๐บ ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) = ( 2 ๐‘† ๐ต )
122 121 oveq2i โŠข ( ( 1 / 2 ) ๐‘† ( ( ๐ด ๐บ ๐ต ) ๐บ ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) ) = ( ( 1 / 2 ) ๐‘† ( 2 ๐‘† ๐ต ) )
123 14 9 7 3pm3.2i โŠข ( ( 1 / 2 ) โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง ๐ต โˆˆ ๐‘‹ )
124 1 3 nvsass โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ( ( 1 / 2 ) โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง ๐ต โˆˆ ๐‘‹ ) ) โ†’ ( ( ( 1 / 2 ) ยท 2 ) ๐‘† ๐ต ) = ( ( 1 / 2 ) ๐‘† ( 2 ๐‘† ๐ต ) ) )
125 13 123 124 mp2an โŠข ( ( ( 1 / 2 ) ยท 2 ) ๐‘† ๐ต ) = ( ( 1 / 2 ) ๐‘† ( 2 ๐‘† ๐ต ) )
126 68 oveq1i โŠข ( ( ( 1 / 2 ) ยท 2 ) ๐‘† ๐ต ) = ( 1 ๐‘† ๐ต )
127 122 125 126 3eqtr2i โŠข ( ( 1 / 2 ) ๐‘† ( ( ๐ด ๐บ ๐ต ) ๐บ ( ( - 1 ๐‘† ๐ด ) ๐บ ๐ต ) ) ) = ( 1 ๐‘† ๐ต )
128 107 127 92 3eqtri โŠข ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( - 1 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) ) = ๐ต
129 128 oveq1i โŠข ( ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( - 1 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) ) ๐‘ƒ ๐ถ ) = ( ๐ต ๐‘ƒ ๐ถ )
130 74 129 oveq12i โŠข ( ( ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) ๐‘ƒ ๐ถ ) + ( ( ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ๐ต ) ) ๐บ ( - 1 ๐‘† ( ( 1 / 2 ) ๐‘† ( ๐ด ๐บ ( - 1 ๐‘† ๐ต ) ) ) ) ) ๐‘ƒ ๐ถ ) ) = ( ( ๐ด ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) )
131 27 35 130 3eqtr2i โŠข ( ( ๐ด ๐บ ๐ต ) ๐‘ƒ ๐ถ ) = ( ( ๐ด ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) )