Theorem dsmmacl

Description: The finite hull is closed under addition. (Contributed by Stefan O'Rear, 11-Jan-2015)

	Ref	Expression
Hypotheses	dsmmcl.p	⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
	dsmmcl.h	⊢ 𝐻 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
	dsmmcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	dsmmcl.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	dsmmcl.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
	dsmmacl.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐻 )
	dsmmacl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐻 )
	dsmmacl.a	⊢ + = ( +g ‘ 𝑃 )
Assertion	dsmmacl	⊢ ( 𝜑 → ( 𝐽 + 𝐾 ) ∈ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		dsmmcl.p	⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
2		dsmmcl.h	⊢ 𝐻 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
3		dsmmcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4		dsmmcl.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
5		dsmmcl.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
6		dsmmacl.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐻 )
7		dsmmacl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐻 )
8		dsmmacl.a	⊢ + = ( +g ‘ 𝑃 )
9		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
10		eqid	⊢ ( 𝑆 ⊕m 𝑅 ) = ( 𝑆 ⊕m 𝑅 )
11	5	ffnd	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
12	1 10 9 2 3 11	dsmmelbas	⊢ ( 𝜑 → ( 𝐽 ∈ 𝐻 ↔ ( 𝐽 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑎 ∈ 𝐼 ∣ ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin ) ) )
13	6 12	mpbid	⊢ ( 𝜑 → ( 𝐽 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑎 ∈ 𝐼 ∣ ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin ) )
14	13	simpld	⊢ ( 𝜑 → 𝐽 ∈ ( Base ‘ 𝑃 ) )
15	1 10 9 2 3 11	dsmmelbas	⊢ ( 𝜑 → ( 𝐾 ∈ 𝐻 ↔ ( 𝐾 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑎 ∈ 𝐼 ∣ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin ) ) )
16	7 15	mpbid	⊢ ( 𝜑 → ( 𝐾 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑎 ∈ 𝐼 ∣ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin ) )
17	16	simpld	⊢ ( 𝜑 → 𝐾 ∈ ( Base ‘ 𝑃 ) )
18	1 9 8 4 3 5 14 17	prdsplusgcl	⊢ ( 𝜑 → ( 𝐽 + 𝐾 ) ∈ ( Base ‘ 𝑃 ) )
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝑆 ∈ 𝑉 )
20	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
21	11	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
22	14	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝐽 ∈ ( Base ‘ 𝑃 ) )
23	17	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝐾 ∈ ( Base ‘ 𝑃 ) )
24		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝑎 ∈ 𝐼 )
25	1 9 19 20 21 22 23 8 24	prdsplusgfval	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝐽 + 𝐾 ) ‘ 𝑎 ) = ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) )
26	25	neeq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( ( 𝐽 + 𝐾 ) ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ↔ ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) )
27	26	rabbidva	⊢ ( 𝜑 → { 𝑎 ∈ 𝐼 ∣ ( ( 𝐽 + 𝐾 ) ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } = { 𝑎 ∈ 𝐼 ∣ ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } )
28	13	simprd	⊢ ( 𝜑 → { 𝑎 ∈ 𝐼 ∣ ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin )
29	16	simprd	⊢ ( 𝜑 → { 𝑎 ∈ 𝐼 ∣ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin )
30		unfi	⊢ ( ( { 𝑎 ∈ 𝐼 ∣ ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin ∧ { 𝑎 ∈ 𝐼 ∣ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin ) → ( { 𝑎 ∈ 𝐼 ∣ ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∪ { 𝑎 ∈ 𝐼 ∣ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ) ∈ Fin )
31	28 29 30	syl2anc	⊢ ( 𝜑 → ( { 𝑎 ∈ 𝐼 ∣ ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∪ { 𝑎 ∈ 𝐼 ∣ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ) ∈ Fin )
32		neorian	⊢ ( ( ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∨ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) ↔ ¬ ( ( 𝐽 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∧ ( 𝐾 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) )
33	32	bicomi	⊢ ( ¬ ( ( 𝐽 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∧ ( 𝐾 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) ↔ ( ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∨ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) )
34	33	con1bii	⊢ ( ¬ ( ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∨ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) ↔ ( ( 𝐽 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∧ ( 𝐾 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) )
35	5	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑎 ) ∈ Mnd )
36		eqid	⊢ ( Base ‘ ( 𝑅 ‘ 𝑎 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑎 ) )
37		eqid	⊢ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) )
38	36 37	mndidcl	⊢ ( ( 𝑅 ‘ 𝑎 ) ∈ Mnd → ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑎 ) ) )
39		eqid	⊢ ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) = ( +g ‘ ( 𝑅 ‘ 𝑎 ) )
40	36 39 37	mndlid	⊢ ( ( ( 𝑅 ‘ 𝑎 ) ∈ Mnd ∧ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑎 ) ) ) → ( ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) )
41	35 38 40	syl2anc2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) )
42		oveq12	⊢ ( ( ( 𝐽 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∧ ( 𝐾 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) → ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) = ( ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) )
43	42	eqeq1d	⊢ ( ( ( 𝐽 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∧ ( 𝐾 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) → ( ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ↔ ( ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) )
44	41 43	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( ( 𝐽 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∧ ( 𝐾 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) → ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) )
45	34 44	syl5bi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ¬ ( ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∨ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) → ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) )
46	45	necon1ad	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) → ( ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∨ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) ) )
47	46	ss2rabdv	⊢ ( 𝜑 → { 𝑎 ∈ 𝐼 ∣ ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ⊆ { 𝑎 ∈ 𝐼 ∣ ( ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∨ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) } )
48		unrab	⊢ ( { 𝑎 ∈ 𝐼 ∣ ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∪ { 𝑎 ∈ 𝐼 ∣ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ) = { 𝑎 ∈ 𝐼 ∣ ( ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ∨ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ) }
49	47 48	sseqtrrdi	⊢ ( 𝜑 → { 𝑎 ∈ 𝐼 ∣ ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ⊆ ( { 𝑎 ∈ 𝐼 ∣ ( 𝐽 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∪ { 𝑎 ∈ 𝐼 ∣ ( 𝐾 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ) )
50	31 49	ssfid	⊢ ( 𝜑 → { 𝑎 ∈ 𝐼 ∣ ( ( 𝐽 ‘ 𝑎 ) ( +g ‘ ( 𝑅 ‘ 𝑎 ) ) ( 𝐾 ‘ 𝑎 ) ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin )
51	27 50	eqeltrd	⊢ ( 𝜑 → { 𝑎 ∈ 𝐼 ∣ ( ( 𝐽 + 𝐾 ) ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin )
52	1 10 9 2 3 11	dsmmelbas	⊢ ( 𝜑 → ( ( 𝐽 + 𝐾 ) ∈ 𝐻 ↔ ( ( 𝐽 + 𝐾 ) ∈ ( Base ‘ 𝑃 ) ∧ { 𝑎 ∈ 𝐼 ∣ ( ( 𝐽 + 𝐾 ) ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin ) ) )
53	18 51 52	mpbir2and	⊢ ( 𝜑 → ( 𝐽 + 𝐾 ) ∈ 𝐻 )