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

Metamath Proof Explorer

Theorem s7rn

Description: Range of a length 7 string. (Contributed by AV, 30-Jul-2025)

Ref Expression
Hypotheses s7rn.a 
|- ( ph -> A e. V )
s7rn.b 
|- ( ph -> B e. V )
s7rn.c 
|- ( ph -> C e. V )
s7rn.d 
|- ( ph -> D e. V )
s7rn.e 
|- ( ph -> E e. V )
s7rn.f 
|- ( ph -> F e. V )
s7rn.g 
|- ( ph -> G e. V )
Assertion s7rn 
|- ( ph -> ran <" A B C D E F G "> = ( ( { A , B , C } u. { D } ) u. { E , F , G } ) )

Proof

Step Hyp Ref Expression
1 s7rn.a 
 |-  ( ph -> A e. V )
2 s7rn.b 
 |-  ( ph -> B e. V )
3 s7rn.c 
 |-  ( ph -> C e. V )
4 s7rn.d 
 |-  ( ph -> D e. V )
5 s7rn.e 
 |-  ( ph -> E e. V )
6 s7rn.f 
 |-  ( ph -> F e. V )
7 s7rn.g 
 |-  ( ph -> G e. V )
8 s4s3 
 |-  <" A B C D E F G "> = ( <" A B C D "> ++ <" E F G "> )
9 8 a1i 
 |-  ( ph -> <" A B C D E F G "> = ( <" A B C D "> ++ <" E F G "> ) )
10 9 rneqd 
 |-  ( ph -> ran <" A B C D E F G "> = ran ( <" A B C D "> ++ <" E F G "> ) )
11 s4cli 
 |-  <" A B C D "> e. Word _V
12 s3cli 
 |-  <" E F G "> e. Word _V
13 11 12 pm3.2i 
 |-  ( <" A B C D "> e. Word _V /\ <" E F G "> e. Word _V )
14 ccatrn 
 |-  ( ( <" A B C D "> e. Word _V /\ <" E F G "> e. Word _V ) -> ran ( <" A B C D "> ++ <" E F G "> ) = ( ran <" A B C D "> u. ran <" E F G "> ) )
15 13 14 mp1i 
 |-  ( ph -> ran ( <" A B C D "> ++ <" E F G "> ) = ( ran <" A B C D "> u. ran <" E F G "> ) )
16 df-s4 
 |-  <" A B C D "> = ( <" A B C "> ++ <" D "> )
17 16 a1i 
 |-  ( ph -> <" A B C D "> = ( <" A B C "> ++ <" D "> ) )
18 17 rneqd 
 |-  ( ph -> ran <" A B C D "> = ran ( <" A B C "> ++ <" D "> ) )
19 s3cli 
 |-  <" A B C "> e. Word _V
20 s1cli 
 |-  <" D "> e. Word _V
21 19 20 pm3.2i 
 |-  ( <" A B C "> e. Word _V /\ <" D "> e. Word _V )
22 ccatrn 
 |-  ( ( <" A B C "> e. Word _V /\ <" D "> e. Word _V ) -> ran ( <" A B C "> ++ <" D "> ) = ( ran <" A B C "> u. ran <" D "> ) )
23 21 22 mp1i 
 |-  ( ph -> ran ( <" A B C "> ++ <" D "> ) = ( ran <" A B C "> u. ran <" D "> ) )
24 1 2 3 s3rn 
 |-  ( ph -> ran <" A B C "> = { A , B , C } )
25 s1rn 
 |-  ( D e. V -> ran <" D "> = { D } )
26 4 25 syl 
 |-  ( ph -> ran <" D "> = { D } )
27 24 26 uneq12d 
 |-  ( ph -> ( ran <" A B C "> u. ran <" D "> ) = ( { A , B , C } u. { D } ) )
28 18 23 27 3eqtrd 
 |-  ( ph -> ran <" A B C D "> = ( { A , B , C } u. { D } ) )
29 5 6 7 s3rn 
 |-  ( ph -> ran <" E F G "> = { E , F , G } )
30 28 29 uneq12d 
 |-  ( ph -> ( ran <" A B C D "> u. ran <" E F G "> ) = ( ( { A , B , C } u. { D } ) u. { E , F , G } ) )
31 10 15 30 3eqtrd 
 |-  ( ph -> ran <" A B C D E F G "> = ( ( { A , B , C } u. { D } ) u. { E , F , G } ) )