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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
s7rn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
s7rn.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
s7rn.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
s7rn.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
s7rn.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
s7rn.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
Assertion s7rn ( 𝜑 → ran ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) )

Proof

Step Hyp Ref Expression
1 s7rn.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 s7rn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3 s7rn.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 s7rn.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
5 s7rn.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
6 s7rn.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
7 s7rn.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
8 s4s3 ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ++ ⟨“ 𝐸 𝐹 𝐺 ”⟩ )
9 8 a1i ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ++ ⟨“ 𝐸 𝐹 𝐺 ”⟩ ) )
10 9 rneqd ⊢ ( 𝜑 → ran ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ran ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ++ ⟨“ 𝐸 𝐹 𝐺 ”⟩ ) )
11 s4cli ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∈ Word V
12 s3cli ⊢ ⟨“ 𝐸 𝐹 𝐺 ”⟩ ∈ Word V
13 11 12 pm3.2i ⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∈ Word V ∧ ⟨“ 𝐸 𝐹 𝐺 ”⟩ ∈ Word V )
14 ccatrn ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∈ Word V ∧ ⟨“ 𝐸 𝐹 𝐺 ”⟩ ∈ Word V ) → ran ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ++ ⟨“ 𝐸 𝐹 𝐺 ”⟩ ) = ( ran ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∪ ran ⟨“ 𝐸 𝐹 𝐺 ”⟩ ) )
15 13 14 mp1i ⊢ ( 𝜑 → ran ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ++ ⟨“ 𝐸 𝐹 𝐺 ”⟩ ) = ( ran ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∪ ran ⟨“ 𝐸 𝐹 𝐺 ”⟩ ) )
16 df-s4 ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ )
17 16 a1i ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) )
18 17 rneqd ⊢ ( 𝜑 → ran ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ran ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) )
19 s3cli ⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word V
20 s1cli ⊢ ⟨“ 𝐷 ”⟩ ∈ Word V
21 19 20 pm3.2i ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word V ∧ ⟨“ 𝐷 ”⟩ ∈ Word V )
22 ccatrn ⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word V ∧ ⟨“ 𝐷 ”⟩ ∈ Word V ) → ran ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) = ( ran ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∪ ran ⟨“ 𝐷 ”⟩ ) )
23 21 22 mp1i ⊢ ( 𝜑 → ran ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ ) = ( ran ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∪ ran ⟨“ 𝐷 ”⟩ ) )
24 1 2 3 s3rn ⊢ ( 𝜑 → ran ⟨“ 𝐴 𝐵 𝐶 ”⟩ = { 𝐴 , 𝐵 , 𝐶 } )
25 s1rn ⊢ ( 𝐷 ∈ 𝑉 → ran ⟨“ 𝐷 ”⟩ = { 𝐷 } )
26 4 25 syl ⊢ ( 𝜑 → ran ⟨“ 𝐷 ”⟩ = { 𝐷 } )
27 24 26 uneq12d ⊢ ( 𝜑 → ( ran ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∪ ran ⟨“ 𝐷 ”⟩ ) = ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) )
28 18 23 27 3eqtrd ⊢ ( 𝜑 → ran ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) )
29 5 6 7 s3rn ⊢ ( 𝜑 → ran ⟨“ 𝐸 𝐹 𝐺 ”⟩ = { 𝐸 , 𝐹 , 𝐺 } )
30 28 29 uneq12d ⊢ ( 𝜑 → ( ran ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∪ ran ⟨“ 𝐸 𝐹 𝐺 ”⟩ ) = ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) )
31 10 15 30 3eqtrd ⊢ ( 𝜑 → ran ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) )