Step |
Hyp |
Ref |
Expression |
1 |
|
invrfval.u |
⊢ 𝑈 = ( Unit ‘ 𝑅 ) |
2 |
|
invrfval.g |
⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) |
3 |
|
invrfval.i |
⊢ 𝐼 = ( invr ‘ 𝑅 ) |
4 |
|
fveq2 |
⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) ) |
5 |
|
fveq2 |
⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) ) |
6 |
5 1
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = 𝑈 ) |
7 |
4 6
|
oveq12d |
⊢ ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) |
8 |
7 2
|
eqtr4di |
⊢ ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) = 𝐺 ) |
9 |
8
|
fveq2d |
⊢ ( 𝑟 = 𝑅 → ( invg ‘ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ) = ( invg ‘ 𝐺 ) ) |
10 |
|
df-invr |
⊢ invr = ( 𝑟 ∈ V ↦ ( invg ‘ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ) ) |
11 |
|
fvex |
⊢ ( invg ‘ 𝐺 ) ∈ V |
12 |
9 10 11
|
fvmpt |
⊢ ( 𝑅 ∈ V → ( invr ‘ 𝑅 ) = ( invg ‘ 𝐺 ) ) |
13 |
|
fvprc |
⊢ ( ¬ 𝑅 ∈ V → ( invr ‘ 𝑅 ) = ∅ ) |
14 |
|
base0 |
⊢ ∅ = ( Base ‘ ∅ ) |
15 |
|
eqid |
⊢ ( invg ‘ ∅ ) = ( invg ‘ ∅ ) |
16 |
14 15
|
grpinvfn |
⊢ ( invg ‘ ∅ ) Fn ∅ |
17 |
|
fn0 |
⊢ ( ( invg ‘ ∅ ) Fn ∅ ↔ ( invg ‘ ∅ ) = ∅ ) |
18 |
16 17
|
mpbi |
⊢ ( invg ‘ ∅ ) = ∅ |
19 |
13 18
|
eqtr4di |
⊢ ( ¬ 𝑅 ∈ V → ( invr ‘ 𝑅 ) = ( invg ‘ ∅ ) ) |
20 |
|
fvprc |
⊢ ( ¬ 𝑅 ∈ V → ( mulGrp ‘ 𝑅 ) = ∅ ) |
21 |
20
|
oveq1d |
⊢ ( ¬ 𝑅 ∈ V → ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) = ( ∅ ↾s 𝑈 ) ) |
22 |
2 21
|
eqtrid |
⊢ ( ¬ 𝑅 ∈ V → 𝐺 = ( ∅ ↾s 𝑈 ) ) |
23 |
|
ress0 |
⊢ ( ∅ ↾s 𝑈 ) = ∅ |
24 |
22 23
|
eqtrdi |
⊢ ( ¬ 𝑅 ∈ V → 𝐺 = ∅ ) |
25 |
24
|
fveq2d |
⊢ ( ¬ 𝑅 ∈ V → ( invg ‘ 𝐺 ) = ( invg ‘ ∅ ) ) |
26 |
19 25
|
eqtr4d |
⊢ ( ¬ 𝑅 ∈ V → ( invr ‘ 𝑅 ) = ( invg ‘ 𝐺 ) ) |
27 |
12 26
|
pm2.61i |
⊢ ( invr ‘ 𝑅 ) = ( invg ‘ 𝐺 ) |
28 |
3 27
|
eqtri |
⊢ 𝐼 = ( invg ‘ 𝐺 ) |