Metamath Proof Explorer


Theorem s4prop

Description: A length 4 word is a union of two unordered pairs of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017)

Ref Expression
Assertion s4prop A S B S C S D S ⟨“ ABCD ”⟩ = 0 A 1 B 2 C 3 D

Proof

Step Hyp Ref Expression
1 df-s4 ⟨“ ABCD ”⟩ = ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩
2 simpl A S B S A S
3 2 adantr A S B S C S D S A S
4 simpr A S B S B S
5 4 adantr A S B S C S D S B S
6 simpl C S D S C S
7 6 adantl A S B S C S D S C S
8 3 5 7 s3cld A S B S C S D S ⟨“ ABC ”⟩ Word S
9 simpr C S D S D S
10 9 adantl A S B S C S D S D S
11 cats1un ⟨“ ABC ”⟩ Word S D S ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩ = ⟨“ ABC ”⟩ ⟨“ ABC ”⟩ D
12 8 10 11 syl2anc A S B S C S D S ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩ = ⟨“ ABC ”⟩ ⟨“ ABC ”⟩ D
13 df-s3 ⟨“ ABC ”⟩ = ⟨“ AB ”⟩ ++ ⟨“ C ”⟩
14 s2cl A S B S ⟨“ AB ”⟩ Word S
15 14 adantr A S B S C S D S ⟨“ AB ”⟩ Word S
16 cats1un ⟨“ AB ”⟩ Word S C S ⟨“ AB ”⟩ ++ ⟨“ C ”⟩ = ⟨“ AB ”⟩ ⟨“ AB ”⟩ C
17 15 7 16 syl2anc A S B S C S D S ⟨“ AB ”⟩ ++ ⟨“ C ”⟩ = ⟨“ AB ”⟩ ⟨“ AB ”⟩ C
18 13 17 syl5eq A S B S C S D S ⟨“ ABC ”⟩ = ⟨“ AB ”⟩ ⟨“ AB ”⟩ C
19 s2prop A S B S ⟨“ AB ”⟩ = 0 A 1 B
20 19 adantr A S B S C S D S ⟨“ AB ”⟩ = 0 A 1 B
21 20 uneq1d A S B S C S D S ⟨“ AB ”⟩ ⟨“ AB ”⟩ C = 0 A 1 B ⟨“ AB ”⟩ C
22 18 21 eqtrd A S B S C S D S ⟨“ ABC ”⟩ = 0 A 1 B ⟨“ AB ”⟩ C
23 22 uneq1d A S B S C S D S ⟨“ ABC ”⟩ ⟨“ ABC ”⟩ D = 0 A 1 B ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D
24 12 23 eqtrd A S B S C S D S ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩ = 0 A 1 B ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D
25 unass 0 A 1 B ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D = 0 A 1 B ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D
26 25 a1i A S B S C S D S 0 A 1 B ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D = 0 A 1 B ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D
27 df-pr ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D = ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D
28 s2len ⟨“ AB ”⟩ = 2
29 28 a1i A S B S C S D S ⟨“ AB ”⟩ = 2
30 29 opeq1d A S B S C S D S ⟨“ AB ”⟩ C = 2 C
31 s3len ⟨“ ABC ”⟩ = 3
32 31 a1i A S B S C S D S ⟨“ ABC ”⟩ = 3
33 32 opeq1d A S B S C S D S ⟨“ ABC ”⟩ D = 3 D
34 30 33 preq12d A S B S C S D S ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D = 2 C 3 D
35 27 34 eqtr3id A S B S C S D S ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D = 2 C 3 D
36 35 uneq2d A S B S C S D S 0 A 1 B ⟨“ AB ”⟩ C ⟨“ ABC ”⟩ D = 0 A 1 B 2 C 3 D
37 24 26 36 3eqtrd A S B S C S D S ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩ = 0 A 1 B 2 C 3 D
38 1 37 syl5eq A S B S C S D S ⟨“ ABCD ”⟩ = 0 A 1 B 2 C 3 D