Theorem nadd4

Description: Rearragement of terms in a quadruple sum. (Contributed by Scott Fenton, 5-Feb-2025)

	Ref	Expression
Assertion	nadd4	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( A +no B ) +no ( C +no D ) ) = ( ( A +no C ) +no ( B +no D ) ) )

Proof

Step	Hyp	Ref	Expression
1		nadd32	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) )
2	1	3expa	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) )
3	2	adantrr	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) )
4	3	oveq1d	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( ( A +no B ) +no C ) +no D ) = ( ( ( A +no C ) +no B ) +no D ) )
5		naddcl	|- ( ( A e. On /\ B e. On ) -> ( A +no B ) e. On )
6	5	adantr	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( A +no B ) e. On )
7		simprl	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> C e. On )
8		simprr	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> D e. On )
9		naddass	|- ( ( ( A +no B ) e. On /\ C e. On /\ D e. On ) -> ( ( ( A +no B ) +no C ) +no D ) = ( ( A +no B ) +no ( C +no D ) ) )
10	6 7 8 9	syl3anc	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( ( A +no B ) +no C ) +no D ) = ( ( A +no B ) +no ( C +no D ) ) )
11		naddcl	|- ( ( A e. On /\ C e. On ) -> ( A +no C ) e. On )
12	11	ad2ant2r	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( A +no C ) e. On )
13		simplr	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> B e. On )
14		naddass	|- ( ( ( A +no C ) e. On /\ B e. On /\ D e. On ) -> ( ( ( A +no C ) +no B ) +no D ) = ( ( A +no C ) +no ( B +no D ) ) )
15	12 13 8 14	syl3anc	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( ( A +no C ) +no B ) +no D ) = ( ( A +no C ) +no ( B +no D ) ) )
16	4 10 15	3eqtr3d	|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( A +no B ) +no ( C +no D ) ) = ( ( A +no C ) +no ( B +no D ) ) )