Description: The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | srngstr.r | |- R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } ) |
|
Assertion | srnginvl | |- ( .* e. X -> .* = ( *r ` R ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | srngstr.r | |- R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } ) |
|
2 | 1 | srngstr | |- R Struct <. 1 , 4 >. |
3 | starvid | |- *r = Slot ( *r ` ndx ) |
|
4 | ssun2 | |- { <. ( *r ` ndx ) , .* >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } ) |
|
5 | 4 1 | sseqtrri | |- { <. ( *r ` ndx ) , .* >. } C_ R |
6 | 2 3 5 | strfv | |- ( .* e. X -> .* = ( *r ` R ) ) |