Step | Hyp | Ref
| Expression |
1 | | df-c 11116 |
. 2
โข โ =
(R ร R) |
2 | | eqeq1 2737 |
. . 3
โข
(โจ๐ง, ๐คโฉ = ๐ด โ (โจ๐ง, ๐คโฉ = (๐ฅ + (i ยท ๐ฆ)) โ ๐ด = (๐ฅ + (i ยท ๐ฆ)))) |
3 | 2 | 2rexbidv 3220 |
. 2
โข
(โจ๐ง, ๐คโฉ = ๐ด โ (โ๐ฅ โ โ โ๐ฆ โ โ โจ๐ง, ๐คโฉ = (๐ฅ + (i ยท ๐ฆ)) โ โ๐ฅ โ โ โ๐ฆ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ)))) |
4 | | opelreal 11125 |
. . . . . 6
โข
(โจ๐ง,
0Rโฉ โ โ โ ๐ง โ R) |
5 | | opelreal 11125 |
. . . . . 6
โข
(โจ๐ค,
0Rโฉ โ โ โ ๐ค โ R) |
6 | 4, 5 | anbi12i 628 |
. . . . 5
โข
((โจ๐ง,
0Rโฉ โ โ โง โจ๐ค, 0Rโฉ โ
โ) โ (๐ง โ
R โง ๐ค
โ R)) |
7 | 6 | biimpri 227 |
. . . 4
โข ((๐ง โ R โง
๐ค โ R)
โ (โจ๐ง,
0Rโฉ โ โ โง โจ๐ค, 0Rโฉ โ
โ)) |
8 | | df-i 11119 |
. . . . . . . . 9
โข i =
โจ0R,
1Rโฉ |
9 | 8 | oveq1i 7419 |
. . . . . . . 8
โข (i
ยท โจ๐ค,
0Rโฉ) = (โจ0R,
1Rโฉ ยท โจ๐ค,
0Rโฉ) |
10 | | 0r 11075 |
. . . . . . . . . 10
โข
0R โ R |
11 | | 1sr 11076 |
. . . . . . . . . . 11
โข
1R โ R |
12 | | mulcnsr 11131 |
. . . . . . . . . . 11
โข
(((0R โ R โง
1R โ R) โง (๐ค โ R โง
0R โ R)) โ
(โจ0R, 1Rโฉ ยท
โจ๐ค,
0Rโฉ) = โจ((0R
ยทR ๐ค) +R
(-1R ยทR
(1R ยทR
0R))), ((1R
ยทR ๐ค) +R
(0R ยทR
0R))โฉ) |
13 | 10, 11, 12 | mpanl12 701 |
. . . . . . . . . 10
โข ((๐ค โ R โง
0R โ R) โ
(โจ0R, 1Rโฉ ยท
โจ๐ค,
0Rโฉ) = โจ((0R
ยทR ๐ค) +R
(-1R ยทR
(1R ยทR
0R))), ((1R
ยทR ๐ค) +R
(0R ยทR
0R))โฉ) |
14 | 10, 13 | mpan2 690 |
. . . . . . . . 9
โข (๐ค โ R โ
(โจ0R, 1Rโฉ ยท
โจ๐ค,
0Rโฉ) = โจ((0R
ยทR ๐ค) +R
(-1R ยทR
(1R ยทR
0R))), ((1R
ยทR ๐ค) +R
(0R ยทR
0R))โฉ) |
15 | | mulcomsr 11084 |
. . . . . . . . . . . . 13
โข
(0R ยทR ๐ค) = (๐ค ยทR
0R) |
16 | | 00sr 11094 |
. . . . . . . . . . . . 13
โข (๐ค โ R โ
(๐ค
ยทR 0R) =
0R) |
17 | 15, 16 | eqtrid 2785 |
. . . . . . . . . . . 12
โข (๐ค โ R โ
(0R ยทR ๐ค) =
0R) |
18 | 17 | oveq1d 7424 |
. . . . . . . . . . 11
โข (๐ค โ R โ
((0R ยทR ๐ค) +R
(-1R ยทR
(1R ยทR
0R))) = (0R
+R (-1R
ยทR (1R
ยทR
0R)))) |
19 | | 00sr 11094 |
. . . . . . . . . . . . . . . 16
โข
(1R โ R โ
(1R ยทR
0R) = 0R) |
20 | 11, 19 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข
(1R ยทR
0R) = 0R |
21 | 20 | oveq2i 7420 |
. . . . . . . . . . . . . 14
โข
(-1R ยทR
(1R ยทR
0R)) = (-1R
ยทR
0R) |
22 | | m1r 11077 |
. . . . . . . . . . . . . . 15
โข
-1R โ R |
23 | | 00sr 11094 |
. . . . . . . . . . . . . . 15
โข
(-1R โ R โ
(-1R ยทR
0R) = 0R) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข
(-1R ยทR
0R) = 0R |
25 | 21, 24 | eqtri 2761 |
. . . . . . . . . . . . 13
โข
(-1R ยทR
(1R ยทR
0R)) = 0R |
26 | 25 | oveq2i 7420 |
. . . . . . . . . . . 12
โข
(0R +R
(-1R ยทR
(1R ยทR
0R))) = (0R
+R 0R) |
27 | | 0idsr 11092 |
. . . . . . . . . . . . 13
โข
(0R โ R โ
(0R +R
0R) = 0R) |
28 | 10, 27 | ax-mp 5 |
. . . . . . . . . . . 12
โข
(0R +R
0R) = 0R |
29 | 26, 28 | eqtri 2761 |
. . . . . . . . . . 11
โข
(0R +R
(-1R ยทR
(1R ยทR
0R))) = 0R |
30 | 18, 29 | eqtrdi 2789 |
. . . . . . . . . 10
โข (๐ค โ R โ
((0R ยทR ๐ค) +R
(-1R ยทR
(1R ยทR
0R))) = 0R) |
31 | | mulcomsr 11084 |
. . . . . . . . . . . . 13
โข
(1R ยทR ๐ค) = (๐ค ยทR
1R) |
32 | | 1idsr 11093 |
. . . . . . . . . . . . 13
โข (๐ค โ R โ
(๐ค
ยทR 1R) = ๐ค) |
33 | 31, 32 | eqtrid 2785 |
. . . . . . . . . . . 12
โข (๐ค โ R โ
(1R ยทR ๐ค) = ๐ค) |
34 | 33 | oveq1d 7424 |
. . . . . . . . . . 11
โข (๐ค โ R โ
((1R ยทR ๐ค) +R
(0R ยทR
0R)) = (๐ค +R
(0R ยทR
0R))) |
35 | | 00sr 11094 |
. . . . . . . . . . . . . 14
โข
(0R โ R โ
(0R ยทR
0R) = 0R) |
36 | 10, 35 | ax-mp 5 |
. . . . . . . . . . . . 13
โข
(0R ยทR
0R) = 0R |
37 | 36 | oveq2i 7420 |
. . . . . . . . . . . 12
โข (๐ค +R
(0R ยทR
0R)) = (๐ค +R
0R) |
38 | | 0idsr 11092 |
. . . . . . . . . . . 12
โข (๐ค โ R โ
(๐ค
+R 0R) = ๐ค) |
39 | 37, 38 | eqtrid 2785 |
. . . . . . . . . . 11
โข (๐ค โ R โ
(๐ค
+R (0R
ยทR 0R)) = ๐ค) |
40 | 34, 39 | eqtrd 2773 |
. . . . . . . . . 10
โข (๐ค โ R โ
((1R ยทR ๐ค) +R
(0R ยทR
0R)) = ๐ค) |
41 | 30, 40 | opeq12d 4882 |
. . . . . . . . 9
โข (๐ค โ R โ
โจ((0R ยทR ๐ค) +R
(-1R ยทR
(1R ยทR
0R))), ((1R
ยทR ๐ค) +R
(0R ยทR
0R))โฉ = โจ0R, ๐คโฉ) |
42 | 14, 41 | eqtrd 2773 |
. . . . . . . 8
โข (๐ค โ R โ
(โจ0R, 1Rโฉ ยท
โจ๐ค,
0Rโฉ) = โจ0R, ๐คโฉ) |
43 | 9, 42 | eqtrid 2785 |
. . . . . . 7
โข (๐ค โ R โ
(i ยท โจ๐ค,
0Rโฉ) = โจ0R, ๐คโฉ) |
44 | 43 | oveq2d 7425 |
. . . . . 6
โข (๐ค โ R โ
(โจ๐ง,
0Rโฉ + (i ยท โจ๐ค, 0Rโฉ)) =
(โจ๐ง,
0Rโฉ + โจ0R, ๐คโฉ)) |
45 | 44 | adantl 483 |
. . . . 5
โข ((๐ง โ R โง
๐ค โ R)
โ (โจ๐ง,
0Rโฉ + (i ยท โจ๐ค, 0Rโฉ)) =
(โจ๐ง,
0Rโฉ + โจ0R, ๐คโฉ)) |
46 | | addcnsr 11130 |
. . . . . . 7
โข (((๐ง โ R โง
0R โ R) โง
(0R โ R โง ๐ค โ R)) โ (โจ๐ง,
0Rโฉ + โจ0R, ๐คโฉ) = โจ(๐ง +R
0R), (0R
+R ๐ค)โฉ) |
47 | 10, 46 | mpanl2 700 |
. . . . . 6
โข ((๐ง โ R โง
(0R โ R โง ๐ค โ R)) โ (โจ๐ง,
0Rโฉ + โจ0R, ๐คโฉ) = โจ(๐ง +R
0R), (0R
+R ๐ค)โฉ) |
48 | 10, 47 | mpanr1 702 |
. . . . 5
โข ((๐ง โ R โง
๐ค โ R)
โ (โจ๐ง,
0Rโฉ + โจ0R, ๐คโฉ) = โจ(๐ง +R
0R), (0R
+R ๐ค)โฉ) |
49 | | 0idsr 11092 |
. . . . . 6
โข (๐ง โ R โ
(๐ง
+R 0R) = ๐ง) |
50 | | addcomsr 11082 |
. . . . . . 7
โข
(0R +R ๐ค) = (๐ค +R
0R) |
51 | 50, 38 | eqtrid 2785 |
. . . . . 6
โข (๐ค โ R โ
(0R +R ๐ค) = ๐ค) |
52 | | opeq12 4876 |
. . . . . 6
โข (((๐ง +R
0R) = ๐ง โง (0R
+R ๐ค) = ๐ค) โ โจ(๐ง +R
0R), (0R
+R ๐ค)โฉ = โจ๐ง, ๐คโฉ) |
53 | 49, 51, 52 | syl2an 597 |
. . . . 5
โข ((๐ง โ R โง
๐ค โ R)
โ โจ(๐ง
+R 0R),
(0R +R ๐ค)โฉ = โจ๐ง, ๐คโฉ) |
54 | 45, 48, 53 | 3eqtrrd 2778 |
. . . 4
โข ((๐ง โ R โง
๐ค โ R)
โ โจ๐ง, ๐คโฉ = (โจ๐ง,
0Rโฉ + (i ยท โจ๐ค,
0Rโฉ))) |
55 | | opex 5465 |
. . . . 5
โข
โจ๐ง,
0Rโฉ โ V |
56 | | opex 5465 |
. . . . 5
โข
โจ๐ค,
0Rโฉ โ V |
57 | | eleq1 2822 |
. . . . . . 7
โข (๐ฅ = โจ๐ง, 0Rโฉ โ
(๐ฅ โ โ โ
โจ๐ง,
0Rโฉ โ โ)) |
58 | | eleq1 2822 |
. . . . . . 7
โข (๐ฆ = โจ๐ค, 0Rโฉ โ
(๐ฆ โ โ โ
โจ๐ค,
0Rโฉ โ โ)) |
59 | 57, 58 | bi2anan9 638 |
. . . . . 6
โข ((๐ฅ = โจ๐ง, 0Rโฉ โง
๐ฆ = โจ๐ค,
0Rโฉ) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ (โจ๐ง,
0Rโฉ โ โ โง โจ๐ค, 0Rโฉ โ
โ))) |
60 | | oveq1 7416 |
. . . . . . . 8
โข (๐ฅ = โจ๐ง, 0Rโฉ โ
(๐ฅ + (i ยท ๐ฆ)) = (โจ๐ง, 0Rโฉ + (i
ยท ๐ฆ))) |
61 | | oveq2 7417 |
. . . . . . . . 9
โข (๐ฆ = โจ๐ค, 0Rโฉ โ (i
ยท ๐ฆ) = (i ยท
โจ๐ค,
0Rโฉ)) |
62 | 61 | oveq2d 7425 |
. . . . . . . 8
โข (๐ฆ = โจ๐ค, 0Rโฉ โ
(โจ๐ง,
0Rโฉ + (i ยท ๐ฆ)) = (โจ๐ง, 0Rโฉ + (i
ยท โจ๐ค,
0Rโฉ))) |
63 | 60, 62 | sylan9eq 2793 |
. . . . . . 7
โข ((๐ฅ = โจ๐ง, 0Rโฉ โง
๐ฆ = โจ๐ค,
0Rโฉ) โ (๐ฅ + (i ยท ๐ฆ)) = (โจ๐ง, 0Rโฉ + (i
ยท โจ๐ค,
0Rโฉ))) |
64 | 63 | eqeq2d 2744 |
. . . . . 6
โข ((๐ฅ = โจ๐ง, 0Rโฉ โง
๐ฆ = โจ๐ค,
0Rโฉ) โ (โจ๐ง, ๐คโฉ = (๐ฅ + (i ยท ๐ฆ)) โ โจ๐ง, ๐คโฉ = (โจ๐ง, 0Rโฉ + (i
ยท โจ๐ค,
0Rโฉ)))) |
65 | 59, 64 | anbi12d 632 |
. . . . 5
โข ((๐ฅ = โจ๐ง, 0Rโฉ โง
๐ฆ = โจ๐ค,
0Rโฉ) โ (((๐ฅ โ โ โง ๐ฆ โ โ) โง โจ๐ง, ๐คโฉ = (๐ฅ + (i ยท ๐ฆ))) โ ((โจ๐ง, 0Rโฉ โ
โ โง โจ๐ค,
0Rโฉ โ โ) โง โจ๐ง, ๐คโฉ = (โจ๐ง, 0Rโฉ + (i
ยท โจ๐ค,
0Rโฉ))))) |
66 | 55, 56, 65 | spc2ev 3598 |
. . . 4
โข
(((โจ๐ง,
0Rโฉ โ โ โง โจ๐ค, 0Rโฉ โ
โ) โง โจ๐ง,
๐คโฉ = (โจ๐ง,
0Rโฉ + (i ยท โจ๐ค, 0Rโฉ))) โ
โ๐ฅโ๐ฆ((๐ฅ โ โ โง ๐ฆ โ โ) โง โจ๐ง, ๐คโฉ = (๐ฅ + (i ยท ๐ฆ)))) |
67 | 7, 54, 66 | syl2anc 585 |
. . 3
โข ((๐ง โ R โง
๐ค โ R)
โ โ๐ฅโ๐ฆ((๐ฅ โ โ โง ๐ฆ โ โ) โง โจ๐ง, ๐คโฉ = (๐ฅ + (i ยท ๐ฆ)))) |
68 | | r2ex 3196 |
. . 3
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ โจ๐ง, ๐คโฉ = (๐ฅ + (i ยท ๐ฆ)) โ โ๐ฅโ๐ฆ((๐ฅ โ โ โง ๐ฆ โ โ) โง โจ๐ง, ๐คโฉ = (๐ฅ + (i ยท ๐ฆ)))) |
69 | 67, 68 | sylibr 233 |
. 2
โข ((๐ง โ R โง
๐ค โ R)
โ โ๐ฅ โ
โ โ๐ฆ โ
โ โจ๐ง, ๐คโฉ = (๐ฅ + (i ยท ๐ฆ))) |
70 | 1, 3, 69 | optocl 5771 |
1
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |