This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ofs1

Description: Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018)

Ref Expression
Assertion ofs1 
|- ( ( A e. S /\ B e. T ) -> ( <" A "> oF R <" B "> ) = <" ( A R B ) "> )

Proof

Step Hyp Ref Expression
1 snex 
 |-  { 0 } e. _V
2 1 a1i 
 |-  ( ( A e. S /\ B e. T ) -> { 0 } e. _V )
3 simpll 
 |-  ( ( ( A e. S /\ B e. T ) /\ i e. { 0 } ) -> A e. S )
4 simplr 
 |-  ( ( ( A e. S /\ B e. T ) /\ i e. { 0 } ) -> B e. T )
5 s1val 
 |-  ( A e. S -> <" A "> = { <. 0 , A >. } )
6 0nn0 
 |-  0 e. NN0
7 fmptsn 
 |-  ( ( 0 e. NN0 /\ A e. S ) -> { <. 0 , A >. } = ( i e. { 0 } |-> A ) )
8 6 7 mpan 
 |-  ( A e. S -> { <. 0 , A >. } = ( i e. { 0 } |-> A ) )
9 5 8 eqtrd 
 |-  ( A e. S -> <" A "> = ( i e. { 0 } |-> A ) )
10 9 adantr 
 |-  ( ( A e. S /\ B e. T ) -> <" A "> = ( i e. { 0 } |-> A ) )
11 s1val 
 |-  ( B e. T -> <" B "> = { <. 0 , B >. } )
12 fmptsn 
 |-  ( ( 0 e. NN0 /\ B e. T ) -> { <. 0 , B >. } = ( i e. { 0 } |-> B ) )
13 6 12 mpan 
 |-  ( B e. T -> { <. 0 , B >. } = ( i e. { 0 } |-> B ) )
14 11 13 eqtrd 
 |-  ( B e. T -> <" B "> = ( i e. { 0 } |-> B ) )
15 14 adantl 
 |-  ( ( A e. S /\ B e. T ) -> <" B "> = ( i e. { 0 } |-> B ) )
16 2 3 4 10 15 offval2 
 |-  ( ( A e. S /\ B e. T ) -> ( <" A "> oF R <" B "> ) = ( i e. { 0 } |-> ( A R B ) ) )
17 ovex 
 |-  ( A R B ) e. _V
18 s1val 
 |-  ( ( A R B ) e. _V -> <" ( A R B ) "> = { <. 0 , ( A R B ) >. } )
19 17 18 ax-mp 
 |-  <" ( A R B ) "> = { <. 0 , ( A R B ) >. }
20 fmptsn 
 |-  ( ( 0 e. NN0 /\ ( A R B ) e. _V ) -> { <. 0 , ( A R B ) >. } = ( i e. { 0 } |-> ( A R B ) ) )
21 6 17 20 mp2an 
 |-  { <. 0 , ( A R B ) >. } = ( i e. { 0 } |-> ( A R B ) )
22 19 21 eqtri 
 |-  <" ( A R B ) "> = ( i e. { 0 } |-> ( A R B ) )
23 16 22 eqtr4di 
 |-  ( ( A e. S /\ B e. T ) -> ( <" A "> oF R <" B "> ) = <" ( A R B ) "> )