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 ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) )