Metamath Proof Explorer

Theorem issubmd

Description: Deduction for proving a submonoid. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses issubmd.b ⊢B=BaseM
issubmd.p ⊢+˙=+M
issubmd.z ⊢0˙=0M
issubmd.m ⊢φ→M∈Mnd
issubmd.cz ⊢φ→χ
issubmd.cp ⊢φ∧x∈B∧y∈B∧θ∧τ→η
issubmd.ch ⊢z=0˙→ψ↔χ
issubmd.th ⊢z=x→ψ↔θ
issubmd.ta ⊢z=y→ψ↔τ
issubmd.et ⊢z=x+˙y→ψ↔η
Assertion issubmd ⊢φ→z∈B|ψ∈SubMnd⁡M

Proof

Step Hyp Ref Expression
1 issubmd.b ⊢B=BaseM
2 issubmd.p ⊢+˙=+M
3 issubmd.z ⊢0˙=0M
4 issubmd.m ⊢φ→M∈Mnd
5 issubmd.cz ⊢φ→χ
6 issubmd.cp ⊢φ∧x∈B∧y∈B∧θ∧τ→η
7 issubmd.ch ⊢z=0˙→ψ↔χ
8 issubmd.th ⊢z=x→ψ↔θ
9 issubmd.ta ⊢z=y→ψ↔τ
10 issubmd.et ⊢z=x+˙y→ψ↔η
11 ssrab2 ⊢z∈B|ψ⊆B
12 11 a1i ⊢φ→z∈B|ψ⊆B
13 1 3 mndidcl ⊢M∈Mnd→0˙∈B
14 4 13 syl ⊢φ→0˙∈B
15 7 14 5 elrabd ⊢φ→0˙∈z∈B|ψ
16 8 elrab ⊢x∈z∈B|ψ↔x∈B∧θ
17 9 elrab ⊢y∈z∈B|ψ↔y∈B∧τ
18 16 17 anbi12i ⊢x∈z∈B|ψ∧y∈z∈B|ψ↔x∈B∧θ∧y∈B∧τ
19 4 adantr ⊢φ∧x∈B∧θ∧y∈B∧τ→M∈Mnd
20 simprll ⊢φ∧x∈B∧θ∧y∈B∧τ→x∈B
21 simprrl ⊢φ∧x∈B∧θ∧y∈B∧τ→y∈B
22 1 2 mndcl ⊢M∈Mnd∧x∈B∧y∈B→x+˙y∈B
23 19 20 21 22 syl3anc ⊢φ∧x∈B∧θ∧y∈B∧τ→x+˙y∈B
24 an4 ⊢x∈B∧θ∧y∈B∧τ↔x∈B∧y∈B∧θ∧τ
25 24 6 sylan2b ⊢φ∧x∈B∧θ∧y∈B∧τ→η
26 10 23 25 elrabd ⊢φ∧x∈B∧θ∧y∈B∧τ→x+˙y∈z∈B|ψ
27 18 26 sylan2b ⊢φ∧x∈z∈B|ψ∧y∈z∈B|ψ→x+˙y∈z∈B|ψ
28 27 ralrimivva ⊢φ→∀x∈z∈B|ψ∀y∈z∈B|ψx+˙y∈z∈B|ψ
29 1 3 2 issubm ⊢M∈Mnd→z∈B|ψ∈SubMnd⁡M↔z∈B|ψ⊆B∧0˙∈z∈B|ψ∧∀x∈z∈B|ψ∀y∈z∈B|ψx+˙y∈z∈B|ψ
30 4 29 syl ⊢φ→z∈B|ψ∈SubMnd⁡M↔z∈B|ψ⊆B∧0˙∈z∈B|ψ∧∀x∈z∈B|ψ∀y∈z∈B|ψx+˙y∈z∈B|ψ
31 12 15 28 30 mpbir3and ⊢φ→z∈B|ψ∈SubMnd⁡M