Description: Lemma for opprbas and oppradd . (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by AV, 6-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opprbas.1 | ⊢ 𝑂 = ( oppr ‘ 𝑅 ) | |
opprlem.2 | ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx ) | ||
opprlem.3 | ⊢ ( 𝐸 ‘ ndx ) ≠ ( .r ‘ ndx ) | ||
Assertion | opprlem | ⊢ ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑂 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opprbas.1 | ⊢ 𝑂 = ( oppr ‘ 𝑅 ) | |
2 | opprlem.2 | ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx ) | |
3 | opprlem.3 | ⊢ ( 𝐸 ‘ ndx ) ≠ ( .r ‘ ndx ) | |
4 | 2 3 | setsnid | ⊢ ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ( 𝑅 sSet 〈 ( .r ‘ ndx ) , tpos ( .r ‘ 𝑅 ) 〉 ) ) |
5 | eqid | ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) | |
6 | eqid | ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) | |
7 | 5 6 1 | opprval | ⊢ 𝑂 = ( 𝑅 sSet 〈 ( .r ‘ ndx ) , tpos ( .r ‘ 𝑅 ) 〉 ) |
8 | 7 | fveq2i | ⊢ ( 𝐸 ‘ 𝑂 ) = ( 𝐸 ‘ ( 𝑅 sSet 〈 ( .r ‘ ndx ) , tpos ( .r ‘ 𝑅 ) 〉 ) ) |
9 | 4 8 | eqtr4i | ⊢ ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑂 ) |