Metamath Proof Explorer

Theorem s7rn

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

Ref Expression
Hypotheses s7rn.a ⊢ φ → A ∈ V
s7rn.b ⊢ φ → B ∈ V
s7rn.c ⊢ φ → C ∈ V
s7rn.d ⊢ φ → D ∈ V
s7rn.e ⊢ φ → E ∈ V
s7rn.f ⊢ φ → F ∈ V
s7rn.g ⊢ φ → G ∈ V
Assertion s7rn ⊢ φ → ran ⁡ ⟨“ ABCDEFG ”⟩ = A B C ∪ D ∪ E F G

Proof

Step Hyp Ref Expression
1 s7rn.a ⊢ φ → A ∈ V
2 s7rn.b ⊢ φ → B ∈ V
3 s7rn.c ⊢ φ → C ∈ V
4 s7rn.d ⊢ φ → D ∈ V
5 s7rn.e ⊢ φ → E ∈ V
6 s7rn.f ⊢ φ → F ∈ V
7 s7rn.g ⊢ φ → G ∈ V
8 s4s3 ⊢ ⟨“ ABCDEFG ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EFG ”⟩
9 8 a1i ⊢ φ → ⟨“ ABCDEFG ”⟩ = ⟨“ ABCD ”⟩ ++ ⟨“ EFG ”⟩
10 9 rneqd ⊢ φ → ran ⁡ ⟨“ ABCDEFG ”⟩ = ran ⁡ ⟨“ ABCD ”⟩ ++ ⟨“ EFG ”⟩
11 s4cli ⊢ ⟨“ ABCD ”⟩ ∈ Word V
12 s3cli ⊢ ⟨“ EFG ”⟩ ∈ Word V
13 11 12 pm3.2i ⊢ ⟨“ ABCD ”⟩ ∈ Word V ∧ ⟨“ EFG ”⟩ ∈ Word V
14 ccatrn ⊢ ⟨“ ABCD ”⟩ ∈ Word V ∧ ⟨“ EFG ”⟩ ∈ Word V → ran ⁡ ⟨“ ABCD ”⟩ ++ ⟨“ EFG ”⟩ = ran ⁡ ⟨“ ABCD ”⟩ ∪ ran ⁡ ⟨“ EFG ”⟩
15 13 14 mp1i ⊢ φ → ran ⁡ ⟨“ ABCD ”⟩ ++ ⟨“ EFG ”⟩ = ran ⁡ ⟨“ ABCD ”⟩ ∪ ran ⁡ ⟨“ EFG ”⟩
16 df-s4 ⊢ ⟨“ ABCD ”⟩ = ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩
17 16 a1i ⊢ φ → ⟨“ ABCD ”⟩ = ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩
18 17 rneqd ⊢ φ → ran ⁡ ⟨“ ABCD ”⟩ = ran ⁡ ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩
19 s3cli ⊢ ⟨“ ABC ”⟩ ∈ Word V
20 s1cli ⊢ ⟨“ D ”⟩ ∈ Word V
21 19 20 pm3.2i ⊢ ⟨“ ABC ”⟩ ∈ Word V ∧ ⟨“ D ”⟩ ∈ Word V
22 ccatrn ⊢ ⟨“ ABC ”⟩ ∈ Word V ∧ ⟨“ D ”⟩ ∈ Word V → ran ⁡ ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩ = ran ⁡ ⟨“ ABC ”⟩ ∪ ran ⁡ ⟨“ D ”⟩
23 21 22 mp1i ⊢ φ → ran ⁡ ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩ = ran ⁡ ⟨“ ABC ”⟩ ∪ ran ⁡ ⟨“ D ”⟩
24 1 2 3 s3rn ⊢ φ → ran ⁡ ⟨“ ABC ”⟩ = A B C
25 s1rn ⊢ D ∈ V → ran ⁡ ⟨“ D ”⟩ = D
26 4 25 syl ⊢ φ → ran ⁡ ⟨“ D ”⟩ = D
27 24 26 uneq12d ⊢ φ → ran ⁡ ⟨“ ABC ”⟩ ∪ ran ⁡ ⟨“ D ”⟩ = A B C ∪ D
28 18 23 27 3eqtrd ⊢ φ → ran ⁡ ⟨“ ABCD ”⟩ = A B C ∪ D
29 5 6 7 s3rn ⊢ φ → ran ⁡ ⟨“ EFG ”⟩ = E F G
30 28 29 uneq12d ⊢ φ → ran ⁡ ⟨“ ABCD ”⟩ ∪ ran ⁡ ⟨“ EFG ”⟩ = A B C ∪ D ∪ E F G
31 10 15 30 3eqtrd ⊢ φ → ran ⁡ ⟨“ ABCDEFG ”⟩ = A B C ∪ D ∪ E F G