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 ) "> )