Step | Hyp | Ref
| Expression |
1 | | simp1 1134 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (πΎ β HL β§ π β π»)) |
2 | | cdlemn4.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
3 | | cdlemn4.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
4 | | cdlemn4.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
5 | | cdlemn4.p |
. . . . . 6
β’ π = ((ocβπΎ)βπ) |
6 | 2, 3, 4, 5 | lhpocnel2 39193 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (π β π΄ β§ Β¬ π β€ π)) |
7 | 1, 6 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (π β π΄ β§ Β¬ π β€ π)) |
8 | | simp2 1135 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (π β π΄ β§ Β¬ π β€ π)) |
9 | | cdlemn4.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
10 | | cdlemn4.f |
. . . . 5
β’ πΉ = (β©β β π (ββπ) = π) |
11 | 2, 3, 4, 9, 10 | ltrniotacl 39753 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
12 | 1, 7, 8, 11 | syl3anc 1369 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β πΉ β π) |
13 | | eqid 2730 |
. . . . 5
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
14 | 4, 9, 13 | tendoidcl 39943 |
. . . 4
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β ((TEndoβπΎ)βπ)) |
15 | 1, 14 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β ( I βΎ π) β ((TEndoβπΎ)βπ)) |
16 | | cdlemn4.j |
. . . 4
β’ π½ = (β©β β π (ββπ) = π
) |
17 | 2, 3, 4, 9, 16 | ltrniotacl 39753 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β π½ β π) |
18 | | cdlemn4.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
19 | | cdlemn4.o |
. . . . 5
β’ π = (β β π β¦ ( I βΎ π΅)) |
20 | 18, 4, 9, 13, 19 | tendo0cl 39964 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π β ((TEndoβπΎ)βπ)) |
21 | 1, 20 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β π β ((TEndoβπΎ)βπ)) |
22 | | cdlemn4.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
23 | | eqid 2730 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
24 | | cdlemn4.s |
. . . 4
β’ + =
(+gβπ) |
25 | | eqid 2730 |
. . . 4
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
26 | 4, 9, 13, 22, 23, 24, 25 | dvhopvadd 40267 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ ( I βΎ π) β ((TEndoβπΎ)βπ)) β§ (π½ β π β§ π β ((TEndoβπΎ)βπ))) β (β¨πΉ, ( I βΎ π)β© + β¨π½, πβ©) = β¨(πΉ β π½), (( I βΎ π)(+gβ(Scalarβπ))π)β©) |
27 | 1, 12, 15, 17, 21, 26 | syl122anc 1377 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (β¨πΉ, ( I βΎ π)β© + β¨π½, πβ©) = β¨(πΉ β π½), (( I βΎ π)(+gβ(Scalarβπ))π)β©) |
28 | 4, 9 | ltrncom 39912 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π½ β π) β (πΉ β π½) = (π½ β πΉ)) |
29 | 1, 12, 17, 28 | syl3anc 1369 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (πΉ β π½) = (π½ β πΉ)) |
30 | | cdlemn4.g |
. . . . 5
β’ πΊ = (β©β β π (ββπ) = π
) |
31 | 2, 3, 5, 4, 9, 10,
30, 16 | cdlemn3 40371 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (π½ β πΉ) = πΊ) |
32 | 29, 31 | eqtrd 2770 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (πΉ β π½) = πΊ) |
33 | | eqid 2730 |
. . . . . . . . 9
β’
((EDRingβπΎ)βπ) = ((EDRingβπΎ)βπ) |
34 | 4, 33, 22, 23 | dvhsca 40256 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (Scalarβπ) = ((EDRingβπΎ)βπ)) |
35 | 34 | fveq2d 6894 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β
(0gβ(Scalarβπ)) =
(0gβ((EDRingβπΎ)βπ))) |
36 | | eqid 2730 |
. . . . . . . 8
β’
(0gβ((EDRingβπΎ)βπ)) =
(0gβ((EDRingβπΎ)βπ)) |
37 | 18, 4, 9, 33, 19, 36 | erng0g 40168 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β
(0gβ((EDRingβπΎ)βπ)) = π) |
38 | 35, 37 | eqtrd 2770 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β
(0gβ(Scalarβπ)) = π) |
39 | 1, 38 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β
(0gβ(Scalarβπ)) = π) |
40 | 39 | oveq2d 7427 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (( I βΎ π)(+gβ(Scalarβπ))(0gβ(Scalarβπ))) = (( I βΎ π)(+gβ(Scalarβπ))π)) |
41 | 4, 33 | erngdv 40167 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β ((EDRingβπΎ)βπ) β DivRing) |
42 | | drnggrp 20510 |
. . . . . . . 8
β’
(((EDRingβπΎ)βπ) β DivRing β ((EDRingβπΎ)βπ) β Grp) |
43 | 41, 42 | syl 17 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β ((EDRingβπΎ)βπ) β Grp) |
44 | 34, 43 | eqeltrd 2831 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β (Scalarβπ) β Grp) |
45 | 1, 44 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (Scalarβπ) β Grp) |
46 | | eqid 2730 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
47 | 4, 13, 22, 23, 46 | dvhbase 40257 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (Baseβ(Scalarβπ)) = ((TEndoβπΎ)βπ)) |
48 | 1, 47 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (Baseβ(Scalarβπ)) = ((TEndoβπΎ)βπ)) |
49 | 15, 48 | eleqtrrd 2834 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β ( I βΎ π) β (Baseβ(Scalarβπ))) |
50 | | eqid 2730 |
. . . . . 6
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
51 | 46, 25, 50 | grprid 18889 |
. . . . 5
β’
(((Scalarβπ)
β Grp β§ ( I βΎ π) β (Baseβ(Scalarβπ))) β (( I βΎ π)(+gβ(Scalarβπ))(0gβ(Scalarβπ))) = ( I βΎ π)) |
52 | 45, 49, 51 | syl2anc 582 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (( I βΎ π)(+gβ(Scalarβπ))(0gβ(Scalarβπ))) = ( I βΎ π)) |
53 | 40, 52 | eqtr3d 2772 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (( I βΎ π)(+gβ(Scalarβπ))π) = ( I βΎ π)) |
54 | 32, 53 | opeq12d 4880 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β β¨(πΉ β π½), (( I βΎ π)(+gβ(Scalarβπ))π)β© = β¨πΊ, ( I βΎ π)β©) |
55 | 27, 54 | eqtr2d 2771 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β β¨πΊ, ( I βΎ π)β© = (β¨πΉ, ( I βΎ π)β© + β¨π½, πβ©)) |