dsmmacl

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

	Ref	Expression
Hypotheses	dsmmcl.p	$⊢ P = S ⨉_{𝑠} R$
	dsmmcl.h	$⊢ H = {Base}_{(S \oplus_{m} R)}$
	dsmmcl.i	$⊢ φ \to I \in W$
	dsmmcl.s	$⊢ φ \to S \in V$
	dsmmcl.r	$⊢ φ \to R : I ⟶ Mnd$
	dsmmacl.j	$⊢ φ \to J \in H$
	dsmmacl.k	$⊢ φ \to K \in H$
	dsmmacl.a	$⊢ \underset{˙}{+} = +_{P}$
Assertion	dsmmacl	$⊢ φ \to J \underset{˙}{+} K \in H$

Proof

Step	Hyp	Ref	Expression
1		dsmmcl.p	$⊢ P = S ⨉_{𝑠} R$
2		dsmmcl.h	$⊢ H = {Base}_{(S \oplus_{m} R)}$
3		dsmmcl.i	$⊢ φ \to I \in W$
4		dsmmcl.s	$⊢ φ \to S \in V$
5		dsmmcl.r	$⊢ φ \to R : I ⟶ Mnd$
6		dsmmacl.j	$⊢ φ \to J \in H$
7		dsmmacl.k	$⊢ φ \to K \in H$
8		dsmmacl.a	$⊢ \underset{˙}{+} = +_{P}$
9		eqid	$⊢ {Base}_{P} = {Base}_{P}$
10		eqid	$⊢ S \oplus_{m} R = S \oplus_{m} R$
11	5	ffnd	$⊢ φ \to R Fn I$
12	1 10 9 2 3 11	dsmmelbas	$⊢ φ \to (J \in H \leftrightarrow (J \in {Base}_{P} \land \{a \in I \| J (a) \neq 0_{R (a)}\} \in Fin))$
13	6 12	mpbid	$⊢ φ \to (J \in {Base}_{P} \land \{a \in I \| J (a) \neq 0_{R (a)}\} \in Fin)$
14	13	simpld	$⊢ φ \to J \in {Base}_{P}$
15	1 10 9 2 3 11	dsmmelbas	$⊢ φ \to (K \in H \leftrightarrow (K \in {Base}_{P} \land \{a \in I \| K (a) \neq 0_{R (a)}\} \in Fin))$
16	7 15	mpbid	$⊢ φ \to (K \in {Base}_{P} \land \{a \in I \| K (a) \neq 0_{R (a)}\} \in Fin)$
17	16	simpld	$⊢ φ \to K \in {Base}_{P}$
18	1 9 8 4 3 5 14 17	prdsplusgcl	$⊢ φ \to J \underset{˙}{+} K \in {Base}_{P}$
19	4	adantr	$⊢ (φ \land a \in I) \to S \in V$
20	3	adantr	$⊢ (φ \land a \in I) \to I \in W$
21	11	adantr	$⊢ (φ \land a \in I) \to R Fn I$
22	14	adantr	$⊢ (φ \land a \in I) \to J \in {Base}_{P}$
23	17	adantr	$⊢ (φ \land a \in I) \to K \in {Base}_{P}$
24		simpr	$⊢ (φ \land a \in I) \to a \in I$
25	1 9 19 20 21 22 23 8 24	prdsplusgfval	$⊢ (φ \land a \in I) \to (J \underset{˙}{+} K) (a) = J (a) +_{R (a)} K (a)$
26	25	neeq1d	$⊢ (φ \land a \in I) \to ((J \underset{˙}{+} K) (a) \neq 0_{R (a)} \leftrightarrow J (a) +_{R (a)} K (a) \neq 0_{R (a)})$
27	26	rabbidva	$⊢ φ \to \{a \in I \| (J \underset{˙}{+} K) (a) \neq 0_{R (a)}\} = \{a \in I \| J (a) +_{R (a)} K (a) \neq 0_{R (a)}\}$
28	13	simprd	$⊢ φ \to \{a \in I \| J (a) \neq 0_{R (a)}\} \in Fin$
29	16	simprd	$⊢ φ \to \{a \in I \| K (a) \neq 0_{R (a)}\} \in Fin$
30		unfi	$⊢ (\{a \in I \| J (a) \neq 0_{R (a)}\} \in Fin \land \{a \in I \| K (a) \neq 0_{R (a)}\} \in Fin) \to \{a \in I \| J (a) \neq 0_{R (a)}\} \cup \{a \in I \| K (a) \neq 0_{R (a)}\} \in Fin$
31	28 29 30	syl2anc	$⊢ φ \to \{a \in I \| J (a) \neq 0_{R (a)}\} \cup \{a \in I \| K (a) \neq 0_{R (a)}\} \in Fin$
32		neorian	$⊢ (J (a) \neq 0_{R (a)} \lor K (a) \neq 0_{R (a)}) \leftrightarrow \neg (J (a) = 0_{R (a)} \land K (a) = 0_{R (a)})$
33	32	bicomi	$⊢ \neg (J (a) = 0_{R (a)} \land K (a) = 0_{R (a)}) \leftrightarrow (J (a) \neq 0_{R (a)} \lor K (a) \neq 0_{R (a)})$
34	33	con1bii	$⊢ \neg (J (a) \neq 0_{R (a)} \lor K (a) \neq 0_{R (a)}) \leftrightarrow (J (a) = 0_{R (a)} \land K (a) = 0_{R (a)})$
35	5	ffvelrnda	$⊢ (φ \land a \in I) \to R (a) \in Mnd$
36		eqid	$⊢ {Base}_{R (a)} = {Base}_{R (a)}$
37		eqid	$⊢ 0_{R (a)} = 0_{R (a)}$
38	36 37	mndidcl	$⊢ R (a) \in Mnd \to 0_{R (a)} \in {Base}_{R (a)}$
39		eqid	$⊢ +_{R (a)} = +_{R (a)}$
40	36 39 37	mndlid	$⊢ (R (a) \in Mnd \land 0_{R (a)} \in {Base}_{R (a)}) \to 0_{R (a)} +_{R (a)} 0_{R (a)} = 0_{R (a)}$
41	35 38 40	syl2anc2	$⊢ (φ \land a \in I) \to 0_{R (a)} +_{R (a)} 0_{R (a)} = 0_{R (a)}$
42		oveq12	$⊢ (J (a) = 0_{R (a)} \land K (a) = 0_{R (a)}) \to J (a) +_{R (a)} K (a) = 0_{R (a)} +_{R (a)} 0_{R (a)}$
43	42	eqeq1d	$⊢ (J (a) = 0_{R (a)} \land K (a) = 0_{R (a)}) \to (J (a) +_{R (a)} K (a) = 0_{R (a)} \leftrightarrow 0_{R (a)} +_{R (a)} 0_{R (a)} = 0_{R (a)})$
44	41 43	syl5ibrcom	$⊢ (φ \land a \in I) \to ((J (a) = 0_{R (a)} \land K (a) = 0_{R (a)}) \to J (a) +_{R (a)} K (a) = 0_{R (a)})$
45	34 44	syl5bi	$⊢ (φ \land a \in I) \to (\neg (J (a) \neq 0_{R (a)} \lor K (a) \neq 0_{R (a)}) \to J (a) +_{R (a)} K (a) = 0_{R (a)})$
46	45	necon1ad	$⊢ (φ \land a \in I) \to (J (a) +_{R (a)} K (a) \neq 0_{R (a)} \to (J (a) \neq 0_{R (a)} \lor K (a) \neq 0_{R (a)}))$
47	46	ss2rabdv	$⊢ φ \to \{a \in I \| J (a) +_{R (a)} K (a) \neq 0_{R (a)}\} \subseteq \{a \in I \| (J (a) \neq 0_{R (a)} \lor K (a) \neq 0_{R (a)})\}$
48		unrab	$⊢ \{a \in I \| J (a) \neq 0_{R (a)}\} \cup \{a \in I \| K (a) \neq 0_{R (a)}\} = \{a \in I \| (J (a) \neq 0_{R (a)} \lor K (a) \neq 0_{R (a)})\}$
49	47 48	sseqtrrdi	$⊢ φ \to \{a \in I \| J (a) +_{R (a)} K (a) \neq 0_{R (a)}\} \subseteq \{a \in I \| J (a) \neq 0_{R (a)}\} \cup \{a \in I \| K (a) \neq 0_{R (a)}\}$
50	31 49	ssfid	$⊢ φ \to \{a \in I \| J (a) +_{R (a)} K (a) \neq 0_{R (a)}\} \in Fin$
51	27 50	eqeltrd	$⊢ φ \to \{a \in I \| (J \underset{˙}{+} K) (a) \neq 0_{R (a)}\} \in Fin$
52	1 10 9 2 3 11	dsmmelbas	$⊢ φ \to (J \underset{˙}{+} K \in H \leftrightarrow (J \underset{˙}{+} K \in {Base}_{P} \land \{a \in I \| (J \underset{˙}{+} K) (a) \neq 0_{R (a)}\} \in Fin))$
53	18 51 52	mpbir2and	$⊢ φ \to J \underset{˙}{+} K \in H$

Metamath Proof Explorer

Theorem dsmmacl

Proof